# 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 : ) :
L.skolem₁.Functions n = L.BoundedFormula Empty (n + 1)
@[simp]
theorem FirstOrder.Language.skolem₁_Relations (L : FirstOrder.Language) :
∀ (x : ), L.skolem₁.Relations x = Empty

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
• L.skolem₁ = { Functions := fun (n : ) => L.BoundedFormula Empty (n + 1), Relations := fun (x : ) => Empty }
Instances For
theorem FirstOrder.Language.card_functions_sum_skolem₁ {L : FirstOrder.Language} :
Cardinal.mk ((n : ) × (L.sum L.skolem₁).Functions n) = Cardinal.mk ((n : ) × L.BoundedFormula Empty (n + 1))
noncomputable instance FirstOrder.Language.skolem₁Structure {L : FirstOrder.Language} {M : Type w} [] [L.Structure M] :
L.skolem₁.Structure 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} [] [L.Structure M] (S : (L.sum L.skolem₁).Substructure M) :
(FirstOrder.Language.LHom.sumInl.substructureReduct S).IsElementary
noncomputable def FirstOrder.Language.Substructure.elementarySkolem₁Reduct {L : FirstOrder.Language} {M : Type w} [] [L.Structure M] (S : (L.sum L.skolem₁).Substructure M) :
L.ElementarySubstructure M

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

Equations
• S.elementarySkolem₁Reduct = { toSubstructure := FirstOrder.Language.LHom.sumInl.substructureReduct S, isElementary' := }
Instances For
theorem FirstOrder.Language.Substructure.coeSort_elementarySkolem₁Reduct {L : FirstOrder.Language} {M : Type w} [] [L.Structure M] (S : (L.sum L.skolem₁).Substructure M) :
S.elementarySkolem₁Reduct = S
instance FirstOrder.Language.Substructure.elementarySkolem₁Reduct.instSmall (L : FirstOrder.Language) (M : Type w) [] [L.Structure M] :
Small.{max u v, w} .elementarySkolem₁Reduct
Equations
• =
theorem FirstOrder.Language.exists_small_elementarySubstructure (L : FirstOrder.Language) (M : Type w) [] [L.Structure M] :
∃ (S : L.ElementarySubstructure M),
theorem FirstOrder.Language.exists_elementarySubstructure_card_eq (L : FirstOrder.Language) {M : Type w} [] [L.Structure M] (s : Set M) (κ : Cardinal.{w'}) (h1 : ) (h2 : ) (h3 : ) (h4 : ) :
∃ (S : L.ElementarySubstructure M), s S =

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 κ.