Large cardinals

Cardinals with strong closure or reflection properties, such as inaccessible, Mahlo, weakly compact and measurable cardinals, whose existence cannot be proved in ZFC.

• Inaccessible cardinals
• Mahlo cardinals

DefinitionMeasurable cardinal#✓fully proved

A cardinal κ is measurable if κ > ℵ₀ and there is a set I with |I| = κ carrying an ultrafilter U on I which is

1. κ-complete: for every family 𝒮 ⊆ U with |𝒮| < κ we have ⋂ 𝒮 ∈ U; and
2. nonprincipal: every cofinite subset of I belongs to U --- equivalently, since U is an ultrafilter, no finite subset of I belongs to U.

def IsMeasurable.{u} (κ : Cardinal.{u}) : Prop :=
  ℵ₀ < κ ∧
  ∃ (I : Type u) (_ : #I = κ) (U : Ultrafilter I),
    CardinalInterFilter (U : Filter I) κ ∧ (U : Filter I) ≤ Filter.cofinite

DefinitionWeakly compact cardinal#✓fully proved

A cardinal \(\kappa\) is weakly compact if \(\aleph_0 < \kappa\) and \(\kappa \to (\kappa)^2_2\): for every set \(I\) of cardinality \(\kappa\) and every colouring \(c\) of the finite subsets of \(I\) with two colours, there are a subset \(H \subseteq I\) of cardinality \(\kappa\) and a colour \(k\) such that \(c(s) = k\) for every two-element subset \(s \subseteq H\).

def IsWeaklyCompact (κ : Cardinal) : Prop :=
  ℵ₀ < κ ∧
  ∀ (I : Type) (_ : #I = κ) (F : Finset I → Bool),
    ∃ (H : Set I) (_ : #H = κ) (k : Bool), IsHomogeneousFor 2 F H k

Uses 1

Statement usesHomogeneous set

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.