Standard Borel Structure on the Model Class

This file shows that ModelsOf φ (the set of coded ℕ-models of an Lω₁ω sentence φ) inherits StandardBorelSpace as a measurable subspace of the structure space.

Main Results

• modelsOf_isClopenable: ModelsOf φ is clopenable (admits a finer Polish topology making it clopen).
• modelsOf_standardBorel: The subtype ↥(ModelsOf φ) is standard Borel.

theorem FirstOrder.Language.modelsOf_isClopenable {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (φ : L.Sentenceω) : PolishSpace.IsClopenable (ModelsOf φ)

ModelsOf φ is clopenable in the structure space: there exists a finer Polish topology making it both open and closed. This follows from ModelsOf φ being measurable in a Polish + Borel space.

instance FirstOrder.Language.modelsOf_standardBorel {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (φ : L.Sentenceω) : StandardBorelSpace ↑(ModelsOf φ)

The subtype of coded ℕ-models of φ is standard Borel: it inherits a standard Borel structure as a measurable subspace of the standard Borel structure space.

@[reducible, inline]

abbrev FirstOrder.Language.ModelSpace {L : Language} [L.IsRelational] (φ : L.Sentenceω) : Type v

The space of coded ℕ-models of φ, as a standard Borel space.

Equations

• FirstOrder.Language.ModelSpace φ = ↑(FirstOrder.Language.ModelsOf φ)