Substitution

A substitution $S$ is a finite set $\{(x_1/t_1),\dots ,(x_n/t_n)\}$ where:

• $x_1,\dots ,x_n$ are distinct variables (only variables can be substituted)
• $t_1,\dots ,t_n$ are terms (variables, constants, or functional terms)

If we let $S$ be a substitution and $\varphi$ a first order formula, then $S(\varphi )$ is the result of applying the substitution $S$ to $\varphi$.