¿Ayuda con la prueba bicondicional de Fitch?

Pista: Plantea siempre un contexto con lo que hay que descargar para deducir el objetivo. Por lo tanto, cuando pretenda introducir un cuantificador universal , debe comenzar la subdemostración asumiendo un término arbitrario . En este caso, dos veces.

Asuma los términos arbitrarios, [a] y [b], de alguna manera derive el bicondicional (pista: se involucrarán varias eliminaciones universales), luego introduzca dos universales.

|  Ɐ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
■

Rellenar en el medio no debe ser demasiado difícil. Parece que su verificador requiere una introducción bicondicional para verse así:

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

Estoy usando un verificador de pruebas diferente, pero tal vez ver cómo se alcanza el objetivo aquí puede ayudar a que esto funcione con el verificador de pruebas que está usando.

Este comprobador de pruebas tiene una forma diferente de aceptar fórmulas bien formadas. Reemplacé "Indiff" con "I".

También noté que el objetivo era simplemente "∀x∀y(Ixy↔Iyx)", es decir, "∀x∀y(Indiff(x,y) ↔ Indiff(y,x)", y tenías como quinto premisa "∀x∀y(Ixy → Iyx)", es decir, "∀x∀y(Indiff(x,y) → Indiff(y,x)". Solo necesitaba usar esa premisa y por eso no incluí los demás.

Para obtener un bicondicional, tuve que comenzar dos subpruebas condicionales. La primera asumí "Iab" en la línea 2 y llegué a la meta de esa subprueba, "Iba", en la línea 5. La segunda subprueba fui en dirección opuesta y asumí "Iba" en la línea 6 y llegué a la meta "Iab " en la línea 9. Dentro de cada subdemostración eliminé el cuantificador universal, pero usando nombres para las variables "x" e "y" que me ayudaron a llegar a la conclusión.

Cuando introduje el bicondicional en la línea 10, esto descartó las suposiciones de las líneas 2 y 6.

Una descripción de las reglas está en forallx (enlace más abajo). Para eliminación universal (∀E) ver páginas 239-240. Para eliminación condicional (→E) ver páginas 103-104. Para la introducción bicondicional (↔I) véanse las páginas 111-112. Para introducción universal (∀I) ver páginas 243-246.

---

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/