BFEquiv is Borel on the Pair Space

This file proves that the back-and-forth equivalence relation BFEquiv α is measurable (Borel) on the pair space StructureSpace L × StructureSpace L for α < ω₁.

Main Definitions

• StructurePairSpace L: The product StructureSpace L × StructureSpace L.
• BFEquivSet: The set of code pairs where BFEquiv α n a b holds.

Main Results

• bfEquivSet_measurableSet: BFEquivSet α n a b is measurable for α < ω₁.

Proof Strategy

Direct transfinite induction on α matching BFEquiv's definition:

• Zero: SameAtomicType a b = countable intersection over AtomicIdx.
• Successor β: IH ∧ (∀ m, ∃ n', IH on snoc) ∧ (∀ n', ∃ m, IH on snoc).
• Limit β: ⋂_{γ < β} IH — countable intersection (since β < ω₁).

@[reducible, inline]

abbrev FirstOrder.Language.StructurePairSpace (L : Language) : Type v

The pair space: two coded structures.

Equations

• L.StructurePairSpace = (L.StructureSpace × L.StructureSpace)

@[instance_reducible]

instance FirstOrder.Language.instMeasurableSpaceStructurePairSpace {L : Language} : MeasurableSpace L.StructurePairSpace

The product measurable space on the pair space.

Equations

• FirstOrder.Language.instMeasurableSpaceStructurePairSpace = inferInstance.prod inferInstance

def FirstOrder.Language.BFEquivSet {L : Language} [L.IsRelational] (α : Ordinal.{0}) (n : ℕ) (a b : Fin n → ℕ) : Set L.StructurePairSpace

The set of code pairs where BFEquiv α n a b holds.

Equations

• FirstOrder.Language.BFEquivSet α n a b = {p : L.StructurePairSpace | FirstOrder.Language.BFEquiv α n a b}

theorem FirstOrder.Language.bfEquivSet_measurableSet {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (α : Ordinal.{0}) (hα : α < Ordinal.omega 1) (n : ℕ) (a b : Fin n → ℕ) : MeasurableSet (BFEquivSet α n a b)

The main theorem: BFEquivSet α n a b is measurable for α < ω₁.