Theorems · Theorem · logic and foundations

FirstOrder.Language.exists_elementaryEmbedding_card_eq

• 1000+ list: Löwenheim–Skolem theorem

∀ (L : FirstOrder.Language) (M : Type w') [inst : L.Structure M] [iM : Infinite M] (κ : Cardinal.{w}),
  Cardinal.aleph0 ≤ κ →
    Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ →
      ∃ N, (Nonempty (L.ElementaryEmbedding (↑N) M) ∨ Nonempty (L.ElementaryEmbedding M ↑N)) ∧ Cardinal.mk ↑N = κ

The Löwenheim–Skolem Theorem: If κ is a cardinal greater than the cardinalities of L and an infinite L-structure M, then there is an elementary embedding in the appropriate direction between then M and a structure of cardinality κ.

Defined in

Mathlib.ModelTheory.Satisfiability

Cited by

1 results in Mathlib

Foundations

Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.StructureInfinite