Ω-Logic
Origin. W. Hugh Woodin, The Axiom of Determinacy, Forcing Axioms, and the Nonstationary Ideal (1999) and "The continuum hypothesis, parts I and II" (Notices of the AMS, 2001). Bagaria, Castells, and Larson's survey (2006) is the standard introduction. Built for one question: whether the continuum hypothesis has a truth value that forcing cannot touch.
Models. Forcing is why set theory is independent — Cohen's method changes the truth of CH without changing the axioms. Woodin's response is to define a consequence relation whose validity is invariant under forcing: whatever forcing can do, it cannot change what follows in Ω-logic. If such a relation is complete, then the questions forcing leaves open are answered by something, and the multiverse of forcing extensions has a definite theory after all.
Formalism.
Ω-validity (semantic): T ⊨_Ω φ iff for every complete Boolean algebra B and every ordinal α, if V^B_α ⊨ T then V^B_α ⊨ φ. Quantifies over every forcing extension and every rank initial segment of it.
Ω-provability (syntactic): T ⊢_Ω φ iff there is a universally Baire set A ⊆ ℝ such that every A-closed transitive model of T satisfies φ. The universally Baire set is the "proof" — a real object playing the role a derivation plays.
Soundness: Given a proper class of Woodin cardinals: T ⊢_Ω φ implies T ⊨_Ω φ. Proved.
The Ω-conjecture: T ⊨_Ω φ implies T ⊢_Ω φ. Completeness of Ω-logic. Open since 1999.
Generic absoluteness: Given a proper class of Woodin cardinals, Ω-validity is itself invariant under forcing — so the relation is not one more thing forcing can move. This is what the large cardinals buy and why the programme needs them.
The CH argument: Woodin argued that if the Ω-conjecture holds and there is a proper class of Woodin cardinals, then any Ω-complete axiomatization of H(ω₂) implies ¬CH — and 2^ℵ⁰ = ℵ₂ specifically. The argument makes CH a definite question with a probable answer.
The reversal: Woodin later moved to the Ultimate-L programme, on which CH is true in the final inner model. The Ω-logic argument and the Ultimate-L argument point opposite ways, and their author holds the second. Both remain in the literature.
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| ⊨_Ω | U+22A8 | Ω-validity | True in all forcing extensions' ranks |
| ⊢_Ω | U+22A2 | Ω-provability | Witnessed by a universally Baire set |
| V^B | — | Forcing extension | Boolean-valued model |
| H(ω₂) | — | Hereditarily < ℵ₂ | The structure the CH argument axiomatizes |
| CH | — | Continuum hypothesis | 2^ℵ⁰ = ℵ₁ |
Metatheory. Ω-logic is the strongest attempt to make CH a question rather than a choice, and its whole force rests on an open conjecture. Generic absoluteness of Ω-validity, given Woodins, is the real theorem: it shows the relation is stable against the method that produced the independence, which is what a forcing-proof logic would have to be. That the author of the CH argument now argues the other way is not a scandal but a datum — the Ω-conjecture would settle the method and not the answer, and Woodin's two programmes disagree about which axioms the settled method should be applied to.
Applies to. The continuum problem and the status of independence. Large cardinals, whose proper class is the hypothesis throughout. The multiverse debate, where Ω-logic is the strongest case for a single universe. Generic absoluteness and forcing-invariant truth.
Limitations. The Ω-conjecture is open after twenty-five years and everything depends on it — soundness without completeness makes Ω-logic a relation with a proof system that may not reach its validities. Ω-provability is not recursively enumerable: the "proofs" are universally Baire sets, so the syntax is as set-theoretic as the semantics and the analogy to a proof system is formal rather than epistemic. And the CH argument's conclusion is not stable even in its author's hands, which is the clearest evidence that the programme establishes a framework rather than a fact.
© 2026 Lingenic LLC