Value of Formula under Assignment Determined by Free Variables

Theorem

Let $\mathbf A$ be a WFF of predicate logic.

Let $\AA$ be a structure for predicate logic.

Let $\sigma, \sigma'$ be assignments for $\mathbf A$ in $\AA$ such that:

For each free variable $x$ of $\mathbf A$, $\map \sigma x = \map {\sigma'} x$

Then:

$\map {\operatorname{val}_\AA} {\mathbf A} \sqbrk \sigma = \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\sigma'}$

where $\map {\operatorname{val}_\AA} {\mathbf A} \sqbrk \sigma$ is the value of $\mathbf A$ under $\sigma$.

Proof

Proceed by the Principle of Structural Induction applied to the bottom-up specification of predicate logic.

If $\mathbf A = \map p {\tau_1, \ldots, \tau_n}$, then:

$\map {\operatorname{val}_\AA} {\mathbf A} \sqbrk \sigma = \map {p_\AA} {\map {\operatorname{val}_\AA} {\tau_1} \sqbrk \sigma, \ldots, \map {\operatorname{val}_\AA} {\tau_n} \sqbrk \sigma}$

Because $\mathbf A$ contains no quantifiers, all its variables are free, and hence are in the domain of $\sigma, \sigma'$ as assignments.

Thus $\sigma, \sigma'$ are assignments for each $\tau_i$, and by Value of Term under Assignment Determined by Variables:

$\map {\operatorname{val}_\AA} {\tau_i} \sqbrk \sigma = \map {\operatorname{val}_\AA} {\tau_i} \sqbrk {\sigma'}$

for each $\tau_i$.

It is immediate that:

$\map {\operatorname{val}_\AA} {\mathbf A} \sqbrk \sigma = \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\sigma'}$

If $\mathbf A = \neg \mathbf B$ and the induction hypothesis applies to $\mathbf B$, then:

\(\ds \map {\operatorname{val}_\AA} {\mathbf A} \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'} }\)

Induction Hypothesis

\(\ds \)

\(=\)

\(\ds \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\sigma'}\)

Definition of Value under $\sigma'$

If $\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'$:

\(\ds \map {\operatorname{val}_\AA} {\mathbf A} \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'}, \map {\operatorname{val}_\AA} {\mathbf B'} \sqbrk {\sigma'} }\)

Induction Hypothesis

\(\ds \)

\(=\)

\(\ds \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\sigma'}\)

Definition of Value under $\sigma'$

If $\mathbf A = \exists x: \mathbf B$ or $\mathbf A = \forall x : \mathbf B$, and the induction hypothesis applies to $\mathbf B$, then from the definition of value under $\sigma$:

$\map {\operatorname{val}_\AA} {\mathbf A} \sqbrk \sigma$

is determined by the values:

$\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk {\sigma + \paren {x / a} }$

where $a$ ranges over $\AA$, and $\sigma + \paren {x / a}$ is the extension of $\sigma$ mapping $x$ to $a$.

Now, for a free variable $y$ of $\mathbf B$:

\(\ds \map {\paren {\sigma + \paren {x / a} } } y\)

\(=\)

\(\ds \begin{cases} a &: \text{if } y = x \\ \map \sigma y &: \text{otherwise} \end{cases}\)

Definition of Extension of Assignment

\(\ds \)

\(=\)

\(\ds \begin{cases} a &: \text{if } y = x \\ \map {\sigma'} y &: \text{otherwise} \end{cases}\)

Assumption on $\sigma, \sigma'$

\(\ds \)

\(=\)

\(\ds \map {\paren {\sigma' + \paren {x / a} } } y\)

Definition of Extension of Assignment

Hence, by the induction hypothesis:

$\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk {\sigma + \paren {x / a} } = \map {\operatorname{val}_\AA} {\mathbf B} \sqbrk {\sigma' + \paren {x / a} }$

It follows that:

$\map {\operatorname{val}_\AA} {\mathbf A} \sqbrk \sigma = \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\sigma'}$

The result follows from the Principle of Structural Induction.

$\blacksquare$