next up previous contents
Next: Turing Machines Up: Metatheory Previous: Augmentation; Completion of Completeness

The Löwenheim-Skolem Theorem

Theorem 4.4 (Löwenheim-Skolem Theorem)   Let $\Phi$ be a satisfiable and countable set of formulas based on some symbol set S. Then there is an interpretation with a countable domain that satisfies $\Phi$.

Proof. Given the Completeness Theorem (4.1), the proof is straightforward. Assume the hypothesis of the theorem to be proved, but stipulate for the time being that $\Phi$ is composed of sentences. It follows immediately that $\Phi$ is consistent. Because every formula contains only finitely many symbols from the relevant symbol set S, there are countably many S-symbols in $\Phi$. Therefore, we can assume that S itself is countable. At this point the interpretation $\cal I$$^\star_w$ specified in the proof of the Completeness Theorem applies. Recall that the domain $\cal D$ of this interpretation was the set of all $\bar{t}$, where t ranges over TS, the set of all terms that can be generated from S. Because TS is countable, so is $\cal D$ (see Theorem 2.2).

It is easy to extend this reasoning to cover the case where $\Phi$ is composed of formulas. To begin, where, as usual, LS denotes the set of all formulas that can be constructed from some symbol set S, define

\begin{displaymath}L^S_n = \{\phi : \phi \in L^S \mbox{ and free}(\phi) \subseteq \{v_1,
\ldots, v_n\}\}.\end{displaymath}

Now, again, let $\Phi$ be composed of formulas, and let $c_1, \ldots, c_n$ be constants not appearing in $\Phi$. Next, set

\begin{displaymath}\Phi' = \{\psi\frac{c_1 \cdots c_n}{v_1 \cdots v_n} : n \in \mbox{{\bf
N}}, \psi \in (L^S_n \cap \Phi)\}.\end{displaymath}

By previous reasoning $\Phi'$ is satisfiable over the countable domain over which $\Phi$ is also satisfiable. QED

Can you see why many regard the Löwenheim-Skolem Theorem to be a paradox? $\ldots$


next up previous contents
Next: Turing Machines Up: Metatheory Previous: Augmentation; Completion of Completeness
Selmer Bringsjord
1999-04-19