Cómo probar '∃xP(x)' a partir de '¬∀x(P(x)→Q(x))'

¿Cómo sería una prueba formal de Fitch para esto?

Me dan ¬∀x(P(x)→Q(x)), y necesito derivar ∃xP(x) de él.

Empecé con esto, pero no sé si estoy haciendo lo correcto y adónde ir desde allí:

ingrese la descripción de la imagen aquí

EDITAR: Lo hizo (ver respuesta)

Hasta ahora no hay respuestas escritas en inglés. ¿No es el quid de la cuestión que si no hubiera $x$ tal que $P(x)$, entonces $P(x)$ sería falso para todos los $x$ y por lo tanto implicaría absolutamente cualquier cosa?

Respuestas (4)

¡Resuelto! Me di cuenta de que no iba a ninguna parte al asumir lo contrario de lo que me dieron como premisa... Obviamente tenía que asumir lo contrario de lo que estaba tratando de probar:

ingrese la descripción de la imagen aquí

En efecto. Tienes una solución correcta. Ahora puede aceptar su propia respuesta para cerrar esta pregunta.

1) ¬∀x(P(x) → Q(x)) --- premisa

2) ¬∃xP(x) --- asumido [a]

3) P(x) --- asumido [b]

4) ∃xP(x) --- de 3) por ∃ -introducción

5) ⊥ --- contradicción: de 2) y 4)

6) Q(x) --- de 5) por ⊥ -elim

7) P(x) → Q(x) --- de 3) y 6) por → -intro, descargando [b]

8) ∀x(P(x) → Q(x)) --- de 7) por ∀ -introducción

9) ⊥ --- contradicción: de 1) y 8)

10) ∃xP(x) --- de 2) por Doble Negación (o ¬ -elim ), descargando [a].

La siguiente prueba es la misma que la de Mauro ALLEGRANZA pero usa el verificador de prueba estilo Fitch de Klement. Las descripciones de las reglas están en forallx . Ambos están disponibles en línea y se enumeran a continuación. Pueden ayudar como material complementario a lo que está utilizando actualmente.

Es posible que se le solicite en su verificador de pruebas que represente las contradicciones como conjunciones de declaraciones contradictorias. Este verificador de prueba solo requiere anotar la contradicción como "⊥" y enumerar las líneas contradictorias como hice en las líneas 5 y 9.

ingrese la descripción de la imagen aquí

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/

Logré hacerlo, pero mi resultado es ligeramente diferente al tuyo. Probé el tuyo por curiosidad, y no funciona en el programa de Fitch que tengo. ¡Estoy desconcertado por el hecho de que su verificador de prueba le permitió exportar la suposición temporal 'a' fuera de su subprueba!
@ 35308 Podría ver esa subdemostración (líneas 3-6) como si dijera lo mismo que la declaración condicional en la línea 7 "Pa> Qa". Dada la suposición Pa, puedo derivar Qa con lo que está disponible (a saber, la línea 2). La subprueba solo mostró cómo se hizo eso y el verificador de pruebas requirió que mostrara eso antes de usar la línea 7.
El problema es que realmente no debería permitirse introducir un nuevo término libre 'a' sin plantear un nuevo contexto para aislarlo.

Pr. ~∀x(P(x)->Q(x))

2. ∃x~(P(x)->Q(x)) ~ Salida universal Pr.

3. ~(P(a)->Q(a)) Salida existencial (x/a) 2

4. P(a)&~Q(a) ~ salida condicional 3

5. P(a) Conjunción fuera 4

6. ∃xP(x) Existencial en 5

Cómo probar '∃xP(x)' a partir de '¬∀x(P(x)→Q(x))'
RespuestasAquíPolítica de privacidad1y, 2v