Wie würde man beim Beweis der folgenden Aussage in der Prädikatenlogik vorgehen?

Sie können es beweisen, indem Sie eine negierte Instanz annehmen und einen Widerspruch beweisen:

{1} 1. ~((Fa → Ga) ∨ (Ga → Fa)) Angenommen.
{1} 2. ~(Fa → Ga) & ~(Ga → Fa) 1 DM
{1} 3. ~(Fa → Ga) 2 &E
{1} 4. ~(~Fa ∨ Ga) 3 MI
{1} 5. Fa & ~Ga 4 DM
{1} 6. Fa 5 &E
{1} 7. ~(Ga → Fa) 2 &E
{1} 8. ~(~Ga ∨ Fa) 7 MI                        
{1} 9. Ga & ~Fa 8 DM
{1} 10. ~Fa 9 &E
{1} 11. Fa & ~Fa 6,10 &I
- 12. ~~((Fa → Ga) ∨ (Ga → Fa)) 1,11 RAA
- 13. (Fa → Ga) ∨ (Ga → Fa) 12 DNE
- 14. ∀x[(Fx → Gx) ∨ (Gx → Fx)] 13 UI

Hier ist eine andere Version, die sich nicht auf Identitäten wie DeMorgans Gesetz stützt:

{1} 1. ~((Fa → Ga) ∨ (Ga → Fa)) Angenommen.
{2} 2. Fa → Ga Angenommen.
{2} 3. (Fa → Ga) ∨ (Ga → Fa) 2 ∨I
{1,2} 4. ⊥ 1,3 &I
{1} 5. ~(Fa → Ga) 2,4 RAA
{6} 6. Ga → Fa Angenommen.
{6} 7. (Fa → Ga) ∨ (Ga → Fa) 6 ∨I
{1,6} 8. ⊥ 1,7 &I
{1} 9. ~(Ga → Fa) 6,8 RAA
{10} 10. Fa-Annahme.
{11} 11. Ga Annahme.
{10,11} 12. Fa & Ga Annahme.
{10,11} 13. Ga12 &E
{11} 14. Fa → Ga 10,13 CP
{1,11} 15. ⊥ 5,14 RAA
{1} 16. ~Ga 10,15 RAA
{17} 17. ~Fa Annahme.
{1,17} 18. ~Fa & ~Ga 16,17 &I
{1,17} 19. ~Ga18 &E
{1} 20. ~Fa → ~Ga 17,19 KP
{11} 21. ~~Ga 11 DNI
{1,11} 22. ~~Fa 20,21 MT
{1,11} 23. Fa 22 DNE
{1} 24. Ga → Fa 11,23 KP
{1} 25. ⊥ 9,24 &I
- 26. ~~((Fa → Ga) ∨ (Ga → Fa)) 1,25 RAA
- 27. (Fa → Ga) ∨ (Ga → Fa) 26 DNE
- 28. ∀x[(Fx → Gx) ∨ (Gx → Fx)] 27 UI

Der folgende Beweis verwendet das Gesetz der ausgeschlossenen Mitte (LEM) und nicht die von user3017 verwendete reductio ad absurdum (RAA) .

Da die Konklusion eine prämissenlose Disjunktion ist und „Gx“ in beiden Disjunkten vorkommt, habe ich versucht, einen Beweis aus der Tautologie „Ga ∨ ¬Ga“ zu konstruieren.

In jedem Fall habe ich die bedingte Einführung (→I) in den Zeilen 4 und 10 verwendet. Dann habe ich die Disjunktionseinführung (∨I) verwendet, um für beide Fälle in den Zeilen 5 und 11 das gleiche Ergebnis zu erhalten.

Im ersten Fall habe ich die Wiederholung (R) verwendet, um Zeile 1 in Zeile 3 zu kopieren.

Im zweiten Fall habe ich die Explosion (X) verwendet, um die gewünschte Konsequenz (Fa) in Zeile 9 zu erhalten.

Das gleiche Ergebnis für beide Fälle zu erhalten, ermöglichte es mir, die Unterbeweise für diese Fälle mit dem Gesetz des ausgeschlossenen Dritten (LEM) in Zeile 11 zu schließen.

In Zeile 12 habe ich einen universellen Quantor eingeführt, um den Beweis zu vervollständigen.

Weitere Informationen zu diesen Regeln finden Sie in forall x: Calgary Remix .

---

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