Teórico de Deducción Natural - Lógica de Primer Orden

Hola.
La regla de introducción del existe dice:

$\infer[I\exists]{\hline(\exists x )\varphi}{ D \\ ...\\ \varphi[t/x]}$

Recordemos que no importa cómo se construya la derivación, una vez terminada, siempre se lee desde las hojas hasta la raíz (de arriba hacia abajo).

Entonces el punto es que la regla, no hace una sustitución, sino que cuando se avanza hacia la conclusión se deshace una sustitución.

De esta forma, $\varphi$ que está al lado del existe, es cualquier fórmula tal que si sustituimos x por t, nos de la fórmula de arriba de la regla. Esto hace que yo pueda (des)sustituir lo que me conviene.

Esto hace que:

$\infer[I\exists] {\hline (\exists z)\, f(x) =' z}{f(x) =' f(x)}$ Es correcta porque $(f(x) =' z)[f(x)/z] = (f(x)='f(x))$.

$\infer[I\exists] {\hline (\exists z)\, z =' f(x)}{f(x) =' f(x)}$ Es correcta porque $(z=' f(x))[f(x)/z] = (f(x)='f(x))$.

$\infer[I\exists] {\hline (\exists z)\, z =' f(x)}{f(x) =' f(x)}$ Es correcta porque $(z=' z)[f(x)/z] = (f(x)='f(x))$.

Espero que quede claro. Si no, pregunten de nuevo !!!!

Saludos