Counting

Results named in Tau Ceti's TauCeti.ModelTheory.Counting modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremMorley's cardinal dichotomy on the tier ℕ#

In a relational language with countably many relation symbols of each arity, the models of φ on ℕ have either at most ℵ₁ or 𝔠 isomorphism classes.

TauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_eq_continuum.{u, v, uι}
  {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)]
  [Countable ι] (φ : L.SentenceInf ι) :
  Cardinal.mk (Quotient (TauCeti.RelationalConfiguration.isoSetoidOn ℕ φ)) ≤ Cardinal.aleph 1 ∨
    Cardinal.mk (Quotient (TauCeti.RelationalConfiguration.isoSetoidOn ℕ φ)) = Cardinal.continuum

Lean

Formalized in Tau Ceti as TauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_eq_continuum.

Other forms

Morley's cardinal dichotomy for Borel sets on ℕ. Formalized in Tau Ceti as TauCeti.mk_isoClasses_le_aleph_one_or_eq_continuum.

TauCeti.mk_isoClasses_le_aleph_one_or_eq_continuum.{u, v} {L : FirstOrder.Language} [L.IsRelational]
  [∀ (n : ℕ), Countable (L.Relations n)] {K : Set (TauCeti.RelationalConfiguration L ℕ)}
  (hK : MeasurableSet K) :
  Cardinal.mk
        (Quotient (Setoid.comap Subtype.val (TauCeti.RelationalConfiguration.isoSetoid L ℕ))) ≤
      Cardinal.aleph 1 ∨
    Cardinal.mk
        (Quotient (Setoid.comap Subtype.val (TauCeti.RelationalConfiguration.isoSetoid L ℕ))) =
      Cardinal.continuum

Sources

• Tau Ceti documentation: TauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_eq_continuum
• Source of TauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_eq_continuum in TauCeti/ModelTheory/Counting/Morley.lean

LeanTauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_eq_continuum · TauCeti.mk_isoClasses_le_aleph_one_or_eq_continuum

Uses 2

Statement usesFirstOrder.Language.BoundedFormulaInf

Proof usesMorley's dichotomy on the tier ℕ

TheoremMorley's dichotomy on the tier ℕ#

In a relational language with countably many relation symbols of each arity, the models on ℕ of an infinitary sentence with countable branching have at most ℵ₁ isomorphism classes, or contain a nonempty perfect set of pairwise non-isomorphic models.

TauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_hasPerfectAntichainOn.{u, v, uι}
  {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)]
  [Countable ι] (φ : L.SentenceInf ι) :
  Cardinal.mk (Quotient (TauCeti.RelationalConfiguration.isoSetoidOn ℕ φ)) ≤ Cardinal.aleph 1 ∨
    (TauCeti.RelationalConfiguration.isoSetoid L ℕ).HasPerfectAntichainOn
      (TauCeti.RelationalConfiguration.modelsOf φ)

Lean

Formalized in Tau Ceti as TauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_hasPerfectAntichainOn.

Other forms

Morley's dichotomy for Borel sets on ℕ. Formalized in Tau Ceti as TauCeti.mk_isoClasses_le_aleph_one_or_hasPerfectAntichainOn.

TauCeti.mk_isoClasses_le_aleph_one_or_hasPerfectAntichainOn.{u, v} {L : FirstOrder.Language}
  [L.IsRelational] [∀ (n : ℕ), Countable (L.Relations n)]
  {K : Set (TauCeti.RelationalConfiguration L ℕ)} (hK : MeasurableSet K) :
  Cardinal.mk
        (Quotient (Setoid.comap Subtype.val (TauCeti.RelationalConfiguration.isoSetoid L ℕ))) ≤
      Cardinal.aleph 1 ∨
    (TauCeti.RelationalConfiguration.isoSetoid L ℕ).HasPerfectAntichainOn K

Sources

• Tau Ceti documentation: TauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_hasPerfectAntichainOn
• Source of TauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_hasPerfectAntichainOn in TauCeti/ModelTheory/Counting/Morley.lean

LeanTauCeti.mk_quotient_isoSetoidOn_nat_le_aleph_one_or_hasPerfectAntichainOn · TauCeti.mk_isoClasses_le_aleph_one_or_hasPerfectAntichainOn

Uses 5 · Used by 2

Statement usesFirstOrder.Language.BoundedFormulaInf

Proof usesSilver's theorem relative to a Borel subset · TauCeti.BFEquiv · TauCeti.exists_complete_self_stabilization · TauCeti.PotentialIso

Used byMorley's cardinal dichotomy on the tier ℕ · Morley's theorem (cardinal form)

TheoremMorley's theorem (cardinal form)#

In a relational language with countably many relation symbols of each arity, an infinitary sentence with countable branching has either at most ℵ₁ or 𝔠 countable models up to isomorphism. Neither the continuum hypothesis nor its negation is assumed.

TauCeti.morley_countableModelCount.{u, v, uι} {L : FirstOrder.Language} [L.IsRelational]
  {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] (φ : L.SentenceInf ι) :
  TauCeti.countableModelCount φ ≤ Cardinal.aleph 1 ∨
    TauCeti.countableModelCount φ = Cardinal.continuum

Lean

Formalized in Tau Ceti as TauCeti.morley_countableModelCount.

Other forms

Morley's theorem (witnessed form). Formalized in Tau Ceti as TauCeti.morley_countableModelCount_le_aleph_one_or_hasPerfectlyMany.

TauCeti.morley_countableModelCount_le_aleph_one_or_hasPerfectlyMany.{u, v, uι}
  {L : FirstOrder.Language} [L.IsRelational] {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)]
  [Countable ι] (φ : L.SentenceInf ι) :
  TauCeti.countableModelCount φ ≤ Cardinal.aleph 1 ∨ TauCeti.HasPerfectlyManyCountableModels φ

Sources

• Tau Ceti documentation: TauCeti.morley_countableModelCount
• Source of TauCeti.morley_countableModelCount in TauCeti/ModelTheory/Counting/Morley.lean

LeanTauCeti.morley_countableModelCount · TauCeti.morley_countableModelCount_le_aleph_one_or_hasPerfectlyMany

Uses 3

Statement usesFirstOrder.Language.BoundedFormulaInf

Proof usesMorley's dichotomy on the tier ℕ · Silver's theorem relative to a Borel subset

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.