First order logic substitution

Question

Let $A \equiv \forall x{.}(\exists y{.}p(x,f(x,y)))\to((\forall x{.}p(x,y))\wedge(\forall x{.}p(y,x)))$

Assume $\theta = \{y\backslash f(x,y)\}$ is a substitution. Calculate $A\theta$ (the application of substitution $θ$ on formula $A$)

I came up with below answer after the substitution. $A\theta \equiv \neg p(x,f(x,f(x,y)))\vee(p(u,f(x,y))∧p(f(x,y),z))$

My problem is the below one.

Give an example that shows : $(\forall x{.}A)\to A\{x\backslash t\}$ would not be universally true for all formulas $A$, if our definition of applying a substitution would not rename bound variables (i.e if for a quantifier Q applying the substitution had been defined as $(Qx{.}A)θ := Qx{.}(Aθ)$ instead.

I am stuck on this question. Some guidance would be appreciated :-)

Answer 1

The final part of the question is quite unclear ...

I think that the issue is about the need to avoid unwanted "capturing" of variables in substitution.

Consider the following example:

$(\forall x \ (\exists y \ (y=x+1))) \to (\exists y \ (y=0+1))$.

It is an arithmetical example of the universally valid axiom schema: $(\forall x \ A)\to A\{x\backslash t\}$, where $A$ is $\exists y \ (y=0+1)$ and $t$ is $0$.

Consider now what happens with $y$ as $t$, i.e. with susbt $\theta = \{ x \backslash y \}$.

We have:

$(\forall x \ (\exists y \ (y=x+1))) \to (\exists y \ (y=y+1))$;

the antecedent is still true in $\mathbb N$ : every natural number has a successor, while the consequent is not : there is no number that is successor of itself.