Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof / 8 / f / i / Solution

The term $x+z$ is not free for substitution for $y$. The occurrence of $y$ in $x<y$ is under $\exists x$, which would capture the inserted $x$. The other occurrence, in the outside disjunct $y<z$, has no enclosing quantifier. The inner $\forall z$ does not bind the occurrence of $y$ in its antecedent, so it creates no additional capture at that substitution site.

Rename the bound $x$ to a fresh $u$, then carry out capture-avoiding first-order substitution. The result isThe inserted $z$ in $u<x+z$ remains free because it lies outside the scope of $\forall z$. One may additionally rename that bound $z$ for readability, but it is not necessary for correctness.