Satisfaction of Lω₁ω Formulas is Borel

This file specializes the carrier-parametric result to structures on ℕ.

Main Definitions

• ModelsOfBounded: The set of codes where a bounded formula is realized.
• ModelsOf: The set of codes where a sentence is realized.

Main Results

• modelsOf_measurableSet: Satisfaction of any Lω₁ω sentence is measurable.

def FirstOrder.Language.ModelsOfBounded {L : Language} [L.IsRelational] {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α n) (v : α → ℕ) (xs : Fin n → ℕ) : Set L.StructureSpace

The set of codes where a bounded formula is realized, given variable assignments.

Equations

• FirstOrder.Language.ModelsOfBounded φ v xs = {c : L.StructureSpace | φ.Realize v xs}

def FirstOrder.Language.ModelsOf {L : Language} [L.IsRelational] (φ : L.Sentenceω) : Set L.StructureSpace

The set of codes where a sentence is realized.

Equations

• FirstOrder.Language.ModelsOf φ = FirstOrder.Language.ModelsOfBounded φ Empty.elim Fin.elim0

theorem FirstOrder.Language.modelsOf_measurableSet {L : Language} [L.IsRelational] (φ : L.Sentenceω) : MeasurableSet (ModelsOf φ)

Satisfaction of any Lω₁ω sentence in a countable relational language is measurable on the structure space.