Few models from level-by-level smallness of the back-and-forth hierarchy

mk_isoSetoid_quotient_le_aleph_one bounds the isomorphism classes of coded models of a sentence by ℵ₁ once every back-and-forth level below ω₁ has countably many classes. This module assembles the level-by-level analysis that produces such bounds from local data, for an arbitrary class C of coded models and every tuple arity at once:

• at level 0, countably many depth-0 classes of n-tuples — an assumption, not a consequence of a countable language, since the atomic type of a tuple is a subset of a countable set of atomic formulas and may a priori take continuum many values;
• at a successor, countably many realized extension spectra (bfExtensionSpectra), which by countable_bfTupleQuotient_succ carry countability up one level;
• at a limit, pointwise isolation from the lower levels (Setoid.IsolatedBy), which by Setoid.countable_quotient_of_isolatedBy carries countability through the limit.

Main results

• BFSmall φ C — the three local smallness conditions.
• countable_bfTupleQuotient_of_bfSmall — the transfinite induction: every level α < ω₁ has countably many classes at every arity.
• countable_bfProjRange_representedIn — the arity-0 classes of C-models cover the depth-α projection of the isomorphism classes represented in C (RepresentedIn).
• mk_representedIn_le_aleph_one_of_bfSmall — hence, by the relativized stratification bound mk_isoSetoid_subtype_le_aleph_one_of_countable_levels, the isomorphism classes represented in C number at most ℵ₁; mk_isoSetoid_quotient_le_aleph_one_of_bfSmall is the case C := Set.univ.

structure FirstOrder.Language.BFSmall {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) : Prop

Level-by-level smallness of a class C of coded models: countably many depth-0 classes at every arity; countably many realized extension spectra at every depth α < ω₁ and arity; pointwise isolation from the lower levels at every limit λ < ω₁ and arity.

• zero (n : ℕ) : Countable (Quotient (bfTupleSetoid φ C 0 n))

  Countably many depth-0 classes of n-tuples.

• succ (α : Ordinal.{0}) : α < Ordinal.omega 1 → ∀ (n : ℕ), Countable ↑(bfExtensionSpectra φ C α n)

  Countably many realized depth-α extension spectra of n-tuples.

• limit (lam : Ordinal.{0}) : lam < Ordinal.omega 1 → Order.IsSuccLimit lam → ∀ (n : ℕ), Setoid.IsolatedBy (fun (β : ↑(Set.Iio lam)) => bfTupleSetoid φ C (↑β) n) (bfTupleSetoid φ C lam n)

  Pointwise isolation from the lower levels at every limit.

theorem FirstOrder.Language.countable_bfTupleQuotient_of_bfSmall {L : Language} [L.IsRelational] {φ : L.Sentenceω} {C : Set ↑(ModelsOf φ)} (h : BFSmall φ C) {α : Ordinal.{0}} (hα : α < Ordinal.omega 1) (n : ℕ) : Countable (Quotient (bfTupleSetoid φ C α n))

The transfinite induction: under BFSmall, every level below ω₁ has countably many classes at every arity.

def FirstOrder.Language.RepresentedIn {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (q : Quotient (isoSetoid φ)) : Prop

The isomorphism classes represented in C.

Equations

• FirstOrder.Language.RepresentedIn φ C q = ∃ c ∈ C, ⟦c⟧ = q

theorem FirstOrder.Language.countable_bfProjRange_representedIn {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (α : Ordinal.{0}) (hcount : Countable (Quotient (bfTupleSetoid φ C α 0))) : Countable ↑(bfProjRange φ (RepresentedIn φ C) α)

The arity-0 bridge: the depth-α classes of C-models (with the empty tuple) map onto the depth-α projection of the isomorphism classes represented in C.

theorem FirstOrder.Language.mk_representedIn_le_aleph_one_of_bfSmall {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} {C : Set ↑(ModelsOf φ)} (h : BFSmall φ C) : Cardinal.mk { q : Quotient (isoSetoid φ) // RepresentedIn φ C q } ≤ Cardinal.aleph 1

Few models from smallness: under BFSmall φ C, the isomorphism classes represented in C number at most ℵ₁.

theorem FirstOrder.Language.mk_isoSetoid_quotient_le_aleph_one_of_bfSmall {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} (h : BFSmall φ Set.univ) : Cardinal.mk (Quotient (isoSetoid φ)) ≤ Cardinal.aleph 1

The case C := Set.univ: level-by-level smallness of all coded models of φ gives at most ℵ₁ isomorphism classes — the hypothesis of mk_isoSetoid_quotient_le_aleph_one obtained from local data.