¿Cómo se haría para probar la siguiente afirmación en lógica de predicados?

Puede probarlo asumiendo una instancia negada y demostrando una contradicción:

{1} 1. ~((Fa → Ga) ∨ (Ga → Fa)) Suposición.
{1} 2. ~(Fa → Ga) & ~(Ga → Fa) 1 DM
{1} 3. ~(Fa → Ga) 2 &E
{1} 4. ~(~Fa ∨ Ga) 3 MI
{1} 5. Fa y ~Ga 4 DM
{1} 6. Fa 5 y E
{1} 7. ~(Ga → Fa) 2 &E
{1} 8. ~(~Ga ∨ Fa) 7 MI                        
{1} 9. Ga y ~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 IU

Aquí hay otra versión que no se basa en identidades como la ley de DeMorgan:

{1} 1. ~((Fa → Ga) ∨ (Ga → Fa)) Suposición.
{2} 2. Fa → Ga Asunción.
{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 Suposición.
{6} 7. (Fa → Ga) ∨ (Ga → Fa) 6 ∨I
{1,6} 8. ⊥ 1,7 &I
{1} 9. ~(Ga → Fa) 6,8 RAA
{10} 10. Supuesto Fa.
{11} 11. Suposición de Ga.
{10,11} 12. Supuesto Fa & Ga.
{10,11} 13. Ga 12 y E
{11} 14. Fa → Ga 10,13 CP
{1,11} 15. ⊥ 5,14 AAR
{1} 16. ~Ga 10,15 RAA
{17} 17. ~Fa Asunción.
{1,17} 18. ~Fa & ~Ga 16,17 &I
{1,17} 19. ~Ga 18 &E
{1} 20. ~Fa → ~Ga 17,19 CP
{11} 21. ~~Ga 11 DNI
{1,11} 22. ~~Fa 20,21 TM
{1,11} 23. Fa 22 DNE
{1} 24. Ga → Fa 11,23 CP
{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

La siguiente prueba utiliza la ley del tercero excluido (LEM) en lugar de reductio ad absurdum (RAA) utilizada por user3017 .

Como la conclusión es una disyunción sin premisas y "Gx" está en ambas disyunciones, traté de construir una demostración a partir de la tautología "Ga ∨ ¬Ga".

En cada caso usé la introducción condicional (→I) en las líneas 4 y 10. Luego usé la introducción de la disyunción (∨I) para obtener el mismo resultado para ambos casos en las líneas 5 y 11.

En el primer caso usé la reiteración (R) para copiar la línea 1 a la línea 3.

En el segundo caso, usé la explosión (X) para obtener el consecuente deseado (Fa) en la línea 9.

Obtener el mismo resultado para ambos casos me permitió cerrar las subpruebas para estos casos usando la ley del medio excluido (LEM) en la línea 11.

En la línea 12 introduje un cuantificador universal para completar la prueba.

Puede encontrar más información sobre estas reglas en forall x: Calgary Remix .

---

Referencias

Editor y comprobador de pruebas de deducción natural JavaScript/PHP estilo Fitch de Kevin Klement http://proofs.openlogicproject.org/

PD Magnus, Tim Button con adiciones de J. Robert Loftis remezcladas y revisadas por Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, invierno de 2018. http://forallx.openlogicproject.org