Parciales

Hola.

La regla de $I_\exists$ dice:

$\infer[I_\exists]{(\exists y) \alpha}{\infer*{\alpha[t/y]}{ }}$

Para poder realizar la sustitución: $t$ debe estar libre para $y$ en $\alpha$.

En este caso:

• $t = g(x)$
• $\alpha = P(x,y) \land y =' g(x)$
  

Por tanto, para poder realizar la sustitución: $g(x)$ debe estar libre para $y$ en $P(x,y) \land y =' g(x)$.

Mirando la definición de término libre para variable, vemos que esto se cumple. (Observar que si la fórmula no tiene cuantificadores, los términos siempre están libres para las variables).

La derivación está bien.

Saludos