Fitch Proof by Contradiction Hilfe

Die Schlußregeln werden so benannt, wie sie aus einem Grund sind.

Wenn Sie das Bedürfnis verspüren, einen Kontext anzusprechen, um ein Ziel abzuleiten, legen Sie fest, welche Einführungsregel Sie benötigen, um das Ziel abzuleiten. Das wird Ihnen sagen, welche Annahme Sie möglicherweise aufstellen und welche Schlussfolgerung Sie ableiten müssen .

• Wenn das Ziel eine Bedingung ist, wie Indiff(a,b) → ~(StrongPref(b,a) v StrongPref(a,b)), verwenden Sie die bedingte Einführung . Nehmen Sie den Vordersatz an und leiten Sie den Nachsatz ab .

• Wenn das Ziel eine Negation ist, wie etwa ~(StrongPref(b,a) v StrongPref(a,b)), verwenden Sie die Negation Introduction . Nehmen Sie das Positive an und leiten Sie einen Widerspruch her.

Wenn Sie ein Ziel erreichen, das nicht durch eine Einführungsregel erzeugt wird, suchen Sie in den Annahmen (und Prämissen) nach Ausschlussregeln , um die Ableitungen zu ergänzen.

• Wenn Sie eine Disjunktion wie StrongPref(b,a) v StrongPref(a,b) angenommen haben, verwenden Sie die Disjunktionsbeseitigung . Nehmen Sie jeden Fall nacheinander an und leiten Sie die gleiche Konsequenz ab.

Das eigentliche Ableiten des Widerspruchs überlasse ich Ihnen (aber okay, Prämissen 3 und 4 sind am nützlichsten).

|  Ɐx Ɐy StrongPref(x,y) ↔ ~WeakPref(y,x) 
|  Ɐx Ɐy Indiff(x,y) → WeakPref(y,x) ^ WeakPref(x,y)
|  |_ [a]
|  |  |_ [b]
|  |  |  |_ Indiff(a,b)
|  |  |  |  :
|  |  |  |  |_ StrongPref(b,a) v StrongPref(a,b)
|  |  |  |  |  |_ StrongPref(b,a)
|  |  |  |  |  |  :
|  |  |  |  |  |  #
|  |  |  |  |  +
|  |  |  |  |  |_ StrongPref(a,b)
|  |  |  |  |  |  :
|  |  |  |  |  |  #
|  |  |  |  |  #
|  |  |  |  ~(StrongPref(b,a) v StrongPref(a,b))
|  |  |  Indiff(a,b) → ~(StrongPref(b,a) v StrongPref(a,b))
|  |  :

Bearbeiten: der fertige Beweis

:
|  Ɐx Ɐy StrongPref(x,y) ↔ ~WeakPref(y,x) 
|_ Ɐx Ɐy Indiff(x,y) → WeakPref(y,x) ^ WeakPref(x,y)
|  |_ [a]                                                   Arbitrary Term
|  |  |_ [b]                                                Arbitrary Term
|  |  |  |_ Indiff(a,b)                                     Assumption
|  |  |  |  Ɐy Indiff(a,y) → WeakPref(y,a) ^ WeakPref(a,y)  Universal Elimination
|  |  |  |  Indiff(a,b) → WeakPref(b,a) ^ WeakPref(a,b)     Universal Elimination
|  |  |  |  WeakPref(b,a) ^ WeakPref(a,b)                   Conditional Elimination
|  |  |  |  WeakPref(b,a)                                   Conjunction Elimination 
|  |  |  |  WeakPref(a,b)                                   Conjunction Elimination
|  |  |  |  |_ StrongPref(b,a) v StrongPref(a,b)            Assumption
|  |  |  |  |  |_ StrongPref(b,a)                           Assumption
|  |  |  |  |  |  Ɐy StrongPref(b,y) ↔ ~WeakPref(y,b)       Universal Elimination
|  |  |  |  |  |  StrongPref(b,a) ↔ ~WeakPref(a,b)          Universal Elimination
|  |  |  |  |  |  ~WeakPref(a,b)                            Biconditional Elimination
|  |  |  |  |  |  #                                         Negation Elimination
|  |  |  |  |  +
|  |  |  |  |  |_ StrongPref(a,b)
|  |  |  |  |  |  Ɐy StrongPref(a,y) ↔ ~WeakPref(y,a)       Universal Elimination
|  |  |  |  |  |  StrongPref(a,b) ↔ ~WeakPref(b,a)          Universal Elimination
|  |  |  |  |  |  ~WeakPref(b,a)                            Biconditional Elimination
|  |  |  |  |  |  #                                         Negation Elimination
|  |  |  |  |  #                                            Disjunction Elimination
|  |  |  |  ~(StrongPref(b,a) v StrongPref(a,b))            Negation Introduction
|  |  |  Indiff(a,b) → ~(StrongPref(b,a) v StrongPref(a,b)) Conditional Introduction
|  |  Ɐy Indiff(a,y) → ~(StrongPref(y,a) v StrongPref(a,y)) Universal Introduction
|  Ɐx Ɐy Indiff(x,y) → ~(StrongPref(y,x) v StrongPref(x,y)) Universal Introduction

Hier ist ein Beweis mit einem anderen Beweisprüfer. Ich habe auch einige Substitutionen vorgenommen.

• Für Indiff habe ich I verwendet .
• Für StrongPref habe ich S verwendet .
• Für WeakPref habe ich W verwendet .

Von den vier Räumlichkeiten habe ich nur die dritte und vierte genutzt.

Hier die Bedenken:

Ich bin jetzt so weit in den Beweis eingestiegen, aber ich bin mir nicht sicher, ob das, was ich tue, falsch ist, da ich keine universellen Instanziierungen mehr verwenden kann. Ebenso kann ich den für ~(StrongPref(b,a) v StrongPref(a,b)) erforderlichen Widerspruch nicht finden.

Ich stieß auch auf ein Problem mit den universellen Instanziierungen oder Einführungen, aber ich hatte zwei separate Prämissen, auf denen ich die universelle Eliminierung verwendete. Ich habe die Variablen in den universellen Aussagen unter diesen beiden Prämissen nicht mit denselben Namen verknüpft. Mit anderen Worten, nur weil ich „x“ mit „a“ in der vierten Prämisse assoziiert habe, heißt das nicht, dass ich „x“ nicht mit „b“ in der dritten Prämisse assoziieren kann. Ähnlich für "y". Das "x" und "y" sind Variablen und können für beliebige Namen stehen, da es sich um universell quantifizierte Variablen handelt. Jeder Name kann verwendet werden.

Um insbesondere den Universalquantor von „x“ in Prämisse 4 zu eliminieren, habe ich die Variable „x“ in Zeile 5 durch den Namen „a“ ersetzt. Dann habe ich den Universalquantor von „y“ in Zeile 5 eliminiert, indem ich die Variable ersetzt habe „y“ mit dem Namen „b“. Daraus entstand Zeile 6.

In Zeile 9 habe ich jedoch die universelle Eliminierung unter Prämisse 3 verwendet, indem ich "x" durch "b" (nicht "a") ersetzt habe. In Zeile 10 habe ich die universelle Eliminierung in Zeile 9 verwendet und "y" durch "a" (nicht "b") ersetzt.

Um die Negation in Zeile 15 einzuführen, habe ich in Zeile 11 „Sba“ angenommen, in Zeile 12 die Biconditional eliminiert, in Zeile 13 die Konjunktion eliminiert und in Zeile 14 einen Widerspruch abgeleitet. Dieser Widerspruch erlaubte mir, „¬Sba“ in Zeile abzuleiten fünfzehn.

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/