Existing in Mathlib · Logic and foundations
Downward Löwenheim–Skolem Theorem
Start with a nonempty first-order structure M, a set s of elements that must be retained, and an infinite size κ. If both the seed and the language fit within κ, and κ itself fits within M, then M has an elementary substructure S that contains every element of s and has exactly size κ, with Mathlib's universe lifts made explicit.
- first-order structure
- elementary substructure
- Skolem functions
- cardinality
- universe lift
- model theory
Exact theorem
Exact Mathlib statement
theorem FirstOrder.Language.exists_elementarySubstructure_card_eq (L : FirstOrder.Language.{u, v}) {M : Type w} [Nonempty M] [L.Structure M] (s : Set M) (κ : Cardinal.{w'}) (h1 : ℵ₀ ≤ κ) (h2 : Cardinal.lift.{w'} #s ≤ Cardinal.lift.{w} κ) (h3 : Cardinal.lift.{w'} L.card ≤ Cardinal.lift.{max u v} κ) (h4 : Cardinal.lift.{w} κ ≤ Cardinal.lift.{w'} #M) : ∃ S : L.ElementarySubstructure M, s ⊆ S ∧ Cardinal.lift.{w'} #S = Cardinal.lift.{w} κThe theorem at a glance
Downward Löwenheim–Skolem theorem at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Downward Löwenheim–Skolem theorem at a glance
Detailed visual description
The poster keeps all four hypotheses visible above a nested M and S diagram, then follows the checked source route through Skolem functions, an ambient κ-sized set, closure in the expanded language, the elementary reduct, and the final cardinal squeeze.
Statement structure
From hypotheses to conclusion
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Downward Löwenheim–Skolem Theorem — scientific diagram
Detailed visual description
This target indexes Mathlib's Downward Löwenheim–Skolem theorem for a nonempty first-order L-structure M, a prescribed seed set s, and an infinite cardinal κ. After the explicit universe lifts, the seed and language cardinalities must be at most κ and κ must be at most the ambient cardinality. The endpoint gives an elementary L-substructure containing s with lifted cardinality exactly κ. It is not an unrestricted countable-submodel claim or the upward theorem.
Why it matters
A mathematical landmark
The theorem is a central size-control principle of model theory: elementary truth can be retained inside a substructure whose cardinality is chosen exactly within explicit seed, language, and ambient bounds.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This target indexes Mathlib's Downward Löwenheim–Skolem theorem for a nonempty first-order L-structure M, a prescribed seed set s, and an infinite cardinal κ. After the explicit universe lifts, the seed and language cardinalities must be at most κ and κ must be at most the ambient cardinality. The endpoint gives an elementary L-substructure containing s with lifted cardinality exactly κ. It is not an unrestricted countable-submodel claim or the upward theorem.
- Proof Atlas did not originate the Downward Löwenheim–Skolem theorem or Mathlib's declaration.
- The theorem does not give a countable elementary substructure unless the displayed hypotheses permit choosing the relevant cardinal to be countable.
- The selected declaration is not the upward Löwenheim–Skolem theorem and does not construct a larger elementary extension.
- The theorem does not make the elementary substructure unique, canonical, proper, or algorithmically computable.
- The generated explanation and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
FirstOrder.Language.exists_elementarySubstructure_card_eqin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.downward-lowenheim-skolem-theorem.v001