The sentence-spectrum characterization of thinness

For a Borel class C of coded structures over a countable relational language,

IsThinOn (structureIsoSetoid L) C ↔ ∀ θ : ℕ → L.Sentenceω, (sentenceTheory θ '' C).Countable

(thin_iff_countable_sentence_spectra): C carries no perfect set of pairwise non-isomorphic structures exactly when every countable list of L_{ω₁ω}-sentences has only countably many truth sequences realized on C. The class need not be isomorphism-invariant, and no Borelness of isomorphism is assumed.

• Thin ⟹ countable spectra: Silver (silver_countable_or_cantorAntichain) is applied to the kernel of the Borel truth-sequence map, a Borel equivalence relation coarser than isomorphism; its Cantor alternative is an isomorphism antichain, which thinness refutes.
• Countable spectra ⟹ thin: on a Borel Cantor antichain the sentences recover the parameter (sentences_recover_cantor), so the spectrum of that list is uncountable.

Sentence form: Sentenceω.isThinOnNatModels_iff_countable_sentence_spectra, with Borelness of the model class discharged.

Not claimed

Countable spectra say ∀ θ, countable image. They do not supply one list θ that classifies isomorphism on C: a Borel complete invariant together with thinness forces countably many classes (countable_iso_classes_of_thin_borel_classifiable). Nothing here establishes the spectrum bound for any particular sentence; applications must supply their own smallness argument. This module lives in Conditional/ beside MorleyPerfect.lean because it consumes the Silver adapter.

Classical background

Scatteredness and its equivalent criteria: Marker, Lectures on Infinitary Model Theory (Cambridge, 2016), Definition 3.3.1 and Corollary 3.3.10; his Corollary 3.3.3 works with the relation of realizing the same fragment types. Keisler, "Randomizations of scattered sentences" (in Iovino, ed., Beyond First Order Model Theory, CRC Press, 2017), §2, codes fragment truth in a similar way. The sentence-spectrum formulation on an arbitrary Borel class, without a Borel isomorphism relation, is assembled here from the project's Silver adapter and its sentence-recovery API.

theorem FirstOrder.Language.sentence_spectrum_countable_or_cantor {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (C : Set L.StructureSpace) (hC : MeasurableSet C) (θ : ℕ → L.Sentenceω) : (sentenceTheory θ '' C).Countable ∨ HasCantorAntichainOn L.structureIsoSetoid C

Silver on truth sequences. For a Borel class and a sentence list, either the realized truth sequences are countable or the class contains a continuous Cantor isomorphism antichain. Silver is applied to equality of truth sequences, coarser than isomorphism.

theorem FirstOrder.Language.thin_iff_countable_sentence_spectra {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (C : Set L.StructureSpace) (hC : MeasurableSet C) : IsThinOn L.structureIsoSetoid C ↔ ∀ (θ : ℕ → L.Sentenceω), (sentenceTheory θ '' C).Countable

Thinness is countability of every countable sentence spectrum, on any Borel class.

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

Sentence form: a sentence is thin on its ℕ-models exactly when every countable sentence list has countably many truth sequences realized in its models.

theorem FirstOrder.Language.countable_iso_classes_of_thin_borel_classifiable {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (C : Set L.StructureSpace) (hC : MeasurableSet C) (hthin : IsThinOn L.structureIsoSetoid C) (hp : ∃ (p : ↑C → ℕ → Bool), Measurable p ∧ ∀ (c d : ↑C), L.structureIsoSetoid ↑c ↑d ↔ p c = p d) : Countable (Quotient (Setoid.comap (fun (c : ↑C) => ↑c) L.structureIsoSetoid))

Guardrail: a Borel complete invariant cannot classify a thin class with uncountably many isomorphism classes. This does not conflict with countable sentence spectra, which quantify over each list separately rather than assert one complete list exists.