Set theory axioms beyond ZFC

Some implications between topological properties are consistent under ZFC, but not provable etc (i.e. Cardinality < 𝔠 → Cardinality < ℵ₁).

We still want to be able to argue about such pathological examples. Thus, this file introduces three typeclasses for common set theoretic axioms (CH, GCH and MA) and proves implications about them.

Note that it is not possible in Lean to define some sort of Unprovable : Prop → Prop; to do this one would need to model first order logic (or some other foundation) within Lean; this has been done before for example here.

Some code in this file is due to Eric Wieser, in particular from https://github.com/leanprover-community/mathlib4/pull/34075.

Main declarations

• ContinuumHypothesis: Typeclass for the (positive answer to the) continuum hypothesis.
• NotContinuumHypothesis: Typeclass for the negation of the continuum hypothesis.
• GeneralizedContinuumHypothesis: Typeclass for the eneralized continuum hypothesis.
• MartinsAxiom: Typeclass for Martin's axiom.
• instMartinsAxiomOfContinuumHypothesis: The continuum hypothesis implies Martin's axiom.

How to use

When writing some statement in Lean that holds in ZFC + n inacessible cardinals where n < ℵ₀, no assumption on the continuum hypothesis or other axioms should be included.

In some cases however, certain constructions or implications only work under additional assumpions. In this case, use the typeclasses given, i.e. for some theorem that is (only) true under the continuum hypothesis, add [ContinuumHypothesis] as an argument.

Since Martin's axiom is implied by the continuum hypothesis, right now following combinations are allowed (consistent w.r.t. ZFC):

• [MartinsAxiom]
• [NotContinuumHypothesis]
• [MartinsAxiom], [NotContinuumHypothesis]
• [ContinuumHypothesis]
• [GeneralizedContinuumHypothesis]

Both including ContinuumHypothesis and NotContinuumHypothesis for instance let's us prove false and thus ought to be never done.

Again, extra axiom assumptions should only be added when it is truly necessary.

class PiBase.ContinuumHypothesis : Prop

The statement that the continuum hypothesis holds.

To avoid a universe parameter, we only state that this holds in universe 0, since it can be lifted to other universes with subsequent theorems.

See ContinuumHypothesis.iff_aleph0_covby_continuum and ContinuumHypothesis.iff_continuum_eq_aleph_one for typical characterizations.

• of_continuum_eq_aleph_one' :: (
• continuum_eq_aleph_one' : Cardinal.continuum = Cardinal.aleph 1
• )

theorem PiBase.ContinuumHypothesis.iff_continuum_eq_aleph_one' : ContinuumHypothesis ↔ Cardinal.continuum = Cardinal.aleph 1

theorem PiBase.ContinuumHypothesis.iff_continuum_eq_aleph_one : ContinuumHypothesis ↔ Cardinal.continuum = Cardinal.aleph 1

@[simp]

theorem PiBase.ContinuumHypothesis.continuum_eq_aleph_one [ContinuumHypothesis] : Cardinal.continuum = Cardinal.aleph 1

theorem PiBase.ContinuumHypothesis.of_continuum_eq_aleph_one : Cardinal.continuum = Cardinal.aleph 1 → ContinuumHypothesis

Alias of the reverse direction of PiBase.ContinuumHypothesis.iff_continuum_eq_aleph_one.

theorem PiBase.ContinuumHypothesis.iff_aleph0_covby_continuum : ContinuumHypothesis ↔ Cardinal.aleph0 ⋖ Cardinal.continuum

theorem PiBase.ContinuumHypothesis.aleph0_covby_continuum [ContinuumHypothesis] : Cardinal.aleph0 ⋖ Cardinal.continuum

theorem PiBase.ContinuumHypothesis.of_aleph0_covby_continuum : Cardinal.aleph0 ⋖ Cardinal.continuum → ContinuumHypothesis

Alias of the reverse direction of PiBase.ContinuumHypothesis.iff_aleph0_covby_continuum.

class PiBase.NotContinuumHypothesis : Prop

• of_aleph_one_lt_continuum' :: (
• aleph_one_lt_continuum' : Cardinal.aleph 1 < Cardinal.continuum
• )

theorem PiBase.NotContinuumHypothesis.iff_aleph_one_lt_continuum' : NotContinuumHypothesis ↔ Cardinal.aleph 1 < Cardinal.continuum

theorem PiBase.NotContinuumHypothesis.iff_aleph_one_lt_continuum : NotContinuumHypothesis ↔ Cardinal.aleph 1 < Cardinal.continuum

@[simp]

theorem PiBase.NotContinuumHypothesis.aleph_one_lt_continuum [NotContinuumHypothesis] : Cardinal.aleph 1 < Cardinal.continuum

theorem PiBase.NotContinuumHypothesis.of_aleph_one_lt_continuum : Cardinal.aleph 1 < Cardinal.continuum → NotContinuumHypothesis

Alias of the reverse direction of PiBase.NotContinuumHypothesis.iff_aleph_one_lt_continuum.

theorem PiBase.NotContinuumHypothesis.iff_not_continuumHypothesis : NotContinuumHypothesis ↔ ¬ContinuumHypothesis

class PiBase.GeneralizedContinuumHypothesis : Prop

Staement of the generalized continuum hypothesis. Note this unfortunately is universe dependent, which is unavoidable.

• succ_cardinal_eq_pow {o : Ordinal.{u}} : Cardinal.aleph0 ≤ Cardinal.aleph o → Cardinal.aleph (o + 1) = 2 ^ Cardinal.aleph o

instance PiBase.instGeneralizedContinuumHypothesis [h : GeneralizedContinuumHypothesis] : GeneralizedContinuumHypothesis

instance PiBase.instContinuumHypothesisOfGeneralizedContinuumHypothesis [h : GeneralizedContinuumHypothesis] : ContinuumHypothesis

def PiBase.MartinsAxiomFor (k : Cardinal.{u}) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem PiBase.martinsAxiomFor_of_le {k c : Cardinal.{u}} (h : k ≤ c) (hc : MartinsAxiomFor c) : MartinsAxiomFor k

theorem PiBase.not_martinsAxiomFor_continuum_bot : ¬MartinsAxiomFor Cardinal.continuum

theorem PiBase.martinsAxiomFor_le_aleph0 {c : Cardinal.{u}} (hc : c ≤ Cardinal.aleph0) : MartinsAxiomFor c

class PiBase.MartinsAxiom : Prop

• martins_axiom_for_lt (k : Cardinal.{0}) : k < Cardinal.continuum → MartinsAxiomFor k

  TODO: add universe independent version, similar as we have for CH

theorem PiBase.martinsAxiom_iff : MartinsAxiom ↔ ∀ k < Cardinal.continuum, MartinsAxiomFor k

instance PiBase.instMartinsAxiomOfContinuumHypothesis [h : ContinuumHypothesis] : MartinsAxiom