Segundo parcial 2008, Ejercicio 3 parte b

Segundo parcial 2008, Ejercicio 3 parte b

de Veronica Viviana Pintos Fernandez -
Número de respuestas: 4

Hola quería saber si la siguiente derivación es correcta:

 

Muchas gracias,

Verónica.

 

Adjunto Parcial 2008 ejer 3 b.png
En respuesta a Veronica Viviana Pintos Fernandez

Re: Segundo parcial 2008, Ejercicio 3 parte b

de Luis Sierra -
¿qué dudas te genera?

luis
En respuesta a Luis Sierra

Re: Segundo parcial 2008, Ejercicio 3 parte b

de Veronica Viviana Pintos Fernandez -

Cuando introduzco los existe, por qué puedo sustituir una sola de las x y luego el otro cambio con la otra introducción del existe..  

En respuesta a Veronica Viviana Pintos Fernandez

Re: Segundo parcial 2008, Ejercicio 3 parte b

de Luis Sierra -
la regla de intro del existe te dice cómo construir una prueba de (Ez) phi(z) a partir de una prueba de phi(t). siendo más prolijo con la notación de sustitución, te dice cómo construir una prueba de (Ez) phi[z/u] a partir de una prueba de phi[t/u].

en el caso de la primera introducción del existe, tú tienes una prueba de w=w /\ w=w, y construyes una prueba de (Ez) (w=w /\ w=z). tu confusión, supongo, viene de creer que lo de abajo es (Ez) ((w=w /\ w=w)[z/w]), lo que claramente no es, y puede explicar tu fragmento "puedo sustituir una sola de las x". pero esto NO es lo que dice la regla.

lo que dice la regla es que la conclusión es de la forma (Ez) phi[z/u]. o sea, phi es la fórmula w=w /\ w=u;
sustitución en la que se cambian TODAS las u.

parafraseando la regla: a partir de una prueba cuya conclusión es w=w /\ w=w (o sea, phi[t/u] con t=w), obtenés una nueva prueba cuya conclusión es (Ez)(w=w /\ w=z) (o sea, (Ez) phi[z/u])

luis