Prove2Me

PFA implies SCH

Open
SingularCardinals.sch_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 singular cardinals hypothesis holds: for every singular strong limit cardinal κ\kappa,

2κ=κ+.2^\kappa=\kappa^+.

Since PFA refutes GCH, this shows SCH follows from hypotheses of a very different kind than 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 sch_of_pfa (h : PFA.{u}) : SCH.{u} := 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 ... also implies SCH".
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