I am given the formula: $\Psi={{\forall}}x\exists y\left(\exists z{{\forall}}xR\left(x,z,w\right)\land\exists wP\left(w,x,z\right)\right)$ for which I'm required to determine if a given simultaneous subtitution $\Psi\left\{ \frac{t_{1}}{x},\frac{t_{2}}{y},\frac{t_{3}}{z},\frac{t_{4}}{w}\right\} $ is valid.
In the reference I have, which does not include explainations, the variables $x,w$ are renamed in the following manner: $\Psi={{\forall}}x\exists y\left(\exists z{{\forall}}\mathbf{u}R\left(\mathbf{u},z,w\right)\land\exists \mathbf{v}P\left(\mathbf{v},x,z\right)\right)$ and then, the general subtitution results in: $\Psi\left\{ \frac{t_{1}}{x},\frac{t_{2}}{y},\frac{t_{3}}{z},\frac{t_{4}}{w}\right\}={{\forall}}x\exists y\left(\exists z{{\forall}}uR\left(u,t_3,t_4\right)\land\exists vP\left(v,t_1,t_3\right)\right)$.
I'm trying to explain myself why it was done this way:
- $x$ is renamed to $u$ in the first term of the conjunction simply because it is already bounded in the outer scope - so the nested bounding in this term is useless, and in order to make it effective, a "new" variable $u$ must be introduced.
- $w$ is renamed to $v$ in the second term of the conjunction because it is free in the first term, so a future subtitution of $w$ could be harmful, otherwise.
- The subtitution - the only thing I don't understand is why $t_1$ subtitutes $x$ in the second term of the conjunction. $x$ is bounded in the outer scope, and thus affects this term, so it seems to me it shouldn't be subtituted. But I guess my understanding lacks something.
Are my explainations make sense? Can someone please explain me the 3rd point? Would appreciate any help.