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

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.

The term $x+z$ is free for substitution for $z$. The only free occurrence of the target $z$ is in the outside disjunct $y<z$, beyond both quantifier scopes. The occurrences under $\forall z$ are bound variables and are not replaced. Therefore no renaming is required, andThe new $x$ and $z$ in the last disjunct are free. First-order substitution replaces the original free occurrences once; it does not recursively substitute into the inserted term.