¿Alguna solución para probar (∀x)(∃y)(Fx & Gy) ⊢ (∃y)(∀x)(Fx & Gy) con deducción natural?

Al principio, veamos en qué casos la primera fórmula es verdadera. Dado que la conjunción requiere que ambos operandos sean verdaderos, sabemos (por simplificación):

(∀x)(Fx)

Esto significa

Fx ⇔ 1

Ahora, dado que Fx siempre es cierto, obtenemos

(Fx y Gy) ⇔ (1 y Gy) ⇔ (Gy)

y

(∀x)(∃y)(Fx y Gy) ⇔ (∃y)(Gy)

así como también

(∃y)(∀x)(Fx y Gy) ⇔ (∃y)(Gy)

Por lo tanto

(∀x)(∃y)(Fx y Gy) ⇔ (∃y)(∀x)(Fx y Gy)

La deducibilidad se sigue de la equivalencia (pero no necesariamente lo contrario):

(∀x)(∃y)(Fx y Gy) ⊢ (∃y)(∀x)(Fx y Gy)

Esta es una ilustración del hecho de que, si todos los predicados toman un solo argumento (es decir, F(x), G(y) ), esto puede reducirse a un problema de lógica proposicional .

Si desea hacerlo paso a paso, solo necesita las reglas de "irrelevancia": el alcance de un cuantificador no necesita incluir ningún conjunto que no use la variable.

(∀x)(∃y)(Fx & Gy) ⊢ Cuantificador irrelevante

(∀x)(Fx & (∃y) Gy) ⊢ Cuantificador irrelevante

(∀x) Fx & (∃y) Gy ⊢ Cuantificador irrelevante (nótese que en realidad es una expresión oracional )

(∃y)((∀x) Fx & Gy) ⊢ Cuantificador irrelevante

(∃y)(∀x)(Fx y Gy)

Aquí hay una manera de probar el resultado:

Intento una prueba indirecta (IP) negando lo que quiero mostrar en la línea 2. En la línea 23 finalmente llego a una contradicción (⊥). En el proceso de llegar allí, utilizo la regla de conversión de cuantificadores (CQ), la regla de De Morgan (DeM) y el silogismo disyuntivo (DS) junto con las reglas de introducción y eliminación.

Para obtener más información sobre estas reglas asociadas con el comprobador de pruebas que utilicé, consulte forall x: Calgary Remix .

Referencia

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/

Puede utilizar las reglas de Introducción y Eliminación para probar la 'irrelevancia del cuantificador' en universos no vacíos.

|_ Ɐx Ǝy (Fx & Gy)
|  |_ [a]
|  |  Ǝy (Fa & Gy)
|  |  |_ [b] Fa & Gb
|  |  |  Fa
|  |  Fa
|  Ɐx Fx
|  |_ [a]
|  |  Ǝy (Fa & Gy)
|  |  |_ [b] Fa & Gb
|  |  |  Gb
|  |  |  |_ [c]
|  |  |  |  Fc
|  |  |  |  Fc & Gb
|  |  |  Ɐx (Fx & Gb)
|  |  Ǝy Ɐx (Fx & Gy)
|  Ǝy Ɐx (Fx & Gy)

Y lo mismo para lo contrario.