Countability Predicates for L∞ω Formulas

This file defines predicates characterizing when an L∞ω formula belongs to specific cardinality-bounded fragments.

Main Definitions

• BoundedFormulaInf.IsCountable: A formula is countable if all index types in iSup/iInf constructors are countable. This characterizes membership in Lω₁ω.
• BoundedFormulaInf.IsKappa: A formula has cardinality < κ if all index types have cardinality < κ. This characterizes membership in Lκω.

inductive FirstOrder.Language.BoundedFormulaInf.IsCountable {L : Language} {α : Type u'} {n : ℕ} : L.BoundedFormulaInf α n → Prop

A formula is countable if all index types in iSup/iInf constructors are countable. This characterizes membership in Lω₁ω.

• falsum {L : Language} {α : Type u'} {n : ℕ} : BoundedFormulaInf.falsum.IsCountable
• equal {L : Language} {α : Type u'} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) : (BoundedFormulaInf.equal t₁ t₂).IsCountable
• rel {L : Language} {α : Type u'} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) : (BoundedFormulaInf.rel R ts).IsCountable
• imp {L : Language} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormulaInf α n} : φ.IsCountable → ψ.IsCountable → (φ.imp ψ).IsCountable
• all {L : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf α (n + 1)} : φ.IsCountable → φ.all.IsCountable
• iSup {L : Language} {α : Type u'} {n : ℕ} {ι : Type} [Countable ι] {φs : ι → L.BoundedFormulaInf α n} : (∀ (i : ι), (φs i).IsCountable) → (BoundedFormulaInf.iSup φs).IsCountable
• iInf {L : Language} {α : Type u'} {n : ℕ} {ι : Type} [Countable ι] {φs : ι → L.BoundedFormulaInf α n} : (∀ (i : ι), (φs i).IsCountable) → (BoundedFormulaInf.iInf φs).IsCountable

inductive FirstOrder.Language.BoundedFormulaInf.IsKappa {L : Language} {α : Type u'} (κ : Cardinal.{0}) {n : ℕ} : L.BoundedFormulaInf α n → Prop

A formula has all index types with cardinality < κ. This characterizes membership in Lκω.

• falsum {L : Language} {α : Type u'} {κ : Cardinal.{0}} {x✝ : ℕ} : IsKappa κ BoundedFormulaInf.falsum
• equal {L : Language} {α : Type u'} {κ : Cardinal.{0}} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) : IsKappa κ (BoundedFormulaInf.equal t₁ t₂)
• rel {L : Language} {α : Type u'} {κ : Cardinal.{0}} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) : IsKappa κ (BoundedFormulaInf.rel R ts)
• imp {L : Language} {α : Type u'} {κ : Cardinal.{0}} {n : ℕ} {φ ψ : L.BoundedFormulaInf α n} : IsKappa κ φ → IsKappa κ ψ → IsKappa κ (φ.imp ψ)
• all {L : Language} {α : Type u'} {κ : Cardinal.{0}} {n : ℕ} {φ : L.BoundedFormulaInf α (n + 1)} : IsKappa κ φ → IsKappa κ φ.all
• iSup {L : Language} {α : Type u'} {κ : Cardinal.{0}} {n : ℕ} {ι : Type} {φs : ι → L.BoundedFormulaInf α n} : Cardinal.mk ι < κ → (∀ (i : ι), IsKappa κ (φs i)) → IsKappa κ (BoundedFormulaInf.iSup φs)
• iInf {L : Language} {α : Type u'} {κ : Cardinal.{0}} {n : ℕ} {ι : Type} {φs : ι → L.BoundedFormulaInf α n} : Cardinal.mk ι < κ → (∀ (i : ι), IsKappa κ (φs i)) → IsKappa κ (BoundedFormulaInf.iInf φs)

theorem FirstOrder.Language.BoundedFormulaInf.IsKappa.mono {L : Language} {α : Type u'} {n : ℕ} {κ κ' : Cardinal.{0}} (hle : κ ≤ κ') {φ : L.BoundedFormulaInf α n} (h : IsKappa κ φ) : IsKappa κ' φ

IsKappa is monotonic in κ.

theorem FirstOrder.Language.BoundedFormulaInf.mk_lt_aleph_one_of_countable' {ι : Type} [Countable ι] : Cardinal.mk ι < Cardinal.aleph 1

Countable types have cardinality < ℵ₁.

theorem FirstOrder.Language.BoundedFormulaInf.countable_of_mk_lt_aleph_one' {ι : Type} (h : Cardinal.mk ι < Cardinal.aleph 1) : Countable ι

Types with cardinality < ℵ₁ are countable.

theorem FirstOrder.Language.BoundedFormulaInf.IsCountable.toIsKappa_aleph1 {L : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf α n} (h : φ.IsCountable) : IsKappa (Cardinal.aleph 1) φ

IsCountable implies IsKappa ℵ₁.

theorem FirstOrder.Language.BoundedFormulaInf.IsKappa.toIsCountable {L : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf α n} (h : IsKappa (Cardinal.aleph 1) φ) : φ.IsCountable

IsKappa ℵ₁ implies IsCountable.

theorem FirstOrder.Language.BoundedFormulaInf.isCountable_iff_isKappa_aleph1 {L : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf α n} : φ.IsCountable ↔ IsKappa (Cardinal.aleph 1) φ

IsCountable is equivalent to IsKappa ℵ₁.

noncomputable def FirstOrder.Language.BoundedFormulaInf.indexBound {L : Language} {α : Type u'} {n : ℕ} : L.BoundedFormulaInf α n → Cardinal.{u_1}

The supremum of cardinalities of all index types appearing in iSup/iInf constructors. This bounds the "size" of the formula's infinitary structure.

Equations

• FirstOrder.Language.BoundedFormulaInf.falsum.indexBound = 0
• (FirstOrder.Language.BoundedFormulaInf.equal t₁ t₂).indexBound = 0
• (FirstOrder.Language.BoundedFormulaInf.rel R ts).indexBound = 0
• (φ.imp ψ).indexBound = max φ.indexBound ψ.indexBound
• φ.all.indexBound = φ.indexBound
• (FirstOrder.Language.BoundedFormulaInf.iSup φs).indexBound = max (Cardinal.mk ι) (⨆ (i : ι), (φs i).indexBound)
• (FirstOrder.Language.BoundedFormulaInf.iInf φs).indexBound = max (Cardinal.mk ι) (⨆ (i : ι), (φs i).indexBound)

theorem FirstOrder.Language.BoundedFormulaInf.isKappa_succ_indexBound {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaInf α n) : IsKappa (Order.succ φ.indexBound) φ

Every formula belongs to L_(indexBound φ + 1)ω.

theorem FirstOrder.Language.BoundedFormulaInf.exists_isKappa {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaInf α n) : ∃ (κ : Cardinal.{0}), IsKappa κ φ

Every L∞ω formula belongs to some Lκω. This establishes L∞ω as the union of all Lκω.