Substitution Theorem for Well-Formed Formulas
Theorem
Let $\mathbf A$ be a WFF of predicate logic.
Let $x \in \mathrm{VAR}$ be a variable.
Let $\tau$ be a term of predicate logic which is freely substitutable for $x$ in $\mathbf A$.
Let $\map {\mathbf A} {x \gets \tau}$ be the substitution instance of $\mathbf A$ substituting $\tau$ for $x$.
Let $\AA$ be a structure for predicate logic.
Let $\sigma$ be an assignment for $\mathbf A$ and $\tau$.
Suppose that:
- $\map {\operatorname{val}_\AA} \tau \sqbrk \sigma = a$
where $\map {\operatorname{val}_\AA} \tau \sqbrk \sigma$ is the value of $\tau$ under $\sigma$.
Then:
- $\map {\operatorname{val}_\AA} {\map {\mathbf A} {x \gets \tau} } \sqbrk \sigma = \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\sigma + \paren {x / a} }$
where $\sigma + \paren {x / a}$ is the extension of $\sigma$ by mapping $x$ to $a$.
Corollary
Let $\map {\mathbf A} {x_1, \ldots, x_n}$ be a WFF whose free variables are among $x_1, \ldots, x_n$.
Let $\tau_1, \ldots, \tau_n$ be closed terms, and let each $\tau_i$ be freely substitutable for $x_i$.
Let $a_i = \map {\operatorname{val}_\AA} {\tau_i}$, where $\operatorname{val}_\AA$ denotes the value of $\tau$ in $\AA$.
Then:
- $\AA \models_{\mathrm{PL}} \map {\mathbf A} {\tau_1, \ldots, \tau_n}$ if and only if $\AA \models_{\mathrm{PL_A}} \mathbf A \sqbrk {a_1, \ldots, a_n}$
where $\models_{\mathrm{PL}}$ denotes model of sentence, and $\models_{\mathrm{PL_A}}$ denotes model of formula.
Proof
Proceed by the Principle of Structural Induction on the bottom-up specification of predicate logic, applied to $\mathbf A$.
If $\mathbf A = \map p {\tau_1, \ldots, \tau_n}$, then:
- $\map {\mathbf A} {x \gets \tau} = \map p {\map {\tau_1} {x \gets \tau}, \ldots, \map {\tau_n} {x \gets \tau} }$
where $\map {\tau_i} {x \gets \tau}$ is the substitution instance of $\tau_i$.
Now:
\(\ds \map {\operatorname{val}_\AA} {\map {\mathbf A} {x \gets \tau} } \sqbrk \sigma\) | \(=\) | \(\ds \map {\operatorname{val}_\AA} {\map p {\map {\tau_1} {x \gets \tau}, \ldots, \map {\tau_n} {x \gets \tau} } } \sqbrk \sigma\) | ||||||||||||
\(\ds \) | \(=\) | \(\ds \map {p_\AA} {\map {\operatorname{val}_\AA} {\map {\tau_1} {x \gets \tau} } \sqbrk \sigma, \ldots, \map {\operatorname{val}_\AA} {\map {\tau_n} {x \gets \tau} } \sqbrk \sigma}\) | Definition of Value under $\sigma$ | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {p_\AA} {\map {\operatorname{val}_\AA} {\tau_1} \sqbrk {\sigma + \paren {x / a} }, \ldots, \map {\operatorname{val}_\AA} {\tau_n} \sqbrk {\sigma + \paren {x / a} } }\) | Substitution Theorem for Terms | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\sigma + \paren {x / a} }\) | Definition of Value under $\sigma + \paren {x / a}$ |
Suppose $\mathbf A = \neg \mathbf B$ and the induction hypothesis applies to $\mathbf B$.
Then since $\tau$ is also free for $x$ in $\mathbf B$:
\(\ds \map {\operatorname{val}_\AA} {\map {\mathbf A} {x \gets \tau} } \sqbrk \sigma\) | \(=\) | \(\ds \map {f^\neg} {\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \sigma}\) | Definition of Value under $\sigma$ | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {f^\neg} {\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk {\sigma + \paren {x / a} } }\) | Induction Hypothesis | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\sigma + \paren {x / a} }\) | Definition of Value under $\sigma + \paren {x / a}$ |
Suppose $\mathbf A = \mathbf B \circ \mathbf B'$ for $\circ$ one of $\land, \lor, \implies, \iff$ and the induction hypothesis applies to $\mathbf B, \mathbf B'$.
Then since $\tau$ is also free for $x$ in $\mathbf B$ and $\mathbf B'$:
\(\ds \map {\operatorname{val}_\AA} {\map {\mathbf A} {x \gets \tau} } \sqbrk \sigma\) | \(=\) | \(\ds \map {f^\circ} {\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \sigma, \map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \sigma}\) | Definition of Value under $\sigma$ | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {f^\circ} {\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk {\sigma + \paren {x / a} }, \map {\operatorname{val}_\AA} {\mathbf B} \sqbrk {\sigma + \paren {x / a} } }\) | Induction Hypothesis | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\sigma + \paren {x / a} }\) | Definition of Value under $\sigma + \paren {x / a}$ |
Suppose $\mathbf A = \exists y: \mathbf B$ or $\mathbf A = \forall y: \mathbf B$, and the induction hypothesis applies to $\mathbf B$.
Because $\tau$ is free for $x$ in $\mathbf A$, it must be that either $x$ does not occur freely in $\mathbf A$, or $y$ does not occur in $\tau$.
In the first case:
- $\map {\mathbf A} {x \gets \tau} = \mathbf A$
and by Value of Formula under Assignment Determined by Free Variables:
- $\map {\operatorname{val}_\AA} {\mathbf A} \sqbrk \sigma = \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\sigma + \paren {x / a} }$
Now consider the case where $y$ does not occur in $\tau$.
From the definition of value under $\sigma$, $\map {\operatorname{val}_\AA} {\map {\mathbf A} {x \gets \tau} } \sqbrk \sigma$ is determined by:
- $\map {\operatorname{val}_\AA} {\map {\mathbf B} {x \gets \tau} } \sqbrk {\sigma + \paren {y / a'} }$
where $a'$ ranges over $\AA$.
Now from Value of Term under Assignment Determined by Variables, since $y$ does not occur in $\tau$:
- $\map {\operatorname{val}_\AA} \tau \sqbrk {\sigma + \paren {y / a'} } = \map {\operatorname{val}_\AA} \tau \sqbrk \sigma = a$
for all $a'$.
Hence the induction hypothesis also applies to the assignment $\sigma + \paren {y / a'}$.
Thus, for all $a'$:
\(\ds \map {\operatorname{val}_\AA} {\map {\mathbf B} {x \gets \tau} } \sqbrk {\sigma + \paren {y / a'} }\) | \(=\) | \(\ds \map {\operatorname{val}_\AA} {\mathbf B} \sqbrk {\sigma + \paren {y / a'} + \paren {x / a} }\) | Induction Hypothesis | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {\operatorname{val}_\AA} {\mathbf B} \sqbrk {\sigma + \paren {x / a} + \paren {y / a'} }\) | Definition of Extension of Assignment |
from which we infer:
- $\map {\operatorname{val}_\AA} {\map {\mathbf A} {x \gets \tau} } \sqbrk \sigma = \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\sigma + \paren {x / a} }$
as desired.
The result follows by the Principle of Structural Induction.
$\blacksquare$
Sources
- 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\text{II}.8$ Further Semantic Notions: Lemma $\text{II}.8.10$