prueba de lenguaje y lógica capítulo 13 pregunta 49 Ayuda

El final no debe ser fangoso. El final es donde comienzas, luego avanzas.

Mire dónde comienza y hacia dónde desea ir.

|  Ex P(x)                         Premise
|_ Ax Ay ((P(x) ^ P(y)) -> x=y)    Premise
|   :
|   :
|  Ex (P(x) ^ Ay (P(y) -> y=x)     ...

Claramente tienes que introducir ese existencial, y el mejor candidato es eliminando la premisa existencial.

|  Ex P(x)                         Premise
|_ Ax Ay ((P(x) ^ P(y)) -> x=y)    Premise
|  |_ [a] P(a)                     Assumption
|  |   :
|  |   :
|  |  P(a) ^ Ay (P(y) -> y=a)      ...
|  |  Ex (P(x) ^ Ay (P(y) -> y=x)) Existential Introduction
|  Ex (P(x) ^ Ay (P(y) -> y=x))    Existential Elimination

Ahora tienes un universal para eliminar (dos veces) y uno para introducir; y también una conjunción.

|  Ex P(x)                            Premise
|_ Ax Ay ((P(x) ^ P(y)) -> x=y)       Premise
|  |_ [a] P(a)                        Assumption
|  |  |_ [b]                          Assumption
|  |  |  |_ P(b)                      Assumption
|  |  |  |  Ay ((P(a) ^ P(y)) -> a=y) Universal Elimination
|  |  |  |  (P(a) ^ P(b)) -> a=b      Universal Elimination
|  |  |  |   :
|  |  |  |   :
|  |  |  |  b=a                       ...
|  |  |  P(b) -> b=a                  Conditional Introduction
|  |  Ay (P(y) -> y=a)                Universal Introduction
|  |  P(a) ^ Ay (P(y) -> y=a)         Conjunction Introduction
|  |  Ex (P(x) ^ Ay (P(y) -> y=x))    Existential Introduction
|  Ex (P(x) ^ Ay (P(y) -> y=x))       Existential Elimination

Estoy seguro de que puedes completar. Agregaré una pista: la Introducción a la Igualdad dice b=b.

La siguiente prueba es similar a la sugerida por Graham Kemp. Lo que es diferente es que estoy usando las primeras ocho líneas de la prueba del OP, mostrando el uso de un verificador de prueba diferente y ofreciendo una forma de entender las reglas de identidad.

En esta prueba observe que a = b en la línea 8 se convierte en b = a en la línea 10. Para llegar a este resultado tengo que introducir una identidad en la línea 9, a = a . No necesito hacer referencia a ninguna línea para presentar esta identidad. Tener esta línea me da una línea en la que puedo hacer una sustitución cuando uso la eliminación de identidad.

La eliminación de identidad es tan simple que es fácil pasar por alto lo que está pasando. Así es como lo describe Frederic Fitch (14.3, página 81):

Supongamos que (...a...) es cualquier proposición que menciona a , y que (...b...) es el resultado de sustituir b por a en uno o más lugares en (...a... ) . De acuerdo con esta regla [de eliminación de identidad], podemos inferir (...b...) de (...a...) y [a = b] .

En la demostración anterior, la identidad que se necesita para esta regla está en la línea 8, a = b , y la proposición que menciona a en la que sustituiremos b por a es la línea 9, a = a , la misma que introdujimos como una identidad. La línea 9 ahora no se ve como una identidad, sino como una proposición que contiene un . Solo sustituimos la primera a en la línea 9 dejando la otra. Esto nos permite inferir la línea 10: b = a .

---

Referencia

Fitch, FB, Lógica simbólica: una introducción, 1952.

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