Fitch Biconditional Proof Hilfe?

Tipp: Stellen Sie immer einen Zusammenhang mit dem her, was ausgetragen werden muss, um das Ziel abzuleiten. Wenn Sie also darauf abzielen, einen universellen Quantor einzuführen, müssen Sie den Unterbeweis beginnen, indem Sie einen beliebigen Term annehmen . In diesem Fall zweimal.

Nehmen wir an, die willkürlichen Terme [a] und [b] leiten irgendwie die Biconditional ab (Hinweis: Es werden mehrere universelle Eliminierungen beteiligt sein), und führen dann zwei Universalien ein.

|  Ɐx Ɐy (Indiff(x,y)→Indiff(y,x))        Premise
|_ :
|  :
|  |_ [a]                                 Assumption
|  |  |_ [b]                              Assumption
|  |  |  Ɐx Ɐy (Indiff(x,y)→Indiff(y,x))  Reiteration
|  |  |  :
|  |  |  Indiff(a,b)↔Indiff(b,a)          Biconditional Introduction
|  |  Ɐy (Indiff(a,y)↔Indiff(y,a))        Universal Introduction
|  Ɐx Ɐy (Indiff(x,y)↔Indiff(y,x))        Universal Introduction
■

Die Füllung in der Mitte sollte nicht zu hart sein. Es sieht so aus, als ob Ihr Checker eine bikonditionale Einführung benötigt, um so auszusehen:

h|  |_ X    Assumption
:|  |  :
k|  |  Y    Somehow derived
 |  +
n|  |_ Y    Assumption
:|  |  :
m|  |  X    Somehow derived
 |  X ↔ Y   Biconditional Introduction (h-k,n-m)

Ich verwende einen anderen Proof-Checker, aber vielleicht hilft es, wenn Sie sehen, wie das Ziel hier erreicht wird, damit dies mit dem von Ihnen verwendeten Proof-Checker funktioniert.

Dieser Proof-Checker hat eine andere Art, wohlgeformte Formeln zu akzeptieren. Ich habe "Indiff" durch "I" ersetzt.

Mir ist auch aufgefallen, dass das Ziel einfach "∀x∀y(Ixy↔Iyx)" war, also "∀x∀y(Indiff(x,y) ↔ Indiff(y,x)", und Sie als fünfter hatten Prämisse "∀x∀y(Ixy → Iyx)", das heißt "∀x∀y(Indiff(x,y) → Indiff(y,x)". Ich musste nur diese Prämisse verwenden und habe sie daher nicht aufgenommen die Anderen.

Um einen Biconditional zu erhalten, musste ich zwei bedingte Unterbeweise beginnen. Beim ersten nahm ich „Iab“ in Zeile 2 an und erreichte das Ziel dieses Unterbeweises „Iba“ in Zeile 5. Beim zweiten Unterbeweis ging ich in die entgegengesetzte Richtung und nahm „Iba“ in Zeile 6 an und erreichte das Ziel „Iab“. " in Zeile 9. In jedem Unterbeweis habe ich den universellen Quantor eliminiert, aber Namen für die "x"- und "y"-Variablen verwendet, die mir geholfen haben, die Schlussfolgerung zu ziehen.

Als ich in Zeile 10 die Biconditional einführte, löste dies die Annahmen in den Zeilen 2 und 6 auf.

Eine Beschreibung der Regeln finden Sie in forallx (Link unten). Universelle Elimination (∀E) siehe Seite 239-240. Zur bedingten Eliminierung (→E) siehe Seiten 103-104. Zur bikonditionalen Einführung (↔I) siehe Seiten 111-112. Universelle Einführung (∀I) siehe Seiten 243-246.

---

Verweise

Kevin Klements JavaScript/PHP-Beweiseditor und -prüfer im Fitch-Stil für natürliche Deduktion http://proofs.openlogicproject.org/

PD Magnus, Tim Button mit Ergänzungen von J. Robert Loftis, remixt und überarbeitet von Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/