Classes of countable models

Let L be a relational language and φ an infinitary sentence. A countable structure is isomorphic to one on ℕ or on some Fin n, so the isomorphism classes of the countable models of φ are the classes of its model classes on these carriers, under isomorphism of the decoded structures:

• TauCeti.RelationalConfiguration.isoSetoidOn V φ: isomorphism restricted to the configurations on V decoding to models of φ;
• TauCeti.CountableModelClasses φ: the disjoint union of the quotient on ℕ (the countably infinite models) and the quotients on each Fin n (the models with n elements);
• TauCeti.countableModelCount φ: its cardinality, the number of countable models of φ up to isomorphism.

Countable here means at most countable: the finite models, including the empty structure, are counted. Leaving them out would be wrong, not just incomplete: with countably many unary predicates, the sentence saying that there is exactly one element has no model on ℕ and continuum many pairwise non-isomorphic models on Fin 1.

Models in arbitrary universes enter through TauCeti.classOf, which sends a countable model to the class of its transport to Fin n if it has n elements and to ℕ otherwise. Two countable models, in any two universes, have the same class exactly when they are isomorphic (TauCeti.classOf_eq_classOf_iff), and every class is the class of a countable model in every universe (TauCeti.classOf_surjective). So CountableModelClasses φ is the set of isomorphism classes of countable models of φ, presented as a type in the universe of the relation symbols, and no statement has to count a proper class of structures.

In a language with countably many relation symbols of each arity there are at most continuum many countable models. A perfect set of pairwise non-isomorphic models, at the tier ℕ or at some finite tier, gives exactly continuum many (TauCeti.HasPerfectlyManyCountableModels.countableModelCount_eq). On a finite carrier no back-and-forth stratification is needed: isomorphism already has closed, hence Borel, graph, so Silver's theorem relative to the Borel model class gives countably many models up to isomorphism or a perfect set of pairwise non-isomorphic ones.

Main results

• TauCeti.countableModelCount_eq_add_sum: the count is the count on ℕ plus the sum of the counts on the finite carriers.
• TauCeti.countableModelCount_le_add_aleph0_mul and TauCeti.countableModelCount_le_aleph0_iff: bounds tier by tier; there are countably many countable models exactly when every tier has countably many classes.
• TauCeti.countableModelCount_le_of_subset: a sentence whose countable models are models of another has at most as many countable models.
• TauCeti.classOf_eq_classOf_iff and TauCeti.classOf_surjective: classOf is a bijection between isomorphism classes of countable models, in any universe, and CountableModelClasses φ.
• TauCeti.exists_classOf_eq_inl_iff and TauCeti.exists_classOf_eq_inr_iff: the infinite models land on the tier ℕ, the models with n elements on the tier Fin n.
• TauCeti.countableModelCount_le_continuum: at most continuum many countable models.
• TauCeti.HasPerfectlyManyCountableModels.countableModelCount_eq: a perfect set of pairwise non-isomorphic models gives continuum many.
• TauCeti.RelationalConfiguration.countable_quotient_isoSetoidOn_or_hasPerfectAntichainOn and TauCeti.RelationalConfiguration.mk_quotient_isoSetoidOn_le_aleph0_or_eq_continuum: on a finite carrier, the models of φ are countably many up to isomorphism or contain a nonempty perfect set of pairwise non-isomorphic ones (hence ≤ ℵ₀ or = 𝔠).
• TauCeti.forall_countable_quotient_isoSetoidOn_fin_or_exists_hasPerfectAntichainOn, TauCeti.sum_mk_quotient_isoSetoidOn_fin_le_aleph0_or_exists_hasPerfectAntichainOn, TauCeti.sum_mk_quotient_isoSetoidOn_fin_le_aleph0_or_hasPerfectlyManyCountableModels, and TauCeti.sum_mk_quotient_isoSetoidOn_fin_le_aleph0_or_eq_continuum: the dichotomy summed across all finite tiers Fin n.

References

• M. Morley, The number of countable models, J. Symbolic Logic 35 (1970), 14–18.
• J. H. Silver, Counting the number of equivalence classes of Borel and coanalytic equivalence relations, Annals of Mathematical Logic 18 (1980), 1–28.
• D. Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, the chapter on the space of countable models.

The tiered presentation of the classes and the finite-carrier dichotomy follow AllCodedIsoClasses, isoSetoidOn, and counting_fin_models_dichotomy in Cameron Freer's cameronfreer/infinitary-logic (InfinitaryLogic/Descriptive/FiniteCarrier.lean, checkpoint 518a366, Apache-2.0); there the bridges are for models in Type and the finite-carrier dichotomy is cardinal-only, whereas here the bridges work in every universe and both witnessed and cardinal forms are proved.

@[reducible, inline]

abbrev TauCeti.RelationalConfiguration.isoSetoidOn {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} (V : Type w) (φ : L.SentenceInf ι) : Setoid ↑(modelsOf φ)

Isomorphism of decoded structures, restricted to the configurations on V that decode to models of φ. Its classes are the isomorphism classes of the models of φ with carrier V. It is an abbreviation, so results stated for the restriction of isoSetoid L V to an arbitrary set of configurations apply to it.

@[simp]

theorem TauCeti.RelationalConfiguration.isoSetoidOn_apply {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {V : Type w} {φ : L.SentenceInf ι} {c d : ↑(modelsOf φ)} : (isoSetoidOn V φ) c d ↔ (isoSetoid L V) ↑c ↑d

Two models of φ are related exactly when their decoded structures are isomorphic.

theorem TauCeti.RelationalConfiguration.mk_quotient_isoSetoidOn_le_of_subset {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {ι' : Type uι'} {V : Type w} {φ : L.SentenceInf ι} {ψ : L.SentenceInf ι'} (h : modelsOf φ ⊆ modelsOf ψ) : Cardinal.mk (Quotient (isoSetoidOn V φ)) ≤ Cardinal.mk (Quotient (isoSetoidOn V ψ))

If every model of φ on V is a model of ψ, the models of φ on V have at most as many isomorphism classes as those of ψ: the inclusion of model classes is injective on classes.

theorem TauCeti.RelationalConfiguration.mk_quotient_isoSetoidOn_le_continuum {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] (V : Type w) [Countable V] (φ : L.SentenceInf ι) : Cardinal.mk (Quotient (isoSetoidOn V φ)) ≤ Cardinal.continuum

On a countable carrier, in a language with countably many relation symbols of each arity, the models of a sentence have at most continuum many isomorphism classes.

theorem TauCeti.RelationalConfiguration.isClosed_setOf_isoSetoidOn {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {V : Type w} [Finite V] (φ : L.SentenceInf ι) : IsClosed {p : ↑(modelsOf φ) × ↑(modelsOf φ) | (isoSetoidOn V φ) p.1 p.2}

On a finite carrier, restricted isomorphism on the model class of φ has closed graph in the square of the model class.

theorem TauCeti.RelationalConfiguration.measurableSet_setOf_isoSetoidOn {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] {V : Type w} [Finite V] (φ : L.SentenceInf ι) : MeasurableSet {p : ↑(modelsOf φ) × ↑(modelsOf φ) | (isoSetoidOn V φ) p.1 p.2}

On a finite carrier, in a language with countably many relation symbols of each arity, restricted isomorphism on the model class of φ has Borel graph.

theorem TauCeti.RelationalConfiguration.countable_quotient_isoSetoidOn_or_hasCantorAntichainOn {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] (V : Type w) [Finite V] (φ : L.SentenceInf ι) : Countable (Quotient (isoSetoidOn V φ)) ∨ (isoSetoid L V).HasCantorAntichainOn (modelsOf φ)

Finite-carrier dichotomy (Cantor form). On a finite carrier, in a language with countably many relation symbols of each arity, the models of an infinitary sentence with countable branching have countably many isomorphism classes or carry a Cantor antichain of pairwise non-isomorphic models.

theorem TauCeti.RelationalConfiguration.countable_quotient_isoSetoidOn_or_hasPerfectAntichainOn {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] (V : Type w) [Finite V] (φ : L.SentenceInf ι) : Countable (Quotient (isoSetoidOn V φ)) ∨ (isoSetoid L V).HasPerfectAntichainOn (modelsOf φ)

Finite-carrier dichotomy (perfect-set form). On a finite carrier, in a language with countably many relation symbols of each arity, the models of an infinitary sentence with countable branching have countably many isomorphism classes or contain a nonempty perfect set of pairwise non-isomorphic models.

theorem TauCeti.RelationalConfiguration.mk_quotient_isoSetoidOn_le_aleph0_or_eq_continuum {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] (V : Type w) [Finite V] (φ : L.SentenceInf ι) : Cardinal.mk (Quotient (isoSetoidOn V φ)) ≤ Cardinal.aleph0 ∨ Cardinal.mk (Quotient (isoSetoidOn V φ)) = Cardinal.continuum

Finite-carrier dichotomy (cardinal form). On a finite carrier, in a language with countably many relation symbols of each arity, the models of an infinitary sentence with countable branching have either at most ℵ₀ or exactly 𝔠 isomorphism classes.

@[reducible, inline]

abbrev TauCeti.CountableModelClasses {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} (φ : L.SentenceInf ι) : Type v

The isomorphism classes of the countable models of φ, tier by tier: the classes of the models with carrier ℕ, and, for each n, the classes of the models with carrier Fin n. Every countable model of φ, in any universe, has exactly one class here (classOf_eq_classOf_iff, classOf_surjective).

noncomputable def TauCeti.countableModelCount {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} (φ : L.SentenceInf ι) : Cardinal.{v}

The number of countable models of φ up to isomorphism, finite models included.

theorem TauCeti.countableModelCount_def {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} (φ : L.SentenceInf ι) : countableModelCount φ = Cardinal.mk (CountableModelClasses φ)

The number of countable models is the cardinality of CountableModelClasses φ.

theorem TauCeti.countableModelCount_eq_add_sum {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} (φ : L.SentenceInf ι) : countableModelCount φ = Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn ℕ φ)) + Cardinal.sum fun (n : ℕ) => Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ))

The number of countable models is the number of models on ℕ up to isomorphism plus, summed over n, the number of models on Fin n up to isomorphism.

theorem TauCeti.mk_quotient_isoSetoidOn_nat_le_countableModelCount {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} (φ : L.SentenceInf ι) : Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn ℕ φ)) ≤ countableModelCount φ

The models on ℕ contribute at most the number of countable models.

theorem TauCeti.mk_quotient_isoSetoidOn_fin_le_countableModelCount {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} (φ : L.SentenceInf ι) (n : ℕ) : Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ)) ≤ countableModelCount φ

The models on Fin n contribute at most the number of countable models.

theorem TauCeti.countableModelCount_le_add_aleph0_mul {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} {a b : Cardinal.{v}} (ha : Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn ℕ φ)) ≤ a) (hb : ∀ (n : ℕ), Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ)) ≤ b) : countableModelCount φ ≤ a + Cardinal.aleph0 * b

If the models on ℕ have at most a isomorphism classes and those on each Fin n at most b, there are at most a + ℵ₀ * b countable models.

theorem TauCeti.countableModelCount_le_aleph0_iff {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} : countableModelCount φ ≤ Cardinal.aleph0 ↔ Countable (Quotient (RelationalConfiguration.isoSetoidOn ℕ φ)) ∧ ∀ (n : ℕ), Countable (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ))

There are countably many countable models of φ exactly when the models on ℕ, and those on each Fin n, have countably many isomorphism classes.

theorem TauCeti.countableModelCount_le_of_subset {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {ι' : Type uι'} {φ : L.SentenceInf ι} {ψ : L.SentenceInf ι'} (hℕ : RelationalConfiguration.modelsOf φ ⊆ RelationalConfiguration.modelsOf ψ) (hfin : ∀ (n : ℕ), RelationalConfiguration.modelsOf φ ⊆ RelationalConfiguration.modelsOf ψ) : countableModelCount φ ≤ countableModelCount ψ

If every countable model of φ, on ℕ and on each Fin n, is a model of ψ, then φ has at most as many countable models as ψ.

theorem TauCeti.countableModelCount_le_continuum {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] (φ : L.SentenceInf ι) : countableModelCount φ ≤ Cardinal.continuum

In a language with countably many relation symbols of each arity, there are at most continuum many countable models.

Countable models in arbitrary universes

noncomputable def TauCeti.classOf {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} (φ : L.SentenceInf ι) {M : Type w} [L.Structure M] [Countable M] (hM : φ.Realize M) : CountableModelClasses φ

The class of a countable model of φ, in any universe: the class of its transport to Fin n along a bijection if it has n elements, and to ℕ otherwise. It does not depend on the bijection (classOf_eq_inl, classOf_eq_inr).

theorem TauCeti.classOf_eq_inl {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} {M : Type w} [L.Structure M] [Countable M] (hM : φ.Realize M) (e : M ≃ ℕ) : classOf φ hM = Sum.inl ⟦⟨e.encodeVia, ⋯⟩⟧

The class of an infinite countable model is that of its transport to ℕ along any bijection.

theorem TauCeti.classOf_eq_inr {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} {M : Type w} [L.Structure M] [Countable M] {n : ℕ} (hM : φ.Realize M) (e : M ≃ Fin n) : classOf φ hM = Sum.inr ⟨n, ⟦⟨e.encodeVia, ⋯⟩⟧⟩

The class of a model with n elements is that of its transport to Fin n along any bijection.

@[simp]

theorem TauCeti.classOf_toStructure_nat {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} (c : ↑(RelationalConfiguration.modelsOf φ)) : classOf φ ⋯ = Sum.inl ⟦c⟧

The class of the structure decoded from a model of φ on ℕ is the class of that model.

@[simp]

theorem TauCeti.classOf_toStructure_fin {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} {n : ℕ} (c : ↑(RelationalConfiguration.modelsOf φ)) : classOf φ ⋯ = Sum.inr ⟨n, ⟦c⟧⟩

The class of the structure decoded from a model of φ on Fin n is the class of that model.

theorem TauCeti.classOf_congr {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [Countable M] [Countable N] (g : L.Equiv M N) (hM : φ.Realize M) (hN : φ.Realize N) : classOf φ hM = classOf φ hN

Isomorphic countable models, in any two universes, have the same class.

theorem TauCeti.exists_classOf_eq_inl_iff {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} {M : Type w} [L.Structure M] [Countable M] (hM : φ.Realize M) : (∃ (q : Quotient (RelationalConfiguration.isoSetoidOn ℕ φ)), classOf φ hM = Sum.inl q) ↔ Infinite M

The class of a countable model lies on the tier ℕ exactly when the model is infinite.

theorem TauCeti.exists_classOf_eq_inr_iff {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} {M : Type w} [L.Structure M] [Countable M] (hM : φ.Realize M) (n : ℕ) : (∃ (q : Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ)), classOf φ hM = Sum.inr ⟨n, q⟩) ↔ Nonempty (M ≃ Fin n)

The class of a countable model lies on the tier Fin n exactly when the model has n elements.

theorem TauCeti.classOf_eq_classOf_iff {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [Countable M] [Countable N] (hM : φ.Realize M) (hN : φ.Realize N) : classOf φ hM = classOf φ hN ↔ Nonempty (L.Equiv M N)

Two countable models of φ, in any two universes, have the same class exactly when they are isomorphic.

theorem TauCeti.classOf_surjective {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} (q : CountableModelClasses φ) : ∃ (M : Type w) (x : L.Structure M) (x_1 : Countable M) (hM : φ.Realize M), classOf φ hM = q

Every class of countable models of φ is the class of a countable model in every universe.

Perfect sets of non-isomorphic models

def TauCeti.HasPerfectlyManyCountableModels {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} (φ : L.SentenceInf ι) : Prop

φ has perfectly many countable models: on ℕ or on some Fin n, its model class contains a nonempty perfect set of configurations whose decoded structures are pairwise non-isomorphic. The finite tiers are needed: with countably many unary predicates, the sentence saying that there is exactly one element has such a set on Fin 1 and no model on ℕ.

theorem TauCeti.hasPerfectlyManyCountableModels_iff {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} : HasPerfectlyManyCountableModels φ ↔ (RelationalConfiguration.isoSetoid L ℕ).HasPerfectAntichainOn (RelationalConfiguration.modelsOf φ) ∨ ∃ (n : ℕ), (RelationalConfiguration.isoSetoid L (Fin n)).HasPerfectAntichainOn (RelationalConfiguration.modelsOf φ)

φ has perfectly many countable models exactly when its model class on ℕ, or on some Fin n, contains a nonempty perfect set of pairwise non-isomorphic configurations.

theorem TauCeti.HasPerfectlyManyCountableModels.of_nat {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} (h : (RelationalConfiguration.isoSetoid L ℕ).HasPerfectAntichainOn (RelationalConfiguration.modelsOf φ)) : HasPerfectlyManyCountableModels φ

A perfect set of pairwise non-isomorphic models on ℕ gives perfectly many countable models.

theorem TauCeti.HasPerfectlyManyCountableModels.of_fin {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} {n : ℕ} (h : (RelationalConfiguration.isoSetoid L (Fin n)).HasPerfectAntichainOn (RelationalConfiguration.modelsOf φ)) : HasPerfectlyManyCountableModels φ

A perfect set of pairwise non-isomorphic models on some Fin n gives perfectly many countable models.

theorem TauCeti.HasPerfectlyManyCountableModels.countableModelCount_eq {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] {φ : L.SentenceInf ι} (h : HasPerfectlyManyCountableModels φ) : countableModelCount φ = Cardinal.continuum

In a language with countably many relation symbols of each arity, a sentence with perfectly many countable models has exactly continuum many.

The finite-tier dichotomy

theorem TauCeti.forall_countable_quotient_isoSetoidOn_fin_or_exists_hasPerfectAntichainOn {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (k : ℕ), Countable (L.Relations k)] [Countable ι] (φ : L.SentenceInf ι) : (∀ (n : ℕ), Countable (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ))) ∨ ∃ (n : ℕ), (RelationalConfiguration.isoSetoid L (Fin n)).HasPerfectAntichainOn (RelationalConfiguration.modelsOf φ)

Across all finite carriers Fin n, either every finite tier has countably many models up to isomorphism, or some finite tier contains a nonempty perfect set of pairwise non-isomorphic models.

theorem TauCeti.countable_quotient_isoSetoidOn_fin_of_not_hasPerfectlyManyCountableModels {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (k : ℕ), Countable (L.Relations k)] [Countable ι] {φ : L.SentenceInf ι} (h : ¬HasPerfectlyManyCountableModels φ) (n : ℕ) : Countable (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ))

A sentence without perfectly many countable models has countably many models up to isomorphism on every finite carrier Fin n.

theorem TauCeti.sum_mk_quotient_isoSetoidOn_fin_le_aleph0_or_exists_hasPerfectAntichainOn {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (k : ℕ), Countable (L.Relations k)] [Countable ι] (φ : L.SentenceInf ι) : (Cardinal.sum fun (n : ℕ) => Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ))) ≤ Cardinal.aleph0 ∨ ∃ (n : ℕ), (RelationalConfiguration.isoSetoid L (Fin n)).HasPerfectAntichainOn (RelationalConfiguration.modelsOf φ)

Across all finite carriers Fin n, the finite tiers together contribute at most countably many isomorphism classes of models, or some finite tier contains a nonempty perfect set of pairwise non-isomorphic models.

theorem TauCeti.sum_mk_quotient_isoSetoidOn_fin_le_aleph0_or_hasPerfectlyManyCountableModels {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (k : ℕ), Countable (L.Relations k)] [Countable ι] (φ : L.SentenceInf ι) : (Cardinal.sum fun (n : ℕ) => Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ))) ≤ Cardinal.aleph0 ∨ HasPerfectlyManyCountableModels φ

The finite tiers together contribute at most countably many isomorphism classes of models, or φ has perfectly many countable models.

theorem TauCeti.sum_mk_quotient_isoSetoidOn_fin_le_aleph0_or_eq_continuum_of_dichotomy {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} {φ : L.SentenceInf ι} (hfin : ∀ (n : ℕ), Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ)) ≤ Cardinal.aleph0 ∨ Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ)) = Cardinal.continuum) : (Cardinal.sum fun (n : ℕ) => Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ))) ≤ Cardinal.aleph0 ∨ (Cardinal.sum fun (n : ℕ) => Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ))) = Cardinal.continuum

If each finite carrier Fin n has either at most ℵ₀ or 𝔠 models of φ up to isomorphism, then the finite tiers together contribute either at most ℵ₀ or 𝔠 isomorphism classes of models. No countability assumption on the language or on the branching index ι is required.

theorem TauCeti.sum_mk_quotient_isoSetoidOn_fin_le_aleph0_or_eq_continuum {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (k : ℕ), Countable (L.Relations k)] [Countable ι] (φ : L.SentenceInf ι) : (Cardinal.sum fun (n : ℕ) => Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ))) ≤ Cardinal.aleph0 ∨ (Cardinal.sum fun (n : ℕ) => Cardinal.mk (Quotient (RelationalConfiguration.isoSetoidOn (Fin n) φ))) = Cardinal.continuum

Across all finite carriers Fin n, in a language with countably many relation symbols of each arity, an infinitary sentence with countable branching has either at most ℵ₀ or 𝔠 finite models up to isomorphism.