Definition of substitution in FOL formulas

Question

Can someone please confirm that the following definition of substitution of terms in FOL formulas is correct and complete.

For any formula $\phi$, the formula $\phi[t/x]$ is the formula $\phi$ with all occurrences of the term $x$ replaced with the term $t$, with the following conditions:

• $x$ must be free in $\phi$
• The term $t$ must be chosen so that any variables within $t$ do not become bound by any quantifier within $\phi$

Is this sufficiently precise, and are there any other conditions/restrictions?

Answer 1

The two bullets are a separate issue from substitution. You can substitute any term for any variable in any formula (although only free occurrences will change). The restrictions in the two bullets come from various inference rules, where only certain substitutions are acceptable.

Consider:

• $\phi_1 \equiv x = y$
• $\phi_2 \equiv x = 0 \to (\forall x)[x = 0]$ as mentioned by Mauro Allegranza in the comments

Then:

• $\phi_1[y/x] \equiv y = y$
• $\phi_2[y/x] \equiv y = 0 \to (\forall x)[x = 0]$

The simplest definition is just "$\phi[t/x]$ is the result of replacing every free occurrence of $x$ in $\phi$ with $t$. An occurrence of $x$ is a free occurrence if it does not appear in the scope of a quantifier $(\forall x)$ or $(\exists x)$."