Skolem Functions and Downward Löwenheim–Skolem

Main Definitions

• FirstOrder.Language.skolem₁ is a language consisting of Skolem functions for another language.

Main Results

• FirstOrder.Language.exists_elementarySubstructure_card_eq is the Downward Löwenheim–Skolem theorem: If s is a set in an L-structure M and κ an infinite cardinal such that max (#s, L.card) ≤ κ and κ ≤ # M, then M has an elementary substructure containing s of cardinality κ.

TODO

• Use skolem₁ recursively to construct an actual Skolemization of a language.

@[simp]

theorem FirstOrder.Language.skolem₁_Functions (L : FirstOrder.Language) (n : ℕ) : (FirstOrder.Language.skolem₁ L).Functions n = FirstOrder.Language.BoundedFormula L Empty (n + 1)

@[simp]

theorem FirstOrder.Language.skolem₁_Relations (L : FirstOrder.Language) : ∀ (x : ℕ), (FirstOrder.Language.skolem₁ L).Relations x = Empty

def FirstOrder.Language.skolem₁ (L : FirstOrder.Language) : FirstOrder.Language

A language consisting of Skolem functions for another language. Called skolem₁ because it is the first step in building a Skolemization of a language.

Equations

• FirstOrder.Language.skolem₁ L = { Functions := fun (n : ℕ) => FirstOrder.Language.BoundedFormula L Empty (n + 1), Relations := fun (x : ℕ) => Empty }

theorem FirstOrder.Language.card_functions_sum_skolem₁ {L : FirstOrder.Language} : Cardinal.mk ((n : ℕ) × (FirstOrder.Language.sum L (FirstOrder.Language.skolem₁ L)).Functions n) = Cardinal.mk ((n : ℕ) × FirstOrder.Language.BoundedFormula L Empty (n + 1))

theorem FirstOrder.Language.card_functions_sum_skolem₁_le {L : FirstOrder.Language} : Cardinal.mk ((n : ℕ) × (FirstOrder.Language.sum L (FirstOrder.Language.skolem₁ L)).Functions n) ≤ max Cardinal.aleph0 (FirstOrder.Language.card L)

noncomputable instance FirstOrder.Language.skolem₁Structure {L : FirstOrder.Language} {M : Type w} [Nonempty M] [FirstOrder.Language.Structure L M] : FirstOrder.Language.Structure (FirstOrder.Language.skolem₁ L) M

The structure assigning each function symbol of L.skolem₁ to a skolem function generated with choice.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.Substructure.skolem₁_reduct_isElementary {L : FirstOrder.Language} {M : Type w} [Nonempty M] [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure (FirstOrder.Language.sum L (FirstOrder.Language.skolem₁ L)) M) : FirstOrder.Language.Substructure.IsElementary ((FirstOrder.Language.LHom.substructureReduct FirstOrder.Language.LHom.sumInl) S)

noncomputable def FirstOrder.Language.Substructure.elementarySkolem₁Reduct {L : FirstOrder.Language} {M : Type w} [Nonempty M] [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure (FirstOrder.Language.sum L (FirstOrder.Language.skolem₁ L)) M) : FirstOrder.Language.ElementarySubstructure L M

Any L.sum L.skolem₁-substructure is an elementary L-substructure.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.Substructure.coeSort_elementarySkolem₁Reduct {L : FirstOrder.Language} {M : Type w} [Nonempty M] [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure (FirstOrder.Language.sum L (FirstOrder.Language.skolem₁ L)) M) : ↥(FirstOrder.Language.Substructure.elementarySkolem₁Reduct S) = ↥S

instance FirstOrder.Language.Substructure.elementarySkolem₁Reduct.instSmall (L : FirstOrder.Language) (M : Type w) [Nonempty M] [FirstOrder.Language.Structure L M] : Small.{max u v, w} ↥(FirstOrder.Language.Substructure.elementarySkolem₁Reduct ⊥)

Equations

• (_ : Small.{max u v, w} ↥(FirstOrder.Language.Substructure.elementarySkolem₁Reduct ⊥)) = (_ : Small.{max u v, w} ↥(FirstOrder.Language.Substructure.elementarySkolem₁Reduct ⊥))

theorem FirstOrder.Language.exists_small_elementarySubstructure (L : FirstOrder.Language) (M : Type w) [Nonempty M] [FirstOrder.Language.Structure L M] : ∃ (S : FirstOrder.Language.ElementarySubstructure L M), Small.{max u v, w} ↥S

theorem FirstOrder.Language.exists_elementarySubstructure_card_eq (L : FirstOrder.Language) {M : Type w} [Nonempty M] [FirstOrder.Language.Structure L M] (s : Set M) (κ : Cardinal.{w'}) (h1 : Cardinal.aleph0 ≤ κ) (h2 : Cardinal.lift.{w', w} (Cardinal.mk ↑s) ≤ Cardinal.lift.{w, w'} κ) (h3 : Cardinal.lift.{w', max u v} (FirstOrder.Language.card L) ≤ Cardinal.lift.{max u v, w'} κ) (h4 : Cardinal.lift.{w, w'} κ ≤ Cardinal.lift.{w', w} (Cardinal.mk M)) : ∃ (S : FirstOrder.Language.ElementarySubstructure L M), s ⊆ ↑S ∧ Cardinal.lift.{w', w} (Cardinal.mk ↥S) = Cardinal.lift.{w, w'} κ

The Downward Löwenheim–Skolem theorem : If s is a set in an L-structure M and κ an infinite cardinal such that max (#s, L.card) ≤ κ and κ ≤ # M, then M has an elementary substructure containing s of cardinality κ.