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 K 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 functionsMathworldPlanetmath 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 L-structuresMathworldPlanetmath with the domain of π’œ being a subset of the domain of ℬ then π’œ is an elementary substructure of ℬ if for every L-formulaMathworldPlanetmathPlanetmath ϕ⁒(x,y) with a∈A and b∈B, we have β„¬βŠ§Ο•β’(a,b) Β‘-ΒΏ For some aβ€²βˆˆA we have π’œβŠ§Ο•β’(a,aβ€²)

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 inductionMathworldPlanetmath on the complexity of formulas (connectivesMathworldPlanetmath, negationMathworldPlanetmath, quantifiersMathworldPlanetmath).

Now, fix a point p∈d⁒o⁒m⁒(π’œ). For each L-formula ϕ⁒(x,y), define the Skolem function of Ο•, gΟ•:Anβ†’A (with A=d⁒o⁒m⁒(π’œ)) by:

p∈Anβ†’ some pβ€²βˆˆA such that π’œβŠ§Ο•β’(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 ℬ whose domain B 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 βˆƒy⁒ϕ⁒(x,y) and b∈Bk and if we apply the Skolem function to b we will have a witness for βˆƒx⁒ϕ⁒(b,x). In other words, this means that π’œβŠ§βˆƒx⁒ϕ⁒(b,x)β†’π’œβŠ§Ο•β’(b,gϕ⁒(b)). By construction gϕ⁒(b) is in B and thus ℬ meets the requirements of Tarski’s Lemma. We can find an elementary substructure of π’œ.

Let’s take K of above and set K0:=K and Ki+1 is the set of the gϕ⁒(p),p∈Ki∧gΟ• (with gΟ• a Skolem function). Let B:=⋃Ki. Then B is closed under Skolem functions. And we have |K|≀ω.|L|+|K|=|L|+|K|. This comes from the fact that |L|+|Ki|=|SF|+|Ki|=βˆ‘kβˆˆβ„•|(S⁒F)k|+|Ki|=βˆ‘kβˆˆβ„•|(S⁒F)k|*|Ki| but we have |Ki+1|β‰€βˆ‘kβˆˆβ„•|(S⁒F)k|*|Ki|. We need now to provide interpretationsMathworldPlanetmath of relationsMathworldPlanetmath, predicatesMathworldPlanetmath, functions and constants so it can fit π’œ.

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π’œβ’(p) at p:

for any n-ary relation symbol P: Pℬ=Pπ’œβ’β‹‚Bn

for an m-ary function symbol f and p∈Bm,pβ€²βˆˆB we have fπ’œβ’(p)=pβ€² Β‘-ΒΏ fℬ⁒(p)=pβ€².

for a constant symbol c, we have cπ’œ=cℬ We have constructed a substructure ℬ of π’œ.

Title proof of downward Lowenheim-Skolem theorem
Canonical name ProofOfDownwardLowenheimSkolemTheorem
Date of creation 2013-03-22 18:18:59
Last modified on 2013-03-22 18:18:59
Owner GodelsTheorem (21277)
Last modified by GodelsTheorem (21277)
Numerical id 14
Author GodelsTheorem (21277)
Entry type Proof
Classification msc 03C07