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.