Woodin's Ω-conjecture

Open

OmegaLogic.omega_conjecture

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

forcinglarge-cardinalsomega-logicset-theory

Woodin's Ω-conjecture. Suppose there is a proper class of Woodin cardinals. Then for every sentence $\varphi$ of the language of set theory,

\emptyset \models_\Omega \varphi \iff \emptyset \vdash_\Omega \varphi .

Here $\emptyset \models_\Omega \varphi$ means that $V^B_\alpha \models \varphi$ for every complete Boolean algebra $B$ and every ordinal $\alpha$ . $\emptyset \vdash_\Omega \varphi$ means that some universally Baire set $A \subseteq \omega^\omega$ has the property that $M_\alpha \models \varphi$ for every strongly $A$ -closed countable transitive model $M$ of ZFC and every ordinal $\alpha \in M$ . All notions are those of the imported definition files.

The "if" direction is soundness (a milestone). The conjecture is therefore the completeness theorem for Ω-logic, which is open.

Preamble

import Definitions.Def_OmegaLogic_Provability
import Definitions.Def_OmegaLogic_LargeCardinals

universe u

Formal statement

namespace OmegaLogic

theorem omega_conjecture (hW : ProperClassWoodin.{u}) (φ : Sent) :
    OmegaValid.{u} ∅ φ ↔ OmegaProvable.{u} ∅ φ := by sorry

end OmegaLogic

Source

Wikipedia, "Ω-logic" (revision oldid=1336097018), section "Analysis", first paragraph ("Woodin's Ω-conjecture asserts that if there is a proper class of Woodin cardinals ... then Ω-logic satisfies an analogue of the completeness theorem"); precise statement from J. Bagaria, N. Castells, P. Larson, "An Ω-logic primer", in Set Theory (Trends in Mathematics), Birkhäuser 2006, pp. 1–28, doi:10.1007/3-7643-7692-9_1; online version https://paulblarson.github.io/omegalogicmaster5.pdf, Section 3, p. 24 ("The Ω-conjecture says: ...").

View graph