Universal Closures are Semantically Equivalent

From ProofWiki
Jump to navigation Jump to search

Theorem

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

Let $\mathbf B, \mathbf B'$ be universal closures of $\mathbf A$.


Then $\mathbf B$ and $\mathbf B'$ are semantically equivalent.


Proof

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


Let $\mathbf B$ be any universal closure of $\mathbf A$.

Then $\mathbf B$ is a sentence of the form:

$\forall x_1: \cdots \forall x_n: \mathbf A$

By definition of the models relation:

$\AA \models_{\mathrm{PL}} \mathbf B$ if and only if $\map {\operatorname{val}_\AA} {\mathbf B} = \T$

Hence, recursively applying the definition of $\map {\operatorname{val}_\AA} \cdot \sqbrk \sigma$, we see:

$\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \O = \T$ if and only if $\forall a_1, \ldots, a_n \in A: \mathop{\map {\operatorname{val}_\AA} {\mathbf A} } \sqbrk {\dfrac{x_1} {a_1} + \ldots + \dfrac{x_n} {a_n} } = \T$

where $\dfrac{x_1} {a_1} + \ldots + \dfrac{x_n} {a_n}$ denotes the iterated extension of an assignment.


By Value of Formula under Assignment Determined by Free Variables:

$\map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\dfrac{x_1} {a_1} + \ldots + \dfrac{x_n} {a_n} }$ only depends on the $a_i$ for the free variables $x_i$ in $\mathbf A$.

Because we check all possible $a_i \in A$ and all free variables $x_i$ in $\mathbf A$ are quantified over in $\mathbf B$, it follows that:

$\forall a_1, \ldots, a_n \in A: \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\dfrac{x_1} {a_1} + \ldots + \dfrac{x_n} {a_n} } = \T$

if and only if:

$\forall a_1, \ldots, a_k \in A: \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\dfrac{x_1} {a_1} + \ldots + \dfrac{x_k} {a_k} } = \T$

where $x_1, \ldots, x_k$ are the free variables of $\mathbf A$.


But this last condition does not depend on $\mathbf B$ beyond that it be a universal closure.

Hence, for any two universal closures $\mathbf B, \mathbf B'$ of $\mathbf A$:

$\AA \models_{\mathrm{PL}} \mathbf B$ if and only if $\AA \models_{\mathrm{PL}} \mathbf B$

The result follows by definition of semantic equivalence.

$\blacksquare$


Sources