Value of Term under Assignment Determined by Variables

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:

For each variable $x$ occurring in $\tau$, $\map \sigma x = \map {\sigma'} x$

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$