PlanetMath (more info)
 Math for the people, by the people.
Encyclopedia | Requests | Forums | Docs | Wiki | Random | RSS  
Login
create new user
name:
pass:
forget your password?
Main Menu
Owner confidence rating: Very low Entry average rating: No information on entry rating
[parent] proof of downward Lowenheim-Skolem theorem (Proof)

We present here a proof of the Downward Lowenheim Skolem Theorem. The idea is to construct a submodel that meets the requirements of the DLS Theorem: we take $ K$ and close it under a procedure of choosing appropriate witnesses for the existential formulas satisfied by $ \mathcal{A}$. Choosing the appropriate witnesses is done with the help of the so-called Skolem functions and thus rests upon the choice function.

Proof: First of all we introduce a usefull tool for the proof. Lemma: (Tarski's Lemma) If $ \mathcal{A}$ and $ \mathcal{B}$ are $ L$-structures with the domain of $ \mathcal{A}$ being a subset of the domain of $ \mathcal{B}$ then $ \mathcal{A}$ is an elementary substructure of $ \mathcal{B}$ if for every $ L$-formula $ \phi(\emph{x},y)$ with $ a \in A$ and $ b \in B$, we have $ \mathcal{B}\models \phi(a,b)$ <-> For some $ a' \in A$ we have $ \mathcal{A}\models \phi(a,a')$

Proof. Let's supposes the biconditionnal holds, then we need to show that $ \mathcal{A}$ is a substructure of $ \mathcal{B}$. This means that we need to show that every formula that is true in $ \mathcal{A}$ is true in $ \mathcal{B}$. The proof is straighforward with an induction on the complexity of formulas (connectives, negation, quantifiers).

Now, fix a point $ p \in {dom}(\mathcal{A})$. For each $ L$-formula $ \phi(\emph{x},y)$, define the Skolem function of $ \phi$, $ g_\phi : A^n \to A$ (with $ A={dom}(\mathcal{A})$) by:

$ p \in A^n \to$ some $ p' \in A$ such that $ \mathcal{A}\models \phi(p,p')$ if such a $ p'$ exists and $ p$ otherwise. The set of Skolem functions has a cardinality equal to that of $ L$.

The purpose here is to construct a model $ \mathcal{B}$ whose domain $ B$ is closed under the skolem functions. This means that the domain of $ \mathcal{A}$ contains all the witnesses we've appropriately choosen. If we take an existential formula $ \exists y \phi(\emph{x},y)$ and $ b \in B^k$ and if we apply the Skolem function to $ b$ we will have a witness for $ \exists x \phi(\emph{b},x)$. In other words, this means that $ \mathcal{A}\models \exists x \phi(b,x) \to \mathcal{A}\models \phi(b,g_\phi(b))$. By construction $ g_\phi(b)$ is in $ B$ and thus $ \mathcal{B}$ meets the requirements of Tarski's Lemma. We can find an elementary substructure of $ \mathcal{A}$.

Let's take $ K$ of above and set $ K_0:=K$ and $ K_{i+1}$ is the set of the $ g_\phi(p), p \in K_i \wedge g_\phi$ (with $ g_\phi$ a Skolem function). Let $ B:= \bigcup K_i$. Then $ B$ is closed under Skolem functions. And we have $ \vert K\vert\leq \omega .\vert L\vert+\vert K\vert= \vert L\vert+\vert K\vert$. This comes from the fact that $ \vert L\vert+\vert K_i\vert=\vert\emph{SF}\vert+\vert K_i\vert= \sum_{k \in \m... ..._k\vert+\vert K_i\vert= \sum_{k \in \mathbb{N} }\vert(SF)_k\vert*\vert K_i\vert$ but we have $ \vert K_{i+1}\vert \leq \sum_{k \in \mathbb{N} }\vert(SF)_k\vert*\vert K_i\vert$. We need now to provide interpretations of relations, predicates, functions and constants so it can fit $ \mathcal{A}$.

We have because $ B$ is closed under $ L$-terms and for an $ L$-function symbol $ f$, the Skolem function of the $ L$-formula $ f(x)=y$ takes the value $ f^\mathcal{A}(p)$ at p:

for any n-ary relation symbol $ P$: $ P^\mathcal{B}=P^\mathcal{A}\bigcap B^n$

for an m-ary function symbol $ f$ and $ p \in B^m , p' \in B$ we have $ f^\mathcal{A}(p)=p'$ <-> $ f^\mathcal{B}(p)=p'$.

for a constant symbol $ c$, we have $ c^\mathcal{A}=c^\mathcal{B}$ We have constructed a substructure $ \mathcal{B}$ of $ \mathcal{A}$.



"proof of downward Lowenheim-Skolem theorem" is owned by GodelsTheorem.
(view preamble | get metadata)

View style:


This object's parent.
Log in to rate this entry.
(view current ratings)

Cross-references: constant symbol, function symbol, n-ary relation, functions, predicates, relations, interpretations, contains, closed under, cardinality, point, fix, quantifiers, negation, connectives, induction, elementary substructure, subset, domain, choice function, Skolem functions, formulas, witnesses, meets, submodel, proof

This is version 11 of proof of downward Lowenheim-Skolem theorem, born on 2008-08-14, modified 2008-10-25.
Object id is 10942, canonical name is ProofOfDownwardLowenheimSkolemTheorem.
Accessed 367 times total.

Classification:
AMS MSC03C07 (Mathematical logic and foundations :: Model theory :: Basic properties of first-order languages and structures)

Pending Errata and Addenda
None.
Discussion
Style: Expand: Order:
forum policy

No messages.

Interact
post | correct | update request | add example | add (any)