Value of Term under Assignment Determined by Variables
Jump to navigation
Jump to search
Theorem
Let $\tau$ be a term of predicate logic.
Let $\AA$ be a structure for predicate logic.
Let $\sigma, \sigma'$ be assignments for $\tau$ in $\AA$ such that:
Then:
- $\map {\operatorname{val}_\AA} \tau \sqbrk \sigma = \map {\operatorname{val}_\AA} \tau \sqbrk {\sigma'}$
where $\map {\operatorname{val}_\AA} \tau \sqbrk \sigma$ is the value of $\tau$ under $\sigma$.
Proof
Proceed by the Principle of Structural Induction applied to the definition of a term.
If $\tau = x$, then:
\(\ds \map {\operatorname{val}_\AA} \tau \sqbrk \sigma\) | \(=\) | \(\ds \map \sigma x\) | Definition of value under $\sigma$ | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {\sigma'} x\) | Assumption on $\sigma, \sigma'$ | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {\operatorname{val}_\AA} \tau \sqbrk {\sigma'}\) | Definition of value under $\sigma$ |
as desired.
If $\tau = \map f {\tau_1, \ldots, \tau_n}$ and the induction hypothesis applies to each $\tau_i$, then:
\(\ds \map {\operatorname{val}_\AA} \tau \sqbrk \sigma\) | \(=\) | \(\ds \map {f_\AA} {\map {\operatorname{val}_\AA} {\tau_1} \sqbrk \sigma, \ldots, \map {\operatorname{val}_\AA} {\tau_n} \sqbrk \sigma}\) | Definition of value under $\sigma$ | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {f_\AA} {\map {\operatorname{val}_\AA} {\tau_1} \sqbrk {\sigma'}, \ldots, \map {\operatorname{val}_\AA} {\tau_n} \sqbrk {\sigma'} }\) | Induction Hypothesis | |||||||||||
\(\ds \) | \(=\) | \(\ds \map {\operatorname{val}_\AA} \tau \sqbrk {\sigma'}\) | Definition of value under $\sigma'$ |
The result follows from the Principle of Structural Induction.
$\blacksquare$