proof of downward Lowenheim-Skolem theorem
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 and close it under a procedure of choosing appropriate witnesses for the existential formulas satisfied by . 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 and are -structures with the domain of being a subset of the domain of then is an elementary substructure of if for every -formula with and , we have ¡-¿ For some we have
Proof. Let’s supposes the biconditionnal holds, then we need to show that is a substructure of . This means that we need to show that every formula that is true in is true in . The proof is straighforward with an induction on the complexity of formulas (connectives, negation, quantifiers).
Now, fix a point . For each -formula , define the Skolem function of , (with ) by:
some such that if such a exists and otherwise. The set of Skolem functions has a cardinality equal to that of .
The purpose here is to construct a model whose domain is closed under the skolem functions. This means that the domain of contains all the witnesses we’ve appropriately choosen. If we take an existential formula and and if we apply the Skolem function to we will have a witness for . In other words, this means that . By construction is in and thus meets the requirements of Tarski’s Lemma. We can find an elementary substructure of .
Let’s take of above and set and is the set of the (with a Skolem function). Let . Then is closed under Skolem functions. And we have . This comes from the fact that but we have . We need now to provide interpretations of relations, predicates, functions and constants so it can fit .
We have because is closed under -terms and for an -function symbol , the Skolem function of the -formula takes the value at p:
for any n-ary relation symbol :
for an m-ary function symbol and we have ¡-¿ .
for a constant symbol , we have We have constructed a substructure of .
|Title||proof of downward Lowenheim-Skolem theorem|
|Date of creation||2013-03-22 18:18:59|
|Last modified on||2013-03-22 18:18:59|
|Last modified by||GodelsTheorem (21277)|