Morley counting, with a witness in the second alternative

morley_counting says the number of isomorphism classes of countable models is ≤ ℵ₁ or exactly 2^{ℵ₀}. Its second alternative is a bare cardinal equation: it asserts that continuum-many classes exist without exhibiting them, and it cannot do better, because its SilverBurgessDichotomy hypothesis carries only cardinal information.

Here the proved Silver route is used directly instead, through silver_core_polish, and the second alternative becomes a perfect set of pairwise non-isomorphic models. That is strictly more information: continuum-many classes follows from a perfect antichain (HasPerfectSetOfPairwiseNonisomorphicNatModels.continuum_le), so the cardinal form is recovered as morley_counting_or_perfect_cardinal below, while the converse fails — a cardinal equation gives no set.

Two tiers, one pipeline

Countable models come in tiers: carrier ℕ, and carrier Fin n for each n. The finite tier is not a formality. An infinite language can have continuum-many Fin n-models and no ℕ-models at all, so a statement offering only an ℕ-tier perfect set would be false; hence the third alternative.

Both tiers run through silver_countable_or_cantorAntichain, which handles the fact that the model class is a Borel subset of the structure space and so is not Polish as a subtype. They differ only in which relation Silver is applied to:

• at ℕ, Silver sees back-and-forth equivalence at a level α < ω₁ — the relation the Scott stratification makes Borel — and the antichain is transferred to isomorphism, which refines it;
• at Fin n, isomorphism is itself Borel (a finite union of permutation graphs), so Silver is applied to it directly.

morley_counting itself is left untouched: it remains the statement parameterized by the dichotomy, and nothing here is a replacement for it.

The two tiers

theorem FirstOrder.Language.morley_counting_coded_or_perfect {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (φ : L.Sentenceω) : Cardinal.mk (Quotient (isoSetoid φ)) ≤ Cardinal.aleph 1 ∨ φ.HasPerfectSetOfPairwiseNonisomorphicNatModels

Morley counting for ℕ-coded models, with a witness. Either at most ℵ₁ isomorphism classes, or a perfect set of pairwise non-isomorphic models.

The case split is on the conclusion itself rather than on a cardinal: if no perfect set exists, then no level of the stratification can produce a Cantor antichain, so every level has a countable quotient and the Scott-height bound applies.

theorem FirstOrder.Language.counting_fin_models_countable_or_perfect {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (φ : L.Sentenceω) (n : ℕ) : Cardinal.mk (Quotient (isoSetoidOn φ n)) ≤ Cardinal.aleph0 ∨ φ.HasPerfectSetOfPairwiseNonisomorphicFinModels n

Finite-carrier counting, with a witness. Either countably many isomorphism classes among the Fin n-models, or a perfect set of pairwise non-isomorphic ones.

Unlike the ℕ tier this needs no stratification: isomorphism of Fin n-structures is the orbit relation of a finite group, hence Borel outright, so Silver applies to it directly and the relation-refinement step is the identity.

The tiered theorem

theorem FirstOrder.Language.morley_counting_or_perfect {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (φ : L.Sentenceω) : Cardinal.mk (AllCodedIsoClasses φ) ≤ Cardinal.aleph 1 ∨ φ.HasPerfectSetOfPairwiseNonisomorphicNatModels ∨ ∃ (n : ℕ), φ.HasPerfectSetOfPairwiseNonisomorphicFinModels n

Morley's counting theorem, with a witness in the second alternative.

Either at most ℵ₁ isomorphism classes of countable models, or a perfect set of pairwise non-isomorphic models at one of the two tiers.

The ℕ-tier and Fin n-tier alternatives are kept separate because they are genuinely different statements about different spaces, and because neither implies the other: a sentence may have a perfect set of finite models and no infinite models whatsoever.

The cardinal form as a corollary

Recovering morley_counting's conclusion from the witnessed one, which is the sense in which the perfect alternatives carry more information rather than merely restating it. The upper bound ≤ 2^{ℵ₀} is not part of the witnessed statement and is supplied here: every tier's quotient is a quotient of a Bool-valued function space on a countable index.

theorem FirstOrder.Language.morley_counting_or_perfect_cardinal {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (φ : L.Sentenceω) : Cardinal.mk (AllCodedIsoClasses φ) ≤ Cardinal.aleph 1 ∨ Cardinal.mk (AllCodedIsoClasses φ) = Cardinal.continuum

The cardinal alternative, as a corollary of the witnessed one.

This is morley_counting's conclusion, obtained without assuming the Silver–Burgess dichotomy: either alternative's perfect set forces continuum-many classes, and the ambient space supplies the matching upper bound.