This web page discusses semantic aspects of substitution in first-order logic. In particular we explore the connections between substitutions and assignments of variables to values in an -structure.
The first of our two propositions discusses two substitutions that may be different but which are semantically the same.
Let be an -structure, an assignment, and be substitutions with . Then if for all we have and for all terms and formulas such that the substitutions are both valid.
Intutively, this proposition works because and
same substitution semantically. That is,
for all . Unfortunately, it isn't quite so simple as this
since and might use quite different variables to obtain
the same value , so we need to be careful of this point.
Fortunately we are told that the substitutions ,
are valid. This means that whatever variables are used in
and they will not be in the scope of any existing quantifiers
and so the values of these variables as given by the assignment
will be unchanged. So the idea is clear, but this technical consideration
makes the induction hypothesis rather more complicated!
By induction on terms and formulas . Our induction hypothesis is that for all terms and formulas with construction sequence of length at most , all assignments and all substitutions with the same domain and same forbidden set of variables, if for each such that neither contain any variable in and are both valid then .
The base case of the induction is when is a variable or a constant symbol or or . The first of these is covered by the assumptions of the proposition. For if is given with for all such that neither contain any variable in , then either in which case there is nothing to prove, or else and neither nor contain any forbidden variable (since the substitution is valid) so the assumption applies giving . The cases of , and are easy.
The induction steps for the various ways of building a more complex term or formula from simpler ones are mostly straightforward. This is because their clauses defining substitition don't change the domains or forbidden variables for substitutions. The only awkward steps are those for the quantifiers and . We do the case of here leaving the other as an exercise.
Suppose is and is an assignment. Then let be arbitrary and . If then let be the restriction substitution with and and let be the restriction substitution with and . Else and we let be the substitution with and and with and .
We now examine our assignment and the substitutions and . Clearly we still have for each such that neither contain any variable in . This means by induction that . Hence as is arbitrary, , as required. The case for ∀ is similar.
The second of our two propositions says that renaming a variable in a formula does not affect the truth of that formula provided we remember to modify the assignment in a similar way. Here a variable is renamed to : this renaming is valid if the formula it is being applied to does not already have any free occurences of and the substitution is valid.
Let be an -structure, an assignment, variables of and a formula that does not contain any free occurrences of . Let be the substitution , and assume is valid. Then for any in we have .
By induction again. We fix and . The induction hypthesis is the remaining proposition, i.e. the rather weighty statement following.
Given this, the induction step in all cases is straightforward.