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 / 1

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.