Satisfaction of Lω₁ω Formulas is Borel

This file proves that for a countable relational language L, the set of codes in StructureSpace L satisfying a given Lω₁ω sentence is measurable (Borel).

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

• modelsOfBounded_measurableSet: Satisfaction of any bounded Lω₁ω formula is measurable.
• 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.modelsOfBounded_measurableSet {L : Language} [L.IsRelational] {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α n) (v : α → ℕ) (xs : Fin n → ℕ) : MeasurableSet (ModelsOfBounded φ v xs)

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

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.