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.ModelsOfBoundedOn {L : Language} [L.IsRelational] {α : Type u_1} {β : Type u'} {n : ℕ} (φ : L.BoundedFormulaω β n) (v : β → α) (xs : Fin n → α) : Set (L.StructureSpaceOn α)

The set of codes in StructureSpaceOn L α where a bounded formula is realized, given variable assignments.

Equations

• FirstOrder.Language.ModelsOfBoundedOn φ v xs = {c : L.StructureSpaceOn α | φ.Realize v xs}

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.modelsOfBoundedOn_measurableSet {L : Language} [L.IsRelational] {α : Type u_1} [Countable α] {β : Type u'} {n : ℕ} (φ : L.BoundedFormulaω β n) (v : β → α) (xs : Fin n → α) : MeasurableSet (ModelsOfBoundedOn φ v xs)

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

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.