Substitution Theorem for Terms
Theorem
Let $\beta, \tau$ be terms.
Let $x \in \mathrm {VAR}$ be a variable.
Let $\map \beta {x \gets \tau}$ be the substitution instance of $\beta$ substituting $\tau$ for $x$.
Let $\AA$ be a structure for predicate logic.
Let $\sigma$ be an assignment for $\beta$ 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 \beta {x \gets \tau} } \sqbrk \sigma = \map {\operatorname{val}_\AA} \beta \sqbrk {\sigma + \paren {x / a} }$
where $\sigma + \paren {x / a}$ is the extension of $\sigma$ by mapping $x$ to $a$.
Proof
Proceed by the Principle of Structural Induction on the definition of term, applied to $\beta$.
If $\beta = y$ for some variable $y$, then:
- $\map \beta {x \gets \tau} = \begin {cases} \tau & : \text{if $y = x$} \\ y & : \text {otherwise} \end {cases}$
In the first case:
\(\ds \map {\operatorname{val}_\AA} {\map \beta {x \gets \tau} } \sqbrk \sigma\) | \(=\) | \(\ds \map {\operatorname{val}_\AA} \tau \sqbrk \sigma\) | ||||||||||||
\(\ds \) | \(=\) | \(\ds a\) | Definition of $a$ | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {\paren {\sigma + \paren {x / a} } } x\) | Definition of Extension of Assignment | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {\operatorname{val}_\AA} \beta \sqbrk {\sigma + \paren {x / a} }\) | Definition of Value under $\sigma + \paren {x / a}$ |
In the second case:
\(\ds \map {\operatorname{val}_\AA} {\map \beta {x \gets \tau} } \sqbrk \sigma\) | \(=\) | \(\ds \map {\operatorname{val}_\AA} y \sqbrk \sigma\) | ||||||||||||
\(\ds \) | \(=\) | \(\ds \map \sigma y\) | Definition of Value under $\sigma$ | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {\paren {\sigma + \paren {x / a} } } y\) | Definition of Extension of Assignment | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {\operatorname{val}_\AA} \beta \sqbrk {\sigma + \paren {x / a} }\) | Definition of Value under $\sigma + \paren {x / a}$ |
as desired.
If $\beta = \map f {\tau_1, \ldots, \tau_n}$ and the induction hypothesis holds for $\tau_1, \ldots, \tau_n$, then:
- $\map \beta {x \gets \tau} = \map f {\map {\tau_1} {x \gets \tau}, \ldots, \map {\tau_n} {x \gets \tau} }$
Now:
\(\ds \map {\operatorname{val}_\AA} {\map \beta {x \gets \tau} } \sqbrk \sigma\) | \(=\) | \(\ds \map {\operatorname{val}_\AA} {\map f {\map {\tau_1} {x \gets \tau}, \ldots, \map {\tau_n} {x \gets \tau} } } \sqbrk \sigma\) | ||||||||||||
\(\ds \) | \(=\) | \(\ds \map {f_\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 {f_\AA} {\map {\operatorname{val}_\AA} {\tau_1} \sqbrk {\sigma + \paren {x / a} }, \ldots, \map {\operatorname{val}_\AA} {\tau_n} \sqbrk {\sigma + \paren {x / a} } }\) | Induction Hypothesis | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {\operatorname{val}_\AA} \beta \sqbrk {\sigma + \paren {x / a} }\) | Definition of Value under $\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.7$