= Solution
The occurrence of $y$ in $P(x,y)$ lies under the quantifier $\exists x$. Directly inserting the term $x+z$ would capture its free $x$: the result $\exists x\,P(x,x+z)$ would make the inserted $x$ bound and change the intended dependence on the original free value. Therefore the term is not free for the literal substitution requested.
Perform <capture-avoiding first-order substitution> by first renaming <bound variables> to fresh names. Renaming the first binder to $u$ is necessary; renaming the second to $v$ is optional but makes the result especially clear. These renamings give the equivalent formula $(\exists u\,P(u,y))\lor(\exists v\,Q(v))$. Substituting only the free occurrences of $y$ now gives
$$
\boxed{(\exists u\,P(u,x+z))\lor(\exists v\,Q(v)).}
$$
Both $x$ and $z$ in the inserted term remain <free variables>. The original $\exists z$ has scope only over its own disjunct and would not capture the inserted $z$ in the first disjunct; its optional renaming is not a necessary capture repair. This distinction avoids confusing reuse of a letter elsewhere with binding within the relevant scope.
Back to article page
