Conditional Counting Dichotomy for Models

This file states the Silver–Burgess dichotomy as an explicit hypothesis, defines the isomorphism equivalence relation on coded ℕ-models, and derives a conditional counting theorem: for Lω₁ω sentences whose ℕ-models have bounded Scott height, the number of isomorphism classes is either ≤ ℵ₀ or exactly 2^ℵ₀.

Main Definitions

• SilverBurgessDichotomy: The Silver–Burgess dichotomy for Borel equivalence relations on standard Borel spaces.
• isoSetoid: The isomorphism equivalence relation on ↥(ModelsOf φ).

Main Results

• counting_coded_models_dichotomy: Conditional on SilverBurgessDichotomy, for any Lω₁ω sentence with bounded Scott height, the number of isomorphism classes among coded ℕ-models is either ≤ ℵ₀ or exactly 2^ℵ₀.

def FirstOrder.Language.SilverBurgessDichotomy : Prop

The Silver–Burgess dichotomy for Borel equivalence relations: on a standard Borel space, a Borel equivalence relation has either at most countably many classes or exactly continuum-many.

Equations

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

def FirstOrder.Language.isoSetoid {L : Language} [L.IsRelational] (φ : L.Sentenceω) : Setoid ↑(ModelsOf φ)

The isomorphism equivalence relation on coded ℕ-models of φ. Two codes are related iff the decoded structures on ℕ are L-isomorphic.

Equations

• FirstOrder.Language.isoSetoid φ = { r := fun (c₁ c₂ : ↑(FirstOrder.Language.ModelsOf φ)) => Nonempty (L.Equiv ℕ ℕ), iseqv := ⋯ }

theorem FirstOrder.Language.counting_coded_models_dichotomy {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (silver : SilverBurgessDichotomy) {φ : L.Sentenceω} {α : Ordinal.{0}} (hα : α < Ordinal.omega 1) (hbound : ∀ (M : Type) [inst : L.Structure M] [inst_1 : Countable M], φ.Realize M → scottHeight M ≤ α) : Cardinal.mk (Quotient (isoSetoid φ)) ≤ Cardinal.aleph0 ∨ Cardinal.mk (Quotient (isoSetoid φ)) = Cardinal.continuum

Conditional counting theorem for ℕ-models with bounded Scott height: if the Silver–Burgess dichotomy holds, then for any Lω₁ω sentence whose ℕ-models all have Scott height ≤ α < ω₁, the number of isomorphism classes among ℕ-models of φ is either ≤ ℵ₀ or exactly 2^ℵ₀.