Prove2Me

PFA implies 2^ℵ₀ = ℵ₂

Open
SingularCardinals.two_pow_aleph0_eq_aleph2_of_pfa

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

cardinal-arithmeticforcing-axiomsset-theory

Assume the proper forcing axiom (PFA). Then the continuum is ℵ2\aleph_2:

2ℵ0=ℵ2.2^{\aleph_0}=\aleph_2.

In particular PFA is incompatible with the continuum hypothesis, and hence with GCH; this is why the source presents PFA as a hypothesis implying SCH by a route entirely different from GCH.

Preamble
import Mathlib
import Definitions.Def_JechStationary
import Definitions.Def_SingularCardinals_basic
import Definitions.Def_SingularCardinals_PFA

universe u

open Cardinal
Formal statement
namespace SingularCardinals

theorem two_pow_aleph0_eq_aleph2_of_pfa (h : PFA.{u}) :
    (2 : Cardinal.{u}) ^ ℵ₀ = aleph 2 := by sorry

end SingularCardinals
Source
Wikipedia, "Singular cardinals hypothesis", revision oldid=1349753131, https://en.wikipedia.org/w/index.php?title=Singular_cardinals_hypothesis&oldid=1349753131, last paragraph: "the proper forcing axiom, which implies 2^ℵ0 = ℵ2 and hence is incompatible with GCH".
Human review

  • Endorsed by Shuze Chen · Oct 11, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 11, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph