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:
- Si t está libre para x en φ, entonces φ[t/x] no genera nuevas ocurrencias ligadas.
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:
- φ := (∀x₁) P(x₁) ∧ P(x₂)
- t := f(x₁)
- φ[t/x₂] = (∀x₁) P(x₁) ∧ P(f(x₁))
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