Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Digital systems, linear algebra and introduction to formal proof / 8 / d / 2 / Solution

Under the same scope convention, $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: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 yes, because neither free $y$ occurrence then lies under that binder. Under that alternative parsing, the result is explicitlyThe 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.