Hola estaba haciendo esta parte del ejercicio y me parece que encontre un atajo para resolverlo sin usar PIP. En el libro hay un lema: "Lemma 3.3.13 t is free for x in ϕ ⇔ the variables of t in ϕ[t/x] are not bound by a quantifier". Si la letra del ejercicio me dice que "x1 está libre para y en φ" y le aplico el lema obtengo que x1 no esta ligada a ningun cuantificador y entonces ambas funciones deben dar 0 en todos los casos.
Esta correta esta respuesta?
Hola Felipe:
Ese lema del libro que mencionás está formulado de una manera algo confusa y puede ser interpretado de una manera equivocada (que es lo que pasa en tu planteo).
En lugar de ese lemma, en el curso admitimos una noción intuitiva algo informal que dice lo siguiente:
Hacemos énfasis en nuevas ocurrencias ligadas.
Esto es porque en φ pueden existir ocurencias ligadas de x que van a seguir apareciendo luego de la sustitución, esto es en φ[t/x].
Por ejemplo:
Se cumple que que t está libre para x₂ en φ.
Esto no significa que x₁ no aparezca ligada en φ[t/x] como parece decir el lema citado:
t is free for x in ϕ ⇔ the variables of t in ϕ[t/x] are not bound by a quantifier
En φ[t/x₂] hay una ocurrencia ligada de x₁ pero no es nueva porque ya estaba en φ antes de la sustitución.
Por lo tanto, no es correcto el planteo que vos hacés.
Espero que aclare tu duda, si no volvé a preguntar.
saludos