Substitution Instance of Term is Term
Jump to navigation
Jump to search
Theorem
Let $\beta, \tau$ be terms of predicate logic.
Let $x \in \operatorname {VAR}$ be a variable.
Let $\map \beta {x \gets \tau}$ be the substitution instance of $\beta$ substituting $\tau$ for $x$.
Then $\map \beta {x \gets \tau}$ is a term.
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 either case, $\map \beta {x \gets \tau}$ is a term.
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} }$
By the induction hypothesis, each $\map {\tau_i} {x \gets \tau}$ is a term.
Hence so is $\map \beta {x \gets \tau}$.
The result follows by the Principle of Structural Induction.
$\blacksquare$
Sources
- 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\mathrm{II}.8$ Further Semantic Notions