Generic Satisfaction Measurability for Carrier-Parametric Structure Spaces

This file proves that satisfaction of Lω₁ω formulas is measurable on StructureSpaceOn L α for any encodable carrier α. This generalizes the ℕ-specific results in SatisfactionBorel.lean.

Main Definitions

• ModelsOfBoundedOn: The set of codes in StructureSpaceOn L α where a bounded formula is realized.
• ModelsOfOn: The set of codes where a sentence is realized.

Main Results

• modelsOfBoundedOn_measurableSet: Satisfaction of any bounded Lω₁ω formula is measurable on StructureSpaceOn L α.
• modelsOfOn_measurableSet: Satisfaction of any Lω₁ω sentence is measurable.

theorem FirstOrder.Language.Term.eq_var_of_isRelational {L : Language} [L.IsRelational] {β : Type u_1} (t : L.Term β) : ∃ (x : β), t = var x

In a relational language, every term is a variable.

def FirstOrder.Language.ModelsOfOn {L : Language} [L.IsRelational] {α : Type u_1} (φ : L.Sentenceω) : Set (L.StructureSpaceOn α)

The set of codes in StructureSpaceOn L α where a sentence is realized.

Equations

• FirstOrder.Language.ModelsOfOn φ = FirstOrder.Language.ModelsOfBoundedOn✝ φ Empty.elim Fin.elim0

theorem FirstOrder.Language.modelsOfOn_measurableSet {L : Language} [L.IsRelational] {α : Type u_1} [Countable α] (φ : L.Sentenceω) : MeasurableSet (ModelsOfOn φ)

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