Segundo parcial 2014 Ejer 3-b

Re: Segundo parcial 2014 Ejer 3-b

de Romina Romero - InCo -
Número de respuestas: 0

Sí.

¿Cómo se prueba un existencial? Hay que dar el testigo.

Si observamos los similitudes entre las premisas y la conclusión, vemos que vamos a precisar la sustitución [g(x)/y].

 \infer[I_\exists]{(\exists y)(P(x,y) \land \lnot y =' f(x))}{P(x,g(x)) \land \lnot g(x) =' f(x)} .

Luego se puede usar una  I_\land ; una  E_\forall para el subárbol izquierdo con la hip. 1 y hay que usar la hipótesis que genera la  E_\exists de la hip. 2  para el subárbol derecho.

El tema es dónde meter la  E_\exists para que cumpla con las restricciones.

Tip (general): hacer las  E_\exists lo más abajo posible.

Acá lo podríamos usar para probar bottom.

Saludos