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), \mbox{ if $\sigma$ defined at $x$} \\ subst(\sigma)(x) &=& x, \mbox{ if $\sigma$ not defined at $x$} \\ subst(\sigma)(f(t_1,\ldots,t_n)) &=& f(subst(\sigma)(t_1),\ldots,subst(\sigma)(t_n))
\end{array} \] 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) &=&
\]
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: .