The witness hull and downward Löwenheim–Skolem for fragments

Let A be a fragment of L_{ω₁ω}, M an L-structure and X ⊆ M. Then X lies in an A-elementary substructure of M, its witness hull, with at most max ℵ₀ |X| |A| |Σ n, L.Functions n| elements. Neither M nor X need be nonempty. The function symbols enter the bound separately, because a fragment need not contain an atomic formula mentioning them. The three cardinals start in the universes of M, of the formulas and of the function symbols, and are compared after lifting into their common universe.

For a formation-closed fragment the bound is Marker's max |X| |A|. This is a corollary of the same construction, not a new one: such a fragment is infinite, since it contains ⊥ at every arity and formulas are tagged with their arity, and it has at least as many members as there are function symbols, so both ℵ₀ and the function-symbol term are absorbed by |A|.

Main definitions

• FirstOrder.Language.Fragment.witnessHull: the witness hull of a set.
• FirstOrder.Language.Fragment.witness, FirstOrder.Language.Fragment.witnessSet and FirstOrder.Language.Fragment.hullStage: the chosen counterexamples and the stages of the hull.

Main results

• FirstOrder.Language.Fragment.aElementary_witnessHull: the witness hull is A-elementary.
• FirstOrder.Language.Fragment.lift_mk_witnessHull_le: its cardinal bound.
• FirstOrder.Language.exists_aElementary_substructure: downward Löwenheim–Skolem for fragments.
• FirstOrder.Language.exists_countable_aElementary_substructure: the countable form.
• FirstOrder.Language.exists_aElementary_substructure_of_eq_univ: the form in one universe.
• FirstOrder.Language.Fragment.FormationClosed.exists_aElementary_substructure: the bound max |X| |A| for a formation-closed fragment.

References

• D. Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, Chapter 1, Theorem 1.22 and Exercise 1.23.
• Ported from cameronfreer/infinitary-logic at commit 518a366cba97b1ae8c4dc64a297a396939bc3e0b, InfinitaryLogic/ModelTheory/FragmentLowenheimSkolem.lean.
• Divergences from that source: the chosen counterexamples come from one partial choice function on the members of A and tuples, and their number is bounded by an injection into A × List Y, rather than by per-arity slices; the hull is the directed supremum of the stage closures; the bounds are stated for an abstract infinite cardinal bounding the inputs, each lifted from its own universe.

noncomputable def FirstOrder.Language.Fragment.witness {L : Language} {M : Type w} [L.Structure M] (p : (n : ℕ) × L.BoundedFormulaω Empty n) : (Fin p.fst → M) → Option M

The chosen counterexample to a universal formula ∀ x, φ at a tuple a, if φ has one; for every other formula, nothing.

theorem FirstOrder.Language.Fragment.witness_all {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (φ : L.BoundedFormulaω Empty (n + 1)) (a : Fin n → M) : witness ⟨n, BoundedFormulaInf.all φ⟩ a = if h : ∃ (m : M), ¬BoundedFormulaInf.Realize φ Empty.elim (Fin.snoc a m) then some h.choose else none

At a universal formula ∀ x, φ, the witness is the chosen counterexample to φ, if any.

theorem FirstOrder.Language.Fragment.witness_all_spec {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {φ : L.BoundedFormulaω Empty (n + 1)} {a : Fin n → M} {m : M} (h : witness ⟨n, BoundedFormulaInf.all φ⟩ a = some m) : ¬BoundedFormulaInf.Realize φ Empty.elim (Fin.snoc a m)

A chosen counterexample is a counterexample.

theorem FirstOrder.Language.Fragment.exists_witness_all {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {φ : L.BoundedFormulaω Empty (n + 1)} {a : Fin n → M} (hex : ∃ (m : M), ¬BoundedFormulaInf.Realize φ Empty.elim (Fin.snoc a m)) : ∃ (m : M), witness ⟨n, BoundedFormulaInf.all φ⟩ a = some m

A universal formula with a counterexample has a chosen one.

theorem FirstOrder.Language.Fragment.exists_eq_all_of_witness_eq_some {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {ψ : L.BoundedFormulaω Empty n} {a : Fin n → M} {m : M} (h : witness ⟨n, ψ⟩ a = some m) : ∃ (φ : L.BoundedFormulaω Empty (n + 1)), ψ = BoundedFormulaInf.all φ ∧ ¬BoundedFormulaInf.Realize φ Empty.elim (Fin.snoc a m)

A chosen witness is produced only for a universal formula ∀ x, φ, and is then a counterexample to φ.

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

The chosen counterexamples for the members of A at the tuples from Y.

@[simp]

theorem FirstOrder.Language.Fragment.mem_witnessSet {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) {Y : Set M} {m : M} : m ∈ A.witnessSet Y ↔ ∃ p ∈ A, ∃ (a : Fin p.fst → M), (∀ (i : Fin p.fst), a i ∈ Y) ∧ witness p a = some m

Membership in witnessSet: a chosen counterexample for a member of A at a tuple from Y.

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

The stages of the witness hull of X: alternately close under the function symbols and add, for each universal member ∀ x, φ of A and each tuple from the closure at which φ has a counterexample in M, a chosen counterexample.

@[simp]

theorem FirstOrder.Language.Fragment.hullStage_zero {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (X : Set M) : A.hullStage X 0 = X

The first stage of the witness hull of X is X.

@[simp]

theorem FirstOrder.Language.Fragment.hullStage_succ {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (X : Set M) (k : ℕ) : A.hullStage X (k + 1) = ↑((Substructure.closure L).toFun (A.hullStage X k)) ∪ A.witnessSet ↑((Substructure.closure L).toFun (A.hullStage X k))

The next stage adds to the closure of a stage its chosen counterexamples.

theorem FirstOrder.Language.Fragment.monotone_closure_hullStage {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) (X : Set M) : Monotone fun (k : ℕ) => (Substructure.closure L).toFun (A.hullStage X k)

The closures of the stages increase.

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

The witness hull of X: the union of the closures of its stages.

theorem FirstOrder.Language.Fragment.mem_witnessHull {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) {X : Set M} {m : M} : m ∈ A.witnessHull X ↔ ∃ (k : ℕ), m ∈ (Substructure.closure L).toFun (A.hullStage X k)

Membership in the witness hull is membership in the closure of some stage.

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

The witness hull contains its seed.

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

The witness hull is A-elementary, by the fragment Tarski–Vaught criterion.

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

The witness hull is the union of the closures of its stages.

The cardinal bound

Each step is bounded by an infinite cardinal κ in the common universe max u v w that bounds the seed, the fragment and the function symbols; the three start in different universes, so each is lifted into max u v w from its own.

theorem FirstOrder.Language.Fragment.lift_mk_witnessSet_le {L : Language} {M : Type w} [L.Structure M] {A : L.Fragment} {κ : Cardinal.{max u v w}} (hκ : Cardinal.aleph0 ≤ κ) (hA : Cardinal.lift.{w, max u v} (Cardinal.mk ↥A) ≤ κ) {Y : Set M} (hY : Cardinal.lift.{max u v, w} (Cardinal.mk ↑Y) ≤ κ) : Cardinal.lift.{max u v, w} (Cardinal.mk ↑(A.witnessSet Y)) ≤ κ

The chosen counterexamples at the tuples from a set of at most κ elements number at most κ, when κ also bounds the fragment.

theorem FirstOrder.Language.Fragment.lift_mk_hullStage_le {L : Language} {M : Type w} [L.Structure M] {A : L.Fragment} {κ : Cardinal.{max u v w}} (hκ : Cardinal.aleph0 ≤ κ) (hA : Cardinal.lift.{w, max u v} (Cardinal.mk ↥A) ≤ κ) (hF : Cardinal.lift.{max v w, u} (Cardinal.mk ((n : ℕ) × L.Functions n)) ≤ κ) {X : Set M} (hX : Cardinal.lift.{max u v, w} (Cardinal.mk ↑X) ≤ κ) (k : ℕ) : Cardinal.lift.{max u v, w} (Cardinal.mk ↑(A.hullStage X k)) ≤ κ

Each stage of the witness hull of X has at most κ elements.

theorem FirstOrder.Language.Fragment.lift_mk_witnessHull_le {L : Language} {M : Type w} [L.Structure M] {A : L.Fragment} {κ : Cardinal.{max u v w}} (hκ : Cardinal.aleph0 ≤ κ) (hA : Cardinal.lift.{w, max u v} (Cardinal.mk ↥A) ≤ κ) (hF : Cardinal.lift.{max v w, u} (Cardinal.mk ((n : ℕ) × L.Functions n)) ≤ κ) {X : Set M} (hX : Cardinal.lift.{max u v, w} (Cardinal.mk ↑X) ≤ κ) : Cardinal.lift.{max u v, w} (Cardinal.mk ↥(A.witnessHull X)) ≤ κ

The witness hull of X has at most κ elements.

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} (Cardinal.mk ↥N) ≤ max Cardinal.aleph0 (max (Cardinal.lift.{max u v, w} (Cardinal.mk ↑X)) (max (Cardinal.lift.{w, max u v} (Cardinal.mk ↥A)) (Cardinal.lift.{max v w, u} (Cardinal.mk ((n : ℕ) × L.Functions n)))))

Downward Löwenheim–Skolem for fragments. Every subset X of M lies in an A-elementary substructure with at most max ℵ₀ |X| |A| |Σ n, L.Functions n| elements.

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

Countable A-elementary substructures. With countably many function symbols, a countable fragment and a countable X ⊆ M, there is a countable A-elementary substructure containing X.

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 Cardinal.aleph0 (max (Cardinal.mk ↑X) (max (Cardinal.mk ↥A) (Cardinal.mk ((n : ℕ) × L.Functions n))))

Downward Löwenheim–Skolem for fragments, in one universe. For a language and a structure in one universe the bound needs no lifts.

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

Downward Löwenheim–Skolem for formation-closed fragments. For a formation-closed fragment A, every subset X of M lies in an A-elementary substructure with at most max |X| |A| elements: the fragment is infinite and has at least as many members as there are function symbols.