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 corollary mk_le_of_functions_le under |Σ Functions| ≤ max ℵ₀ |A|; the countable corollary is exists_countable_aElementary_substructure. The file is stated for Language.{0,0} and Type 0 carriers — the consumers' setting.

The witness sets and the hull

def FirstOrder.Language.tvWitnessSet {L : Language} {M : Type} [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} [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} [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} [L.Structure M] (A : L.Fragment) (X : Set M) : Monotone (lsStage A X)

def FirstOrder.Language.lsHull {L : Language} {M : Type} [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} [L.Structure M] (A : L.Fragment) (X : Set M) : X ⊆ ↑(lsHull A X)

theorem FirstOrder.Language.coe_lsHull {L : Language} {M : Type} [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} [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} [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} (A : L.Fragment) (Y : Set M) (n : ℕ) : Type

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} [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} [L.Structure M] (A : L.Fragment) (Y : Set M) : tvWitnessSet A Y ⊆ ⋃ (n : ℕ), some ⁻¹' Set.range (tvSliceWitness A Y n)

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

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

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

The honest per-stage bound.

theorem FirstOrder.Language.mk_lsHull_le {L : Language} {M : Type} [L.Structure M] (A : L.Fragment) (X : Set M) : Cardinal.mk ↥(lsHull A X) ≤ max (max Cardinal.aleph0 (Cardinal.mk ↑X)) (max (Cardinal.mk ↑A.toSet) (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} [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)))

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_countable_aElementary_substructure {L : Language} {M : Type} [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.