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

Use broad scope up to the enclosing parenthesis, consistent with (c). Thus the first conjunct is read as$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 thenEvery 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 yQ(y,y)$ is unchanged.

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.