This is an old revision of the document!
Substitutions for First-Order Logic
Motivating Example
It is important to be precise about substitutions in first-order logic. For example, we would like to derive from formula formula , denoted that results from substituting a term instead of . For example, from we would like to derive . Consider, however formula \[
\forall x. \exists y. x < y
\] Consider an interpretation in integers. This formula is true in this domain. Now substitute instead of x the term y+1. We obtain \[
\exists y. y + 1 < y
\] This formula is false. We say that the variable in term was captured during substitution. When doing substitution in first-order logic we must avoid variable capture. One way to do this is to rename bound variables. Suppose we want to instantiate the formula with . Then we first rename variables in the formula, obtaining \[
\forall x_1. \exists y_1. x_1 < y_1
\] and then after substitution we obtain , which is a correct consequence of .
Naive and Safe Substitutions
Let be a set of variables (that is, ). A variable substitution is a function where is the set of terms first-order logic.
We define naive substitution recursively, first for terms:
\[\begin{array}{rcl}
subst(\sigma)( x ) &=& \sigma( x ),\ \sigma \mbox{ d{}efined at } x
subst(\sigma)( x ) &=& x,\ \sigma \mbox{ not d{}efined at } x
subst(\sigma)(f(t_1,\ldots,t_n)) &=& f(subst(\sigma)(t_1),\ldots,subst(\sigma)(t_n))
\end{array}\]
and then for formulas: \[\begin{array}{rcl}
nsubst(\sigma)(R(t_1,\ldots,t_n)) &=& R(nsubst(\sigma)(t_1),\ldots,nsubst(\sigma)(t_n)) \\ nsubst(\sigma)(t_1 = t_2) &=& (nsubst(\sigma)(t_1) = nsubst(\sigma)(t_n)) \\ nsubst(\sigma)(\lnot F) &=& \\ nsubst(\sigma)(F_1 \land F_2) &=& \\ nsubst(\sigma)(\forall x.F) &=& \\ nsubst(\sigma)(\exists x.F) &=&
\end{array} \]
Lemma: Let be a variable substitution and a term. Then for every interpretation , \[
e_T(nsubst(\sigma)(t))(I) = e_T(t)(I[x_1 \mapsto e_T(t_1)(I),\ldots, x_n \mapsto e_T(t_n)(I)])
\]
To avoid variable capture, we introduce in addition to a safe substitution, . \[ \begin{array}{rcl}
sfsubst(\sigma)(R(t_1,\ldots,t_n)) &=& R(nsubst(\sigma)(t_1),\ldots,nsubst(\sigma)(t_n)) \\ sfsubst(\sigma)(t_1 = t_2) &=& (nsubst(\sigma)(t_1) = nsubst(\sigma)(t_n)) \\ sfsubst(\sigma)(\lnot F) &=& \\ sfsubst(\sigma)(F_1 \land F_2) &=& \\ sfsubst(\sigma)(\forall x.F) &=& \\ sfsubst(\sigma)(\exists x.F) &=&
\end{array} \]
Lemma: Let be a variable substitution and a term. Then for every interpretation , \[
e_F(sfsubst(\sigma)(F))(I) = e_F(F)(I[x_1 \mapsto e_T(t_1)(I),\ldots, x_n \mapsto e_T(t_n)(I)])
\]
Lemma: .