Theorem: Value of Formula under Assignment Determined by Free Variables

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:
{{begin-eqn}}
{{eqn|l = \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk \sigma
     |r = \map {f^\neg} {\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \sigma}
     |c = {{Defof|Value of Formula under Assignment|Value under $\sigma$}}
}}
{{eqn|r = \map {f^\neg} {\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk {\sigma'} }
     |c = Induction Hypothesis
}}
{{eqn|r = \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\sigma'}
     |c = {{Defof|Value of Formula under Assignment|Value under $\sigma'$}}
}}
{{end-eqn}}
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'$:
{{begin-eqn}}
{{eqn|l = \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk \sigma
     |r = \map {f^\circ} {\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \sigma, \map {\operatorname{val}_\AA} {\mathbf B'} \sqbrk \sigma}
     |c = {{Defof|Value of Formula under Assignment|Value under $\sigma$}}
}}
{{eqn|r = \map {f^\circ} {\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk {\sigma'}, \map {\operatorname{val}_\AA} {\mathbf B'} \sqbrk {\sigma'} }
     |c = Induction Hypothesis
}}
{{eqn|r = \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\sigma'}
     |c = {{Defof|Value of Formula under Assignment|Value under $\sigma'$}}
}}
{{end-eqn}}
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$:
{{begin-eqn}}
{{eqn|l = \map {\paren {\sigma + \paren {x / a} } } y
     |r = \begin{cases} a &: \text{if } y = x \\ \map \sigma y &: \text{otherwise} \end{cases}
     |c = {{Defof|Extension of Assignment}}
}}
{{eqn|r = \begin{cases} a &: \text{if } y = x \\ \map {\sigma'} y &: \text{otherwise} \end{cases}
     |c = Assumption on $\sigma, \sigma'$
}}
{{eqn|r = \map {\paren {\sigma' + \paren {x / a} } } y
     |c = {{Defof|Extension of Assignment}}
}}
{{end-eqn}}
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.
{{qed}}
Category:Predicate Logic
70ddx0l0sevhwuwsgcin8l13bw3o6lt