= Solution
Under the same scope convention, \b[$g(t,z)$ is not <free for substitution> for $y$]. The occurrence of $y$ inside $Q(f(x,y),f(z,z))$ is free but lies under $\exists t$, so its replacement would capture the new $t$. Rename this binder to fresh $s$. Substitute only for the free $y$ occurrences in the first conjunct:
$$
\boxed{\forall x\left(P(x,g(t,z),z)\lor
\exists s\left(Q(z,s)\land
Q\bigl(f(x,g(t,z)),f(z,z)\bigr)\right)\right)
\land\exists y\,Q(y,y).}
$$
The two occurrences of $y$ in the final conjunct are <bound variables> and remain unchanged. The inserted $t,z$ remain free.
If instead one gives the printed $\exists t$ only the scope $Q(z,t)$, this part's free-for-substitution answer becomes \b[yes], because neither free $y$ occurrence then lies under that binder. Under that alternative parsing, the result is explicitly
$$
\forall x\left(P(x,g(t,z),z)\lor
\left((\exists t\,Q(z,t))\land Q(f(x,g(t,z)),f(z,z))\right)\right)
\land\exists y\,Q(y,y).
$$
The narrower reading does not change the negative answer in (1): its occurrence of $z$ inside $Q(z,t)$ still requires renaming that binder before substitution. The broad-scope answers above give a single consistent parsing across the paper.
Back to article page
