(a) Let us temporarily call an instance of variable $x$ (or $y$ ) bounded by $\forall z$ iff the instance is within some subformula $\forall z\alpha$ of $\phi$ . Then, every instance of $x$ or $y$ in $\phi$ will become $x$ or $y$ depending on whether it is bounded by $\forall x$ and/or $\forall y$ (for cases). In two of these cases, if a variable is not bounded by $\forall y$ (regardless of whether it is bounded by $\forall x$ or not), it will eventually become $x$ in $(\phi_{y}^{x})_{x}^{y}$ . If the variable is bounded by $\forall y$ , then depending on whether it is bounded by $\forall x$ or not, it will, correspondingly, remain the same as in $\phi$ or become $y$ in $(\phi_{y}^{x})_{x}^{y}$ . Therefore, we have several potential cases when $x$ may become $y$ and $y$ may become $x$ . Based on this, consider $\phi$ equal to $Py\rightarrow\forall yPx$ . Then $(\phi_{y}^{x})_{x}^{y}=Px\rightarrow\forall yPy$ , where a free $x$ turned out to be $y$ and a free $y$ turned out to be $x$ .

Based on this observation, it is clear that if there is no $y$ in $\phi$ then a) no $y$ can become $x$ (no extra $x$ ’s), and b) no $x$ is bounded by $\forall y$ , hence, no $x$ can become $y$ (no missing $x$ ’s). A more formal prove is given in (b).

(b) As suggested we show the statement by induction. For a variable or constant symbol $z\neq y$ , if $z\neq x$ , then $\phi_{y}^{x}=(\phi_{y}^{x})_{x}^{y}=z$ , otherwise $\phi_{y}^{x}=y$ and $(\phi_{y}^{x})_{x}^{y}=x=z$ . For a term $t=f_{i}t_{1}\ldots t_{n}$ that does not contain $y$ , by induction, $(t_{y}^{x})_{x}^{y}=f_{i}((t_{1})_{y}^{x})_{x}^{y}\ldots((t_{n})_{y}^{x})_{x}^{y}=f_{i}t_{1}\ldots t_{n}=t$ . Similarly, for an atomic formula $\phi=Pt_{1}\ldots t_{n}$ that does not contain $y$ , by induction, $(\phi_{y}^{x})_{x}^{y}=P((t_{1})_{y}^{x})_{x}^{y}\ldots((t_{n})_{y}^{x})_{x}^{y}=Pt_{1}\ldots t_{n}=\phi$ (and $x$ is substitutable for $y$ in $\phi_{y}^{x}$ because the latter is an atomic formula as well).

Further, by definition and induction, if $\alpha$ and $\beta$ not containing $y$ are such that $x$ is substitutable for $y$ in $\alpha_{y}^{x}$ and $\beta_{y}^{x}$ , $(\alpha_{y}^{x})_{x}^{y}=\alpha$ and $(\beta_{y}^{x})_{x}^{y}=\beta$ , then a) $(\neg\alpha)_{y}^{x}=\neg\alpha{}_{y}^{x}$ , $x$ is substitutable for $y$ in it, and $((\neg\alpha)_{y}^{x})_{x}^{y}=\neg(\alpha_{y}^{x})_{x}^{y}=\neg\alpha$ , and b) $((\alpha\rightarrow\beta)_{y}^{x})=\alpha_{y}^{x}\rightarrow\beta_{y}^{x}$ , $x$ is substitutable for $y$ in it, and $((\alpha\rightarrow\beta)_{y}^{x})_{x}^{y}=(\alpha_{y}^{x})_{x}^{y}\rightarrow(\beta_{y}^{x})_{x}^{y}=\alpha\rightarrow\beta$ . Moreover, $(\forall x\alpha)_{y}^{x}=\forall x\alpha$ not containing $y$ at all, and $(\forall z\alpha)_{y}^{x}=\forall z\alpha_{y}^{x}$ , $z\notin\{x,y\}$ , $x$ does not occur free, hence, is substitutable for $y$ in it, and $((\forall z\alpha)_{y}^{x})_{x}^{y}=\forall z(\alpha_{y}^{x})_{x}^{y}=\forall z\alpha$ .