Documentation

Mathlib.ModelTheory.Skolem

Skolem Functions and Downward Löwenheim–Skolem #

Main Definitions #

Main Results #

TODO #

source
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
  • L.skolem₁ = { Functions := fun (n : ℕ) => L.BoundedFormula Empty (n + 1), Relations := fun (x : ℕ) => Empty }
Instances For
    source
    @[simp]
    theorem FirstOrder.Language.skolem₁_Functions (L : FirstOrder.Language) (n : ℕ) :
    L.skolem₁.Functions n = L.BoundedFormula Empty (n + 1)
    source
    @[simp]
    theorem FirstOrder.Language.skolem₁_Relations (L : FirstOrder.Language) (x✝ : ℕ) :
    L.skolem₁.Relations x✝ = Empty
    source
    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))
    source
    theorem FirstOrder.Language.card_functions_sum_skolem₁_le {L : FirstOrder.Language} :
    Cardinal.mk ((n : ℕ) × (L.sum L.skolem₁).Functions n) ≤ Cardinal.aleph0 ⊔ L.card
    source
    noncomputable instance FirstOrder.Language.skolem₁Structure {L : FirstOrder.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
    • One or more equations did not get rendered due to their size.
    source
    theorem FirstOrder.Language.Substructure.skolem₁_reduct_isElementary {L : FirstOrder.Language} {M : Type w} [Nonempty M] [L.Structure M] (S : (L.sum L.skolem₁).Substructure M) :
    (FirstOrder.Language.LHom.sumInl.substructureReduct S).IsElementary
    source
    noncomputable def FirstOrder.Language.Substructure.elementarySkolem₁Reduct {L : FirstOrder.Language} {M : Type w} [Nonempty M] [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
      source
      theorem FirstOrder.Language.Substructure.coeSort_elementarySkolem₁Reduct {L : FirstOrder.Language} {M : Type w} [Nonempty M] [L.Structure M] (S : (L.sum L.skolem₁).Substructure M) :
      ↥S.elementarySkolem₁Reduct = ↥S
      source
      instance FirstOrder.Language.Substructure.elementarySkolem₁Reduct.instSmall (L : FirstOrder.Language) (M : Type w) [Nonempty M] [L.Structure M] :
      Small.{max u v, w} ↥⊥.elementarySkolem₁Reduct
      source
      theorem FirstOrder.Language.exists_small_elementarySubstructure (L : FirstOrder.Language) (M : Type w) [Nonempty M] [L.Structure M] :
      ∃ (S : L.ElementarySubstructure M), Small.{max u v, w} ↥S
      source
      theorem FirstOrder.Language.exists_elementarySubstructure_card_eq (L : FirstOrder.Language) {M : Type w} [Nonempty M] [L.Structure 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} L.card ≤ Cardinal.lift.{max u v, w'} κ) (h4 : Cardinal.lift.{w, w'} κ ≤ Cardinal.lift.{w', w} (Cardinal.mk M)) :
      ∃ (S : L.ElementarySubstructure 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 κ.