Thinness is countability of every fragment spectrum

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

IsThinOn (structureIsoSetoid L) C ↔ ∀ F : Fragment L, F.toSet.Countable → ∀ n, (F.typeSpectrum n C).Countable

(thin_iff_countable_fragment_spectra): C carries no perfect set of pairwise non-isomorphic structures exactly when every countable fragment realizes only countably many n-types on C, at every finite arity. The class need not be isomorphism-invariant.

• Thin ⟹ countable spectra (fragmentSpectrum_countable_or_cantor): Silver's dichotomy (silver_countable_or_cantorAntichain) is applied to spectrum equivalence, the Borel relation "same realized F-types at arity n" (measurableSet_sameRealizedSpectrum), which isomorphism refines (sameRealizedSpectrum_of_iso). Countably many classes give countably many realized spectra, each countable, hence countably many realized types; the Cantor alternative is an isomorphism antichain, which thinness excludes. This is Marker's argument (Corollary 3.3.3); no Baire-property theorem for analytic sets enters.
• Countable spectra ⟹ thin: arity zero. For a sentence list θ, the fragment generated by its range is countable, and its arity-zero spectrum determines the truth sequences of θ; so countable fragment spectra give countable sentence spectra, and the sentence-spectrum characterization (thin_iff_countable_sentence_spectra) finishes.

Not claimed

The realized spectrum is not a complete isomorphism invariant, and nothing here proves any particular class thin: the theorem connects the existing criteria.

Classical background: Marker, Lectures on Infinitary Model Theory (Cambridge, 2016), Definition 3.3.1, Corollary 3.3.3, and Corollary 3.3.10.

theorem FirstOrder.Language.Fragment.fragmentSpectrum_countable_or_cantor {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (F : L.Fragment) (hF : F.toSet.Countable) (n : ℕ) (C : Set L.StructureSpace) (hC : MeasurableSet C) : (F.typeSpectrum n C).Countable ∨ HasCantorAntichainOn L.structureIsoSetoid C

Silver on spectrum equivalence. For a Borel class and a countable fragment at a fixed arity, either the realized spectrum on the class is countable or the class contains a continuous Cantor isomorphism antichain.

theorem FirstOrder.Language.Fragment.thin_iff_countable_fragment_spectra {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (C : Set L.StructureSpace) (hC : MeasurableSet C) : IsThinOn L.structureIsoSetoid C ↔ ∀ (F : L.Fragment), F.toSet.Countable → ∀ (n : ℕ), (F.typeSpectrum n C).Countable

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

theorem FirstOrder.Language.Sentenceω.isThinOnNatModels_iff_countable_fragment_spectra {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (φ : L.Sentenceω) : φ.IsThinOnNatModels ↔ ∀ (F : L.Fragment), F.toSet.Countable → ∀ (n : ℕ), (F.typeSpectrum n (ModelsOf φ)).Countable

Sentence form: a sentence is thin on its ℕ-models exactly when every countable fragment realizes only countably many types, at every arity, in its models.