Skolem Functions and Downward Löwenheim–Skolem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

@[simp]

theorem first_order.language.skolem₁_functions (L : first_order.language) (n : ℕ) :

L.skolem₁.functions n = L.bounded_formula empty (n + 1)

source

def first_order.language.skolem₁ (L : first_order.language) :

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

L.skolem₁ = {functions := λ (n : ℕ), L.bounded_formula empty (n + 1), relations := λ (_x : ℕ), empty}

Instances for first_order.language.skolem₁

first_order.language.skolem₁_Structure

source

@[simp]

theorem first_order.language.skolem₁_relations (L : first_order.language) (_x : ℕ) :

L.skolem₁.relations _x = empty

source

theorem first_order.language.card_functions_sum_skolem₁ {L : first_order.language} :

cardinal.mk (Σ (n : ℕ), (L.sum L.skolem₁).functions n) = cardinal.mk (Σ (n : ℕ), L.bounded_formula empty (n + 1))

source

theorem first_order.language.card_functions_sum_skolem₁_le {L : first_order.language} :

cardinal.mk (Σ (n : ℕ), (L.sum L.skolem₁).functions n) ≤ linear_order.max cardinal.aleph_0 L.card

source

@[protected, instance]

noncomputable def first_order.language.skolem₁_Structure {L : first_order.language} {M : Type w} [nonempty M] [L.Structure M] :

L.skolem₁.Structure M

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

Equations

first_order.language.skolem₁_Structure = {fun_map := λ (n : ℕ) (φ : L.skolem₁.functions n) (x : fin n → M), classical.epsilon (λ (a : M), first_order.language.bounded_formula.realize φ inhabited.default (fin.snoc x a)), rel_map := λ (_x : ℕ) (r : L.skolem₁.relations _x), empty.elim r}

source

theorem first_order.language.substructure.skolem₁_reduct_is_elementary {L : first_order.language} {M : Type w} [nonempty M] [L.Structure M] (S : (L.sum L.skolem₁).substructure M) :

(⇑(first_order.language.Lhom.sum_inl.substructure_reduct) S).is_elementary

source

noncomputable def first_order.language.substructure.elementary_skolem₁_reduct {L : first_order.language} {M : Type w} [nonempty M] [L.Structure M] (S : (L.sum L.skolem₁).substructure M) :

L.elementary_substructure M

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

Equations

S.elementary_skolem₁_reduct = {to_substructure := ⇑(first_order.language.Lhom.sum_inl.substructure_reduct) S, is_elementary' := _}

Instances for ↥first_order.language.substructure.elementary_skolem₁_reduct

first_order.language.elementary_skolem₁_reduct.small

source

theorem first_order.language.substructure.coe_sort_elementary_skolem₁_reduct {L : first_order.language} {M : Type w} [nonempty M] [L.Structure M] (S : (L.sum L.skolem₁).substructure M) :

↥(S.elementary_skolem₁_reduct) = ↥S

source

@[protected, instance]

def first_order.language.elementary_skolem₁_reduct.small (L : first_order.language) (M : Type w) [nonempty M] [L.Structure M] :

small ↥(⊥.elementary_skolem₁_reduct)

source

theorem first_order.language.exists_small_elementary_substructure (L : first_order.language) (M : Type w) [nonempty M] [L.Structure M] :

∃ (S : L.elementary_substructure M), small ↥S

source

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 : L.elementary_substructure M), 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 κ.