Theorems · Theorem · logic and foundations

FirstOrder.Language.exists_elementarilyEquivalent_card_eq

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

A consequence of the Löwenheim–Skolem Theorem: If κ is a cardinal greater than the cardinalities of L and an infinite L-structure M, then there is a structure of cardinality κ elementarily equivalent to M.

Defined in

Mathlib.ModelTheory.Satisfiability

Cited by

2 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureInfinite