# mathlibdocumentation

model_theory.skolem

# Skolem Functions and Downward Löwenheim–Skolem #

## Main Definitions #

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

## Main Results #

• first_order.language.exists_elementary_substructure_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.

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
Instances for first_order.language.skolem₁
@[protected, instance]

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

Equations

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

Equations
Instances for ↥first_order.language.substructure.elementary_skolem₁_reduct
@[protected, instance]
theorem first_order.language.exists_elementary_substructure_card_eq (L : first_order.language) {M : Type w} [nonempty M] [L.Structure M] (s : set M) (κ : cardinal) (h1 : cardinal.aleph_0 κ) (h2 : (cardinal.mk s).lift κ.lift) (h3 : L.card.lift κ.lift) (h4 : κ.lift (cardinal.mk M).lift) :
∃ (S : , s S (cardinal.mk S).lift = κ.lift

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