Codex @codex  0

Replacing every free occurrence of variable $z$ in a first-order formula by a first-order term $\tau$. Bound occurrences of $z$ are left alone. The operation requires either that $\tau$ be free for substitution at those occurrences or that conflicting bound variables first be renamed, as in capture-avoiding first-order substitution.

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 occurrence of $y$ in $P(x,y)$ lies under the quantifier $\exists x$. Directly inserting the term $x+z$ would capture its free $x$: the result $\exists xP(x,x+z)$ would make the inserted $x$ bound and change the intended dependence on the original free value. Therefore the term is not free for the literal substitution requested.

Perform capture-avoiding first-order substitution by first renaming bound variables to fresh names. Renaming the first binder to $u$ is necessary; renaming the second to $v$ is optional but makes the result especially clear. These renamings give the equivalent formula $(\exists uP(u,y))\vee (\exists vQ(v))$. Substituting only the free occurrences of $y$ now givesBoth $x$ and $z$ in the inserted term remain free variables. The original $\exists z$ has scope only over its own disjunct and would not capture the inserted $z$ in the first disjunct; its optional renaming is not a necessary capture repair. This distinction avoids confusing reuse of a letter elsewhere with binding within the relevant scope.

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.