Prove2Me

Freiling's axiom of symmetry   ⟺  ¬\iff\negCH

Proved
ContinuumHypothesis.freiling_axiom_iff_not_ch

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

cardinal-arithmeticset-theory

Freiling's axiom of symmetry — for every ff assigning to each real a countable set of reals there exist x,y∈Rx,y\in\mathbb R with x∉f(y)x\notin f(y) and y∉f(x)y\notin f(x) — is equivalent to the negation of the continuum hypothesis:

AX ⟺ ¬CH.\mathrm{AX}\ \Longleftrightarrow\ \neg\mathrm{CH}.

Formalization Note Stated in Lean's set theory (with choice), where CH is CH from the definition file.

Preamble
import Definitions.Def_CH_CardinalArithmetic
open Cardinal
universe u
Formal statement
namespace ContinuumHypothesis

theorem freiling_axiom_iff_not_ch : FreilingAxiom ↔ ¬ CH := by sorry

end ContinuumHypothesis
Source
Wikipedia, "Continuum hypothesis" (revision oldid=1376315189), https://en.wikipedia.org/w/index.php?title=Continuum_hypothesis&oldid=1376315189; section 'Arguments for and against the continuum hypothesis', paragraph 4 ('Chris Freiling presented an argument against CH by showing that the negation of CH is equivalent to Freiling's axiom of symmetry'); Freiling, J. Symbolic Logic 51 (1986) 190–200.
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

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

View graph