Isomorphism is Borel under Bounded Scott Height

This file proves that isomorphism restricted to models of a sentence is Borel (measurable) when the Scott height is bounded by a countable ordinal.

Main Results

• iso_borel_of_bounded_scottHeight: If all countable models of φ have Scott height ≤ α < ω₁, then the set of isomorphic pairs within ModelsOf(φ) × ModelsOf(φ) is measurable.

def FirstOrder.Language.IsoSet (L : Language) [L.IsRelational] : Set L.StructurePairSpace

The set of code pairs whose decoded structures are isomorphic.

Equations

• L.IsoSet = {p : L.StructurePairSpace | Nonempty (L.Equiv ℕ ℕ)}

theorem FirstOrder.Language.iso_borel_of_bounded_scottHeight {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} {α : Ordinal.{0}} (hα : α < Ordinal.omega 1) (hbound : ∀ (M : Type) [inst : L.Structure M] [inst_1 : Countable M], φ.Realize M → scottHeight M ≤ α) : MeasurableSet (L.IsoSet ∩ ModelsOf φ ×ˢ ModelsOf φ)

Isomorphism on coded structures is Borel when Scott height is bounded. If all countable models of φ have Scott height ≤ α < ω₁, then the set of isomorphic pairs within ModelsOf(φ) × ModelsOf(φ) is measurable.