= Solution
Use broad scope up to the enclosing parenthesis, consistent with (c). Thus the first conjunct is read as
$$
\forall x\left(P(x,y,z)\lor
\exists t\bigl(Q(z,t)\land Q(f(x,y),f(z,z))\bigr)\right).
$$
\b[$f(u,t)$ is not <free for substitution> for $z$.] The free occurrence of $z$ in $Q(z,t)$ lies under $\exists t$; inserting $f(u,t)$ there would capture its $t$. Rename that <bound variable> to a fresh $s$ first, using <alpha equivalence>. The <capture-avoiding first-order substitution> is then
$$
\boxed{\forall x\left(P(x,y,f(u,t))\lor
\exists s\left(Q(f(u,t),s)\land
Q\bigl(f(x,y),f(f(u,t),f(u,t))\bigr)\right)\right)
\land\exists y\,Q(y,y).}
$$
Every occurrence of $z$ in the original formula is free, so all four are replaced. The variable $t$ introduced by the term remains free, and the final $\exists y\,Q(y,y)$ is unchanged.
Back to article page
