
# 2.6: Two Technical Lemmas


In this section we present two rather technical lemmas that we need to complete the proof of Theorem 2.5.1. The proofs that are involved are not pretty, and if you are the trusting sort, you may want to scan through this section rather quickly. On the other hand, if you come to grips with these results, you will gain a better appreciation for the details of substitutability and assignment functions.

To motivate the first lemma, consider this example: Suppose that we are working in the language of number theory and that the structure under consideration comprises the natural numbers. Let the term $$u$$ be $$x \cdot v$$ and the term $$t$$ be $$y + z$$. Then $$u_t^x$$ is $$\left( y + z \right) \cdot v$$. Now we have to fix a couple of assignment functions. Let the assignment function $$s$$ look like this:

$\begin{array}{c|c} Vars & s \\ \hline x & 12 \\ y & 3 \\ z & 7 \\ v & 4 \\ \vdots & \vdots \end{array}$

So $$s \left( x \right) = 12$$, $$s \left( y \right) = 3$$, and so on.

Now, suppose that $$s'$$ is an assignment function that is just like $$s$$, except that $$s'$$ sends $$x$$ to the value $$\bar{s} \left( t \right)$$, which is $$\bar{s} \left( y + z \right) = 3 + 7 = 10$$:

$\begin{array}{c|c|c} Vars & s & s' \\ \hline x & 12 & 10 \\ y & 3 & 3 \\ z & 7 & 7 \\ v & v & v \\ \vdots & \vdots & \vdots \end{array}$

Now, if you compare $$\bar{s} \left( u_t^x \right)$$ and $$\bar{s'} \left( u \right)$$, you find that

$\left. \begin{array} { c } { \overline { s } \left( u _ { t } ^ { x } \right) = \overline { s } ( ( y + z ) \cdot v ) = ( 3 + 7 ) \cdot 4 = 10 \cdot 4 = 40 } \\ { \overline { s ^ { \prime } } ( u ) = \overline { s ^ { \prime } } ( x \cdot v ) = 10 \cdot 4 = 40 } \end{array} \right.$

So, in this situation, the element of the universe that is assigned by $$s$$ to $$u_t^x$$ is the same as the element of the universe that is assigned by $$s^\prime$$ to $$u$$. In some sense, the lemma states that it does not matter whether you alter the term or the assignment function, the result is the same.

Here is the formal statement:

Lemma 2.6.1. Suppose that $$u$$ is a term, $$x$$ is a variable, and $$t$$ is a term. Suppose that $$s \: : \: Vars \rightarrow A$$ is a variable assignment function and that $$s^\prime = s \left[ x | \overline{s} \left( t \right) \right]$$. Then $$\overline{s} \left( u_t^x \right) = \overline{s^\prime} \left( u \right)$$.

Proof. The proof is by induction on the complexity of the term $$u$$. If $$u$$ is the variable $$x$$, then

\left.\begin{aligned} \overline { s } \left( u _ { t } ^ { x } \right) & = \overline { s } \left( x _ { t } ^ { x } \right) \\ & = \overline { s } ( t ) \\ & = \overline { s ^ { \prime } } ( x ) \\ & = \overline { s ^ { \prime } } ( u ) \end{aligned} \right.

If $$u$$ is the variable $$y$$ and $$y$$ is different than $$x$$, then

\left.\begin{aligned} \overline { s } \left( u _ { t } ^ { x } \right) & = \overline { s } \left( y _ { t } ^ { x } \right) \\ & = \overline { s } ( y ) \\ & = s ( y ) \\ & = s ^ { \prime } ( y ) \\ & = \overline { s } ^ { \prime } ( u ) \end{aligned} \right.

If $$u$$ is a constant symbol $$c$$, then $$\overline{s} \left( u_t^x \right) = \overline{s} \left( c_t^x \right) = \overline{s} \left( c \right) = c^\mathfrak{A} = \overline{s^\prime} \left( u \right)$$.

The last inductive case is if $$u$$ is $$f \left( r_1, r_2, \ldots, r_n \right)$$, with each $$r_i$$ a term. In this case,

$\begin{array}{rcll} \overline{s} \left( u_t^x \right) & = & \overline{s} \left( \left[ f \left( r_1, r_2, \ldots, r_n \right) \right]_t^x \right) & \\ & = & \overline{s} \left( f \left( \left( r_1 \right)_t^x, \left( r_2 \right)_t^x, \ldots, \left( r_n \right)_t^x \right) \right) & \\ & = & f^\mathfrak{A} \left( \overline{s} \left[ \left( r_1 \right)_t^x \right], \overline{s} \left[ \left( r_2 \right)_t^x \right], \ldots, \overline{s} \left[ \left( r_n \right)_t^x \right] \right) & \text{definition of} \: \overline{s} \\ & = & f^\mathfrak{A} \left( \overline{s^\prime} \left( r_1 \right), \overline{s^\prime} \left( r_2 \right), \ldots, \overline{s^\prime} \left( r_n \right) \right) & \text{inductive hypothesis} \\ & = & \overline{s^\prime} \left( f \left( r_1, r_2, \ldots, r_n \right) \right) & \text{definition of} \: \overline{s^\prime} \\ & = & \overline{s^\prime} \left( u \right) & \end{array}$

So for every term $$u$$, $$\overline{s} \left( u_t^x \right) = \overline{s^\prime} \left( u \right)$$.

Chaff: That was hard. If you understood that proof the first time through, you have done something quite out of the ordinary. If, on the other hand, you are a mere mortal, you might want to work through the proof again, keeping an example in mind as you work. Pick a language, terms $$u$$ and $$t$$ in your language, and a variable $$x$$. Fix a particular assignment function $$s$$. Then just follow through the steps of the proof, keeping track of where everything goes. We would write it out for you, but you will get more out of doing it for yourself. Go to it!

Our next technical result is the lemma that we quoted explicitly in the proof of Theorem 2.5.1. This theorem states that as long as $$t$$ is substitutable for $$x$$ in $$\phi$$, the two different ways of evaluating the truth of "$$\phi$$, where you interpret $$x$$ as $$t$$" coincide. The first way of evaluating the truth would be by forming the formula $$\phi_t^x$$ and seeing if $$\mathfrak{A} \models \phi_t^x \left[ s \right]$$. The second way would be to change the assignment function $$s$$ to interpret $$x$$ as $$\overline{s} \left( t \right)$$ and checking whether the original formula $$\phi$$ is true with this new assignment function. The theorem states that the two methods are equivalent.

Theorem 2.6.2. Suppose that $$\phi$$ is an $$\mathcal{L}$$-formula, $$x$$ is a variable, $$t$$ is a term, and $$t$$ is substitutable for $$x$$ in $$\phi$$. Suppose that $$s \: : \: Vars \rightarrow A$$ is a variable assignment function and that $$s^\prime = s \left[ x | \overline{s} \left( t \right) \right]$$. Then $$\mathfrak{A} \models \phi_t^x \left[ s \right]$$ if and only if $$\mathfrak{A} \models \phi \left[ s^\prime \right]$$.

Proof. We use induction on the complexity of $$\phi$$. The first base case is where $$\phi : \equiv u_1 = u_2$$, where $$u_1$$ and $$u_2$$ are terms. Then the following are equivalent:

$\begin{array}{ll} \mathfrak{A} \models \phi_t^x \left[ s \right] & \\ \mathfrak{A} \models \left( u_1 \right)_t^x = \left( u_2 \right)_t^x \left[ s \right] & \\ \overline{s} \left( \left( u_1 \right)_t^x \right) = \overline{s} \left( \left( u_2 \right)_t^x \right) & \text{definition of satisfaction} \\ \overline{s^\prime} \left( u_1 \right) = \overline{s^\prime} \left( u_2 \right) & \text{by Lemma 2.6.1} \\ \mathfrak{A} \models \phi \left[ s^\prime \right] & \end{array}$

The second base case is where $$\phi : \equiv R \left( u_1, u_2, \ldots, u_n \right). This case is similar to the case above. The inductive cases involving the connectives \(\lor$$ and $$\neg$$ follow immediately from the inductive hypothesis.

This leaves the last inductive case, where $$\phi : \equiv \forall y \psi$$. We break this case down into two subcases: In the first subcase $$x$$ is $$y$$, and in the second subcase $$x$$ is not $$y$$.

If $$\phi : \equiv \forall y \psi$$ and $$y$$ is $$x$$, then $$\phi_t^x$$ is $$\phi$$. Therefore, $$\mathfrak{A} \models \phi_t^x \left[ s \right]$$ if and only if $$\mathfrak{A} \models \phi \left[ s \right]$$. But as $$s$$ and $$s^\prime$$ agree on all of the free variables of $$\phi$$ ($$x$$ is not free\), by Proposition 1.7.7, $$\mathfrak{A} \models \phi \left[ s \right]$$ if and only if $$\mathfrak{A} \models \phi \left[ s^\prime \right]$$, as needed for this subcase.

The second subcase, where $$\phi : \equiv \forall y \psi$$ and $$y$$ is not $$x$$, is examined in two sub-subcases:

Sub-subcase 1: If $$\phi : \equiv \forall y \psi$$, $$y$$ is not $$x$$, and $$x$$ is not free in $$\psi$$, then we know by Exercise 5 in Section 1.8 that $$\psi_t^x$$ is $$\psi$$, and thus $$\phi_t^x$$ is $$\phi$$. But then

$\begin{array}{ll} \mathfrak{A} \models \phi_t^x \left[ s \right] & \text{iff} \\ \mathfrak{A} \models \left( \forall y \right) \left( \psi_t^x \right) \left[ s \right] & \text{iff} \\ \mathfrak{A} \models \left( \psi_t^x \right) \left[ s \left[ y | a \right] \right] & \text{for every} \: a \in A \end{array}.$

But we also know that

$\begin{array}{ll} \mathfrak{A} \models \phi \left[ s^\prime \right] & \text{iff} \\ \mathfrak{A} \models \left( \forall y \right) \left( \psi \right) \left[ s^\prime \right] & \text{iff} \\ \mathfrak{A} \models \psi \left[ s^\prime \left[ y | a \right] \right] & \text{for every} \: a \in A \end{array}.$

But since $$x$$ is not $$y$$, we know that for any $$a \in A$$, $$s^\prime \left[ y | a \right] = s \left[ y | a \right] \left[ x | \overline{s} \left( t \right) \right]$$, so by the inductive hypothesis (notice that $$t$$ is substitutable for $$x$$ in $$\psi$$) we have

$\mathfrak{A} \models \left( \psi_t^x \right) \left[ s \left[ y | a \right] \right] \: \text{iff} \: \mathfrak{A} \models \psi \left[ s^\prime \left[ y | a \right] \right].$

So $$\mathfrak{A} \models \phi_t^x \left[ s \right]$$ if and only if $$\mathfrak{A} \models \phi \left[ s^\prime \right]$$, as needed.