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.

The isomorphism relation isoSetoid this file counts is defined in Descriptive/StructureIsoSetoid.lean, as the restriction of the ambient relation on StructureSpace L.

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.

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^ℵ₀.