Recovering Borel data by sentences

Truth sequences

sentenceTheory θ c is the truth sequence of a countable list of sentences θ at the coded structure c. It is measurable (measurable_sentenceTheory) and isomorphism-invariant (sentenceTheory_eq_of_iso). These basics stay here, below any use of Silver: the spectrum characterization (Conditional/SentenceSpectrum.lean) consumes them, and observable recovery need not import it.

Relative López–Escobar

sentence_pullback_of_iso_compatible: a Borel predicate on a standard Borel family of structures that is constant on isomorphic outputs is the pullback of one sentence. The proof saturates the two images, separates them by sentence_separates_analytic_classes, and reads the sentence back along the family. The antichain form sentence_pullback_on_antichain, where isomorphism compatibility is automatic, is a corollary.

Cantor parameters

On a Borel Cantor isomorphism antichain, countably many sentences recover every parameter bit (sentences_recover_cantor, sentenceTheory_eq_parameter). Hence a class on which every countable sentence list has countably many realized truth sequences carries no such antichain (no_antichain_of_countable_sentence_spectra), and a sentence with that property is thin (thin_of_countable_sentence_spectra). The converse needs Silver and lives in Conditional/SentenceSpectrum.lean.

Classical background

López–Escobar is Marker, Lectures on Infinitary Model Theory (Cambridge, 2016), Theorem 4.3.7; Gao, Invariant Descriptive Set Theory (CRC Press, 2009), Theorem 11.3.6, is an alternative exposition. The relative form on a Borel family and the recovery of Cantor parameters are derived here from invariant separation; these formulations are not claimed to occur in the sources.

Truth sequences

noncomputable def FirstOrder.Language.sentenceTheory {L : Language} [L.IsRelational] (θ : ℕ → L.Sentenceω) (c : L.StructureSpace) : ℕ → Bool

The truth sequence of a countable list of sentences at a coded structure.

Equations

• FirstOrder.Language.sentenceTheory θ c n = decide (c ∈ FirstOrder.Language.ModelsOf (θ n))

theorem FirstOrder.Language.measurable_sentenceTheory {L : Language} [L.IsRelational] (θ : ℕ → L.Sentenceω) : Measurable (sentenceTheory θ)

theorem FirstOrder.Language.sentenceTheory_eq_of_iso {L : Language} [L.IsRelational] (θ : ℕ → L.Sentenceω) {c d : L.StructureSpace} (h : L.structureIsoSetoid c d) : sentenceTheory θ c = sentenceTheory θ d

Relative López–Escobar

theorem FirstOrder.Language.sentence_pullback_of_iso_compatible {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] {X : Type} [MeasurableSpace X] [StandardBorelSpace X] (f : X → L.StructureSpace) (hf : Measurable f) (U : Set X) (hU : MeasurableSet U) (hiso : ∀ (x y : X), L.structureIsoSetoid (f x) (f y) → (x ∈ U ↔ y ∈ U)) : ∃ (θ : L.Sentenceω), ∀ (x : X), f x ∈ ModelsOf θ ↔ x ∈ U

Relative López–Escobar. A Borel predicate on a standard Borel family of structures that respects isomorphism of the outputs is the pullback of one sentence. No antichain is required, and the family may have repetitions.

theorem FirstOrder.Language.sentence_pullback_on_antichain {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] {X : Type} [MeasurableSpace X] [StandardBorelSpace X] (f : X → L.StructureSpace) (hf : Measurable f) (hanti : ∀ (x y : X), x ≠ y → ¬L.structureIsoSetoid (f x) (f y)) (U : Set X) (hU : MeasurableSet U) : ∃ (θ : L.Sentenceω), ∀ (x : X), f x ∈ ModelsOf θ ↔ x ∈ U

On an isomorphism antichain every Borel predicate is the pullback of one sentence: compatibility with isomorphism is automatic.

Cantor parameters

theorem FirstOrder.Language.sentences_recover_cantor {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (f : (ℕ → Bool) → L.StructureSpace) (hf : Measurable f) (hanti : ∀ (x y : ℕ → Bool), x ≠ y → ¬L.structureIsoSetoid (f x) (f y)) : ∃ (θ : ℕ → L.Sentenceω), ∀ (x : ℕ → Bool) (n : ℕ), f x ∈ ModelsOf (θ n) ↔ x n = true

Sentences recover the Cantor parameter on a Borel isomorphism antichain: each bit is the truth of one sentence.

theorem FirstOrder.Language.sentenceTheory_eq_parameter {L : Language} [L.IsRelational] (f : (ℕ → Bool) → L.StructureSpace) (θ : ℕ → L.Sentenceω) (hθ : ∀ (x : ℕ → Bool) (n : ℕ), f x ∈ ModelsOf (θ n) ↔ x n = true) (x : ℕ → Bool) : sentenceTheory θ (f x) = x

theorem FirstOrder.Language.no_antichain_of_countable_sentence_spectra {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (C : Set L.StructureSpace) (hsmall : ∀ (θ : ℕ → L.Sentenceω), (sentenceTheory θ '' C).Countable) (f : (ℕ → Bool) → L.StructureSpace) (hf : Measurable f) (hC : ∀ (x : ℕ → Bool), f x ∈ C) : ¬∀ (x y : ℕ → Bool), x ≠ y → ¬L.structureIsoSetoid (f x) (f y)

A class on which every countable sentence list has countably many realized truth sequences carries no Borel Cantor isomorphism antichain.

theorem FirstOrder.Language.thin_of_countable_sentence_spectra {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (φ : L.Sentenceω) (hsmall : ∀ (θ : ℕ → L.Sentenceω), (sentenceTheory θ '' ModelsOf φ).Countable) : φ.IsThinOnNatModels

Countable sentence spectra give thinness: the sufficient direction, without Silver.