Sematic aspects of substitution

1. Introduction

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 $L$ -structure.

2. The propositions

The first of our two propositions discusses two substitutions that may be different but which are semantically the same.

Proposition.

Let $M$ be an $L$ -structure, $a : {VAR}_{L} \to M$ an assignment, and $T, S$ be substitutions with $V = dom (S) = dom (T)$ . Then if $a (T (v)) = a (S (v))$ for all $v \in V$ we have $a (T (t)) = a (S (t))$ and $a (T (θ)) = a (S (θ))$ for all terms and formulas $t, θ$ such that the substitutions $T (θ), S (θ)$ are both valid.

Intutively, this proposition works because $S$ and $T$ are the same substitution semantically. That is, $a (T (v)) = a (S (v))$ for all $v$ . Unfortunately, it isn't quite so simple as this since $T (v)$ and $S (v)$ might use quite different variables to obtain the same value $a (T (v)) = a (S (v))$ , so we need to be careful of this point. Fortunately we are told that the substitutions $T (θ)$ , $S (θ)$ are valid. This means that whatever variables are used in $T (v)$ and $S (v)$ they will not be in the scope of any existing quantifiers and so the values of these variables as given by the assignment $a$ will be unchanged. So the idea is clear, but this technical consideration makes the induction hypothesis rather more complicated!

Proof.

By induction on terms and formulas $t, θ$ . Our induction hypothesis is that for all terms and formulas $θ$ with construction sequence of length at most $n$ , all assignments $a$ and all substitutions $S, T$ with the same domain and same forbidden set of variables, if $a (S (w)) = a (T (w))$ for each $w \in dom (S) = dom (T)$ such that neither $S (w), T (w)$ contain any variable in $(S') = (T')$ and $T (θ), S (θ)$ are both valid then $a (T (θ)) = a (S (θ))$ .

The base case of the induction is when $θ$ is a variable $v$ or a constant symbol $c$ or $⊤$ or $⊥$ . The first of these is covered by the assumptions of the proposition. For if $a$ is given with $a (S (w)) = a (T (w))$ for all $w \in dom (S) = dom (T)$ such that neither $S (w), T (w)$ contain any variable in $(S') = (T')$ , then either $S (v) = T (v) = v$ in which case there is nothing to prove, or else $v \in dom (S) = dom (T)$ and neither $S (v)$ nor $T (v)$ contain any forbidden variable (since the substitution is valid) so the assumption applies giving $a (S (v)) = a (T (v))$ . The cases of $c$ , $⊤$ 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 $v ψ$ and $a$ is an assignment. Then let $x \in M$ be arbitrary and $b = a [x / v]$ . If $v \in dom (S) = dom (T)$ then let $S'$ be the restriction substitution with $dom (S') = dom (S) ∖ \{v\}$ and $(S') = (S) \cup \{v\}$ and let $T'$ be the restriction substitution with $dom (T') = dom (T) ∖ \{v\}$ and $(T') = (T) \cup \{v\}$ . Else $v \notin dom (S)$ and we let $S'$ be the substitution with $dom (S') = dom (S)$ and $(S') = (S) \cup \{v\}$ and $T'$ with $dom (T') = dom (T)$ and $(T') = (T) \cup \{v\}$ .

We now examine our assignment $b$ and the substitutions $S'$ and $T'$ . Clearly we still have $b (S' (w)) = b (T' (w))$ for each $w \in dom (S') = dom (T')$ such that neither $S' (w), T' (w)$ contain any variable in $(S') = (T')$ . This means by induction that $b (S' (ψ)) = b (T' (ψ))$ . Hence as $x$ is arbitrary, $a (S (∃ v ψ)) = a (T (∃ v ψ))$ , 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 $v$ is renamed to $u$ : this renaming is valid if the formula it is being applied to does not already have any free occurences of $u$ and the substitution $v \mapsto u$ is valid.

Proposition.

Let $M$ be an $L$ -structure, $a : {VAR}_{L} \to M$ an assignment, $u, v$ variables of $L$ and $ϕ$ a formula that does not contain any free occurrences of $u$ . Let $S$ be the substitution $v \mapsto u$ , and assume $S (ϕ)$ is valid. Then for any $x$ in $M$ we have $a [x / v] (ϕ) = a [x / u] (S (ϕ))$ .

Proof.

By induction again. We fix $v, u$ and $M$ . The induction hypthesis is the remaining proposition, i.e. the rather weighty statement $H (n)$ following.

whenever $a : {VAR}_{L} \to M$ is an assignment, $ϕ$ a term or formula constructed in at most $n$ steps that does not contain any free occurrences of $u$ and $S$ the substitution $v \mapsto u$ with some or no forbidden variables, and assume $S (ϕ)$ is valid. Then for any $x$ in $M$ we have $a [x / v] (ϕ) = a [x / u] (S (ϕ))$ .

Given this, the induction step in all cases is straightforward.