Borel observables are sentence truths

Relative López–Escobar for Borel families of structures, allowing repetitions and non-isomorphic members with the same observable. Everything here is below Silver: the only input is sentence_pullback_of_iso_compatible.

• sentences_recover_observable: a measurable Cantor-valued invariant p of a Borel family f is exactly sentenceTheory θ (f x) for some countable sentence list θ.
• sentences_encode_observable: the target may be any countably separated measurable space, through a measurable injection into Cantor space.
• sentence_classification_iff_borel_classification: on a Borel class, a Borel complete invariant exists iff a complete countable list of sentences does.

No selector of representatives is built, and no Borel map into the syntax of sentences is claimed: the sentence list exists for the chosen observable, by classical choice. The thinness corollary (a Borel complete invariant on a thin class forces countably many classes) needs the spectrum characterization and lives in Conditional/SentenceSpectrum.lean.

Classical background

Countable separating families and Borel complete invariants: Gao, Invariant Descriptive Set Theory (CRC Press, 2009), Proposition 5.4.4. The observable-recovery statements here are derived from the project's sentence-recovery API and are not claimed to occur in that form in the source.

theorem FirstOrder.Language.sentences_recover_observable {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] {X : Type} [MeasurableSpace X] [StandardBorelSpace X] (f : X → L.StructureSpace) (hf : Measurable f) (p : X → ℕ → Bool) (hp : Measurable p) (hiso : ∀ (x y : X), L.structureIsoSetoid (f x) (f y) → p x = p y) : ∃ (θ : ℕ → L.Sentenceω), ∀ (x : X), sentenceTheory θ (f x) = p x

A Borel Cantor-valued invariant of a Borel family is a sequence of sentence truths on that family. The invariant need not be complete.

theorem FirstOrder.Language.sentences_encode_observable {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] {X Y : Type} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [MeasurableSpace.CountablySeparated Y] (f : X → L.StructureSpace) (hf : Measurable f) (p : X → Y) (hp : Measurable p) (hiso : ∀ (x y : X), L.structureIsoSetoid (f x) (f y) → p x = p y) : ∃ (e : Y → ℕ → Bool) (θ : ℕ → L.Sentenceω), Measurable e ∧ Function.Injective e ∧ ∀ (x : X), sentenceTheory θ (f x) = e (p x)

Countably separated targets: the chosen measurable injection encodes observables, not representatives of isomorphism classes.

theorem FirstOrder.Language.sentence_classification_iff_borel_classification {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (C : Set L.StructureSpace) (hC : MeasurableSet C) : (∃ (θ : ℕ → L.Sentenceω), ∀ (c d : ↑C), L.structureIsoSetoid ↑c ↑d ↔ sentenceTheory θ ↑c = sentenceTheory θ ↑d) ↔ ∃ (p : ↑C → ℕ → Bool), Measurable p ∧ ∀ (c d : ↑C), L.structureIsoSetoid ↑c ↑d ↔ p c = p d

Smooth classification is sentence classification on a Borel class: a Borel complete invariant with Cantor target exists iff a complete countable list of sentences does.