Logic and foundations · existing Mathlib declaration
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
The theorem at a glance
Downward Löwenheim–Skolem theorem at a glance
A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.
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.
Formal orientation
Statement map
This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is 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.
Complementary intuition
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.
The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.
Authoritative formal type
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} κSelected evidence declaration text
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} κProofAtlas record
What has been checked
These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.
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.
Provenance
Origin and evidence stay separate
- Existing declaration
FirstOrder.Language.exists_elementarySubstructure_card_eqin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Preferred checked artifact
artifact.library.mathlib.downward-lowenheim-skolem-theorem.v001- Source handling
- Verified upstream reference; no mirrored source package