Genuine downward Löwenheim–Skolem for fragments (issue #13 unit 5)

Per the frozen audit (docs/fragments-audit.md §5–§6): from an arbitrary M and X ⊆ M, construct an A-elementary substructure containing X with the HONEST cardinal bound

|N| ≤ max(ℵ₀, |X|, |A|, |Σ n, L.Functions n|).

The construction is the semantic witness hull (Marker, Exercise 1.23, presented with choice functions instead of a language expansion): interleave Substructure.closure (all language functions — this is where |Σ Functions| honestly enters) with chosen witnesses for failures of the fragment-controlled universals (tvWitnessSet — |A|-many witness suppliers), iterate ω times, and close once more. The union is closed under both, so the Tarski–Vaught criterion (aElementary_of_tarskiVaught) applies. Witnesses are extracted from existence proofs (Exists.choose), so no Nonempty M hypothesis and no dummy elements are needed.

Marker's textbook bound max(|A|,|X|) (Theorem 1.22) is the special case |Σ Functions| ≤ max ℵ₀ |A|; the countable corollary, which is what the consumers use, is exists_countable_aElementary_substructure.

The language's two universes and the carrier's are independent. The three cardinals being compared therefore start in three different universes, so every bound is stated with an explicit Cardinal.lift into max u v w. exists_aElementary_substructure_of_eq_univ is the same-universe form, where those lifts are identities.

The witness sets and the hull

def FirstOrder.Language.tvWitnessSet {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (Y : Set M) : Set M

The chosen witnesses over a base set Y: for each fragment-controlled universal and each tuple from Y admitting a counterexample in M, THE chosen counterexample.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.lsStage {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (X : Set M) : ℕ → Set M

The Löwenheim–Skolem stages: alternately close under all language functions and add the fragment witnesses.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.lsStage A X 0 = X

theorem FirstOrder.Language.lsStage_mono {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (X : Set M) (k : ℕ) : lsStage A X k ⊆ lsStage A X (k + 1)

theorem FirstOrder.Language.lsStage_mono_le {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (X : Set M) : Monotone (lsStage A X)

def FirstOrder.Language.lsHull {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (X : Set M) : L.Substructure M

The witness hull: the substructure generated by all stages.

Equations

• FirstOrder.Language.lsHull A X = (FirstOrder.Language.Substructure.closure L).toFun (⋃ (k : ℕ), FirstOrder.Language.lsStage A X k)

theorem FirstOrder.Language.subset_lsHull {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (X : Set M) : X ⊆ ↑(lsHull A X)

theorem FirstOrder.Language.coe_lsHull {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (X : Set M) : ↑(lsHull A X) = ⋃ (k : ℕ), ↑((Substructure.closure L).toFun (lsStage A X k))

The hull's carrier is the union of the stage closures — directedness makes the last closure redundant.

theorem FirstOrder.Language.exists_stage_of_tuple {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) {X : Set M} {n : ℕ} (a : Fin n → ↥(lsHull A X)) : ∃ (K : ℕ), ∀ (i : Fin n), ↑(a i) ∈ ↑((Substructure.closure L).toFun (lsStage A X K))

Finitely many hull elements lie in a common stage closure.

theorem FirstOrder.Language.aElementary_lsHull {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (X : Set M) : AElementary A (lsHull A X).subtype

The hull is A-elementary — the Tarski–Vaught criterion holds by construction.

The cardinal bound

def FirstOrder.Language.tvSlice {L : Language} {M : Type w} (A : L.Fragment) (Y : Set M) (n : ℕ) : Type (max u v w)

The per-arity witness suppliers: fragment-controlled bodies paired with tuples from Y.

Equations

• FirstOrder.Language.tvSlice A Y n = { q : L.BoundedFormulaω Empty (n + 1) × (Fin n → M) // ⟨n, q.1.all⟩ ∈ A.toSet ∧ ∀ (i : Fin n), q.2 i ∈ Y }

noncomputable def FirstOrder.Language.tvSliceWitness {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (Y : Set M) (n : ℕ) : tvSlice A Y n → Option M

The choice map from a slice: the chosen counterexample, when one exists.

Equations

• FirstOrder.Language.tvSliceWitness A Y n q = if h : ∃ (m' : M), ¬(↑q).1.Realize Empty.elim (Fin.snoc (↑q).2 m') then some h.choose else none

theorem FirstOrder.Language.tvWitnessSet_subset_iUnion {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (Y : Set M) : tvWitnessSet A Y ⊆ ⋃ (n : ℕ), some ⁻¹' Set.range (tvSliceWitness A Y n)

Mathlib's heterogeneous-universe lemmas produce the complementary lift level: for a set in M they give lift.{max u v}, and for language-side data lift.{w}. Both land in Cardinal.{max u v w}, but Lean keeps the level expressions distinct, so every bound below is stated with the uniform lift.{max u v w} and converted once through these.

theorem FirstOrder.Language.mk_tvSlice_le {L : Language} {M : Type w} (A : L.Fragment) (Y : Set M) (n : ℕ) : Cardinal.mk (tvSlice A Y n) ≤ max (max Cardinal.aleph0 (Cardinal.lift.{max u v w, w} (Cardinal.mk ↑Y))) (Cardinal.lift.{max u v w, max u v} (Cardinal.mk ↑A.toSet))

theorem FirstOrder.Language.mk_tvWitnessSet_le {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (Y : Set M) : Cardinal.lift.{max u v w, w} (Cardinal.mk ↑(tvWitnessSet A Y)) ≤ max (max Cardinal.aleph0 (Cardinal.lift.{max u v w, w} (Cardinal.mk ↑Y))) (Cardinal.lift.{max u v w, max u v} (Cardinal.mk ↑A.toSet))

theorem FirstOrder.Language.lift_mk_closure_le {L : Language} {M : Type w} [L.Structure M] (S : Set M) {κ : Cardinal.{max u v w}} (hκ : Cardinal.aleph0 ≤ κ) (hS : Cardinal.lift.{max u v w, w} (Cardinal.mk ↑S) ≤ κ) (hF : Cardinal.lift.{max u v w, u} (Cardinal.mk ((n : ℕ) × L.Functions n)) ≤ κ) : Cardinal.lift.{max u v w, w} (Cardinal.mk ↑↑((Substructure.closure L).toFun S)) ≤ κ

The substructure-closure bound is lifted into the common universe max u v w. Mathlib's own statement lives in Cardinal.{max u w}, so it needs one further lift, and the function-symbol summand arrives with the complementary level.

theorem FirstOrder.Language.mk_lsStage_le {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (X : Set M) (k : ℕ) : Cardinal.lift.{max u v w, w} (Cardinal.mk ↑(lsStage A X k)) ≤ max (max Cardinal.aleph0 (Cardinal.lift.{max u v w, w} (Cardinal.mk ↑X))) (max (Cardinal.lift.{max u v w, max u v} (Cardinal.mk ↑A.toSet)) (Cardinal.lift.{max u v w, u} (Cardinal.mk ((n : ℕ) × L.Functions n))))

The honest per-stage bound.

theorem FirstOrder.Language.mk_lsHull_le {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (X : Set M) : Cardinal.lift.{max u v w, w} (Cardinal.mk ↥(lsHull A X)) ≤ max (max Cardinal.aleph0 (Cardinal.lift.{max u v w, w} (Cardinal.mk ↑X))) (max (Cardinal.lift.{max u v w, max u v} (Cardinal.mk ↑A.toSet)) (Cardinal.lift.{max u v w, u} (Cardinal.mk ((n : ℕ) × L.Functions n))))

The honest hull bound: |N| ≤ max(ℵ₀, |X|, |A|, |Σ Functions|).

theorem FirstOrder.Language.exists_aElementary_substructure {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (X : Set M) : ∃ (N : L.Substructure M), X ⊆ ↑N ∧ AElementary A N.subtype ∧ Cardinal.lift.{max u v w, w} (Cardinal.mk ↥N) ≤ max (max Cardinal.aleph0 (Cardinal.lift.{max u v w, w} (Cardinal.mk ↑X))) (max (Cardinal.lift.{max u v w, max u v} (Cardinal.mk ↑A.toSet)) (Cardinal.lift.{max u v w, u} (Cardinal.mk ((n : ℕ) × L.Functions n))))

Genuine downward Löwenheim–Skolem for fragments (issue #13 unit 5): every X ⊆ M is contained in an A-elementary substructure of size at most max(ℵ₀, |X|, |A|, |Σ Functions|) — the honest bound; only function symbols enlarge the hull beyond the fragment's witnesses.

theorem FirstOrder.Language.exists_aElementary_substructure_of_eq_univ {L : Language} {M : Type u} [L.Structure M] (A : L.Fragment) (X : Set M) : ∃ (N : L.Substructure M), X ⊆ ↑N ∧ AElementary A N.subtype ∧ Cardinal.mk ↥N ≤ max (max Cardinal.aleph0 (Cardinal.mk ↑X)) (max (Cardinal.mk ↑A.toSet) (Cardinal.mk ((n : ℕ) × L.Functions n)))

The same-universe form, for a language and a structure that already share one universe: the lifts are then all identities, so this is the statement without the universe bookkeeping.

theorem FirstOrder.Language.exists_countable_aElementary_substructure {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) {X : Set M} (hX : X.Countable) (hA : A.toSet.Countable) [hF : Countable ((n : ℕ) × L.Functions n)] : ∃ (N : L.Substructure M), X ⊆ ↑N ∧ AElementary A N.subtype ∧ Countable ↥N

The countable corollary (Marker, Theorem 1.22 second half — what #17 consumes): countable data yields a countable A-elementary substructure.

Universe regression

These instantiate the hull construction and its cardinal bound where the language's two universes and the structure's universe are pairwise distinct, and at the same-universe specialization. They are compiled, so they fail if the file is ever reconstrained; the variable block alone would not catch that, since a Language.{u, v} binder can still be silently pinned by a downstream lemma.