Measurable Structure on the Structure Space

This file equips StructureSpace L with a MeasurableSpace structure, derived from the product measurable space on RelQuery L → Bool. The key result is that cylinder sets (sets determined by a single relation query) are measurable.

Main Results

• StructureSpace.instMeasurableSpace: MeasurableSpace instance on StructureSpace L.
• measurableSet_relHolds: The set of codes where a given relation query holds is measurable.

instance FirstOrder.Language.instMeasurableSpaceStructureSpaceOn {L : Language} {α : Type u_1} : MeasurableSpace (L.StructureSpaceOn α)

Equations

• FirstOrder.Language.instMeasurableSpaceStructureSpaceOn = MeasurableSpace.pi

theorem FirstOrder.Language.measurableSet_relHoldsOn {L : Language} {α : Type u_1} (q : L.RelQueryOn α) : MeasurableSet {c : L.StructureSpaceOn α | c q = true}

The set of codes where a given relation query returns true is measurable (generic).

instance FirstOrder.Language.instMeasurableSpaceStructureSpace {L : Language} : MeasurableSpace L.StructureSpace

StructureSpace L inherits the product measurable space from RelQuery L → Bool. Since Bool has MeasurableSpace Bool := ⊤ (all sets measurable), this is the σ-algebra generated by cylinder sets.

Equations

• FirstOrder.Language.instMeasurableSpaceStructureSpace = MeasurableSpace.pi

theorem FirstOrder.Language.measurableSet_relHolds {L : Language} (q : L.RelQuery) : MeasurableSet {c : L.StructureSpace | c q = true}

The set of codes where a given relation query returns true is measurable. These are the basic cylinder sets generating the σ-algebra.