{
"$type": "site.standard.document",
"bskyPostRef": {
"cid": "bafyreibh4imnfr2sxljnmifgx56dpncuqe6zortrkdvhbfwxdx5skacks4",
"commit": {
"cid": "bafyreih4ltyhez4ozildpifx2brrdsmqcvvdxvj2zhaqinq5enjc455spq",
"rev": "3mmr4vq4azh2y"
},
"uri": "at://did:plc:g5hiaok54wc2rpigewi75kdu/app.bsky.feed.post/3mmr4vpy4is2z",
"validationStatus": "valid"
},
"content": {
"$type": "pub.leaflet.content",
"pages": [
{
"$type": "pub.leaflet.pages.linearDocument",
"blocks": [
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#link",
"uri": "https://bpb-us-e1.wpmucdn.com/websites.harvard.edu/dist/f/94/files/2022/07/EFI_Woodin_StrongAxiomsOfInfinity.pdf"
}
],
"index": {
"byteEnd": 46,
"byteStart": 28
}
}
],
"plaintext": "Earlier today I discovered Hugh Woodin's work, and at once recognized abstraction based reasoning — the same reasoning software engineers use every day to reason about their code. What follows is the result of synthesizing his work with my experience as a software engineer."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.horizontalRule"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"plaintext": "The proof sketch, stated whole"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The Ω Conjecture — that every Ω-valid sentence has a universally Baire witness — follows from a transfinite induction on logical complexity, structured as follows."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.horizontalRule"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"plaintext": "The conceptual foundation"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Forcing conditions are finite partial definitions — interfaces in the software engineering sense. The forcing relation p ⊩ φ is a sound and complete proof system relative to a fixed forcing notion, by the fundamental theorem of forcing. A generic filter is an impl block — the single object that simultaneously satisfies every accumulated contract obligation. The generic extension M[G] is the concrete type that results from applying the impl block to the ground model."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Ω-validity is the property of holding in every possible impl block of every possible trait hierarchy — truth across all forcing extensions simultaneously. A universally Baire witness is a proof written purely in the contract language — definable without reference to any particular impl block, coherent across all of them simultaneously."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The Ω Conjecture is parametricity for Cohen's type system — every property true of all impl blocks has a proof from the trait hierarchy alone, without inspecting any particular implementation. This is Reynolds' theorem, translated into the forcing setting."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#link",
"uri": "https://en.wikipedia.org/wiki/Forcing_(computability)"
}
],
"index": {
"byteEnd": 31,
"byteStart": 5
}
}
],
"level": 3,
"plaintext": "The Type System Correspondence"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Trait — forcing notion ℙ"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Child trait adding obligations — stronger forcing notion, more constraints"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Trait hierarchy — iterated forcing system"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Dense set — an obligation that every serious completion must meet"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Method implementation — meeting a specific dense set"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "impl block — generic filter G"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Struct or enum being implemented on — the ground model M"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The resulting concrete type with all methods — the generic extension M[G]"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.horizontalRule"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"plaintext": "The Boolean valued model as the pre-forcing witness space"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The key insight is that the witnesses for Ω-valid sentences already exist as ground model objects, before any forcing occurs."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "A Boolean valued model V^𝔹 is constructed entirely within the ground model M. It assigns to every sentence φ a Boolean value ‖φ‖ ∈ 𝔹, where 𝔹 is a complete Boolean algebra. These Boolean values encode the complete truth value structure of φ across all possible forcing extensions simultaneously — before any generic filter is chosen. The generic filter G — the impl block — then selects one particular completion by collapsing the Boolean values to {0,1} via the ultrafilter condition. But V^𝔹 already contained all possible completions, as ground model objects, before G existed."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "This is the forcing analogue of Reynolds' parametricity. In Reynolds' logical relation, the relation is defined before any type instantiation occurs — it is a property of the type itself, not of any particular value at that type. V^𝔹 does exactly the same thing: it defines the complete truth value structure before any particular generic is chosen. The witnesses are properties of the contract language itself, not of any particular completion."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The Boolean values ‖φ‖ ∈ 𝔹 code as sets of reals as follows. The complete theory of any forcing extension — the set of sentences true in it — is a countable object regardless of the size of the forcing notion, since sentences are finite strings over a countable alphabet. These complete theories code canonically into ω^ω, the Baire space of descriptive set theory. The Boolean value ‖φ‖ is then represented as:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.blockquote",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 78,
"byteStart": 0
}
}
],
"plaintext": "A_φ = {r ∈ ω^ω : r codes a complete theory in which ‖φ‖ is realized}"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "A_φ is a set of reals, defined entirely within the ground model via V^𝔹, before any forcing occurs. This coding is uniform across all forcing notions, countable and uncountable, because it operates on complete theories rather than on forcing conditions directly. The Ω Conjecture reduces to: for every Ω-valid φ, A_φ is universally Baire."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 3,
"plaintext": "The critical case: Σ²₁ sentences"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
],
"index": {
"byteEnd": 386,
"byteStart": 184
}
}
],
"plaintext": "The heart of the Ω Conjecture concerns Ω-valid Σ²₁ sentences — sentences of the form ∃X⊆ℝ φ(X) where φ is projective. In the Boolean valued model, ‖∃Xφ(X)‖ = ⋁X ‖φ(X)‖ — the join over all witnesses X, computed in 𝔹 before any forcing. This join is a ground model object. In the induction below, this is the existential quantification successor case: A{∃Xφ} is the projection of A_φ, which is universally Baire under a proper class of Woodin cardinals. The forcing witnessing the Σ²₁ sentence is encoded in the Boolean join — the existential witness X is already present in V^𝔹 at the level of Boolean values, before any generic is chosen."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.horizontalRule"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"plaintext": "The logical relation"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Define R(p, φ) in Boolean valued model terms:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.blockquote",
"plaintext": "R(p, φ) holds if and only if ‖φ‖ ≥ p in the Boolean algebra 𝔹."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "This is a ground model statement. It says p is a lower bound for the Boolean value of φ — meaning every completion honoring p satisfies φ. No quantification over forcing extensions is needed, because V^𝔹 already contains all completions simultaneously as a ground model object."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The witness set A_φ is the set of reals representing ‖φ‖ as defined above. The logical operations on Boolean values correspond directly to operations on witness sets:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.unorderedList",
"children": [
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Conjunction: ‖φ∧ψ‖ = ‖φ‖ ∧ ‖ψ‖ — meet in 𝔹, corresponding to A_φ ∩ A_ψ"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Negation: ‖¬φ‖ = ¬‖φ‖ — Boolean complement in 𝔹, corresponding to the complement of A_φ"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Existential quantification: ‖∃xφ‖ = ⋁_x ‖φ(x)‖ — join in 𝔹, corresponding to the projection of A_φ"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
],
"index": {
"byteEnd": 49,
"byteStart": 29
}
},
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
],
"index": {
"byteEnd": 123,
"byteStart": 115
}
}
],
"plaintext": "Countable conjunction: ‖∧{n<ω} φ_n‖ = ⋀{n<ω} ‖φ_n‖ — countable meet in 𝔹, corresponding to ∩{n<ω} A{φ_n}"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
],
"index": {
"byteEnd": 56,
"byteStart": 31
}
},
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
],
"index": {
"byteEnd": 142,
"byteStart": 130
}
}
],
"plaintext": "Uncountable conjunction: ‖∧{β<ω₁} φ_β‖ = ⋀{β<ω₁} ‖φ_β‖ — ω₁-length meet in 𝔹, corresponding to ∩{β<ω₁} A{φ_β}"
}
}
]
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "All of these operations are performed in 𝔹 before forcing occurs. The induction shows that each operation preserves the universally Baire property of the corresponding witness sets."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.horizontalRule"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"plaintext": "The induction"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Run a transfinite induction on the logical complexity of φ, measured by position in the analytical hierarchy. At each stage, the witness A_φ is the Boolean value ‖φ‖ represented as a set of reals in ω^ω — a ground model object constructed in V^𝔹 before any forcing."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 10,
"byteStart": 0
}
}
],
"plaintext": "Base case: φ is arithmetic. Arithmetic truth is forcing-absolute — ‖φ‖ is either 𝟙 (the top element of 𝔹, meaning φ holds in all extensions) or 𝟘 (meaning φ holds in none). So A_φ is Borel, defined by a simple arithmetic condition on complete theories. Universally Baire trivially, since Borel sets are universally Baire without large cardinal assumptions."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 31,
"byteStart": 0
}
}
],
"plaintext": "Successor case — conjunction: ‖φ∧ψ‖ = ‖φ‖ ∧ ‖ψ‖ in 𝔹. A_{φ∧ψ} = A_φ ∩ A_ψ. Finite intersections of universally Baire sets are universally Baire. No additional assumptions needed."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 28,
"byteStart": 0
}
},
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#code"
}
],
"index": {
"byteEnd": 198,
"byteStart": 184
}
}
],
"plaintext": "Successor case — negation: ‖¬φ‖ = ¬‖φ‖ in 𝔹 — the Boolean complement. A_{¬φ} is the complement of A_φ in the appropriate sense. This is the forcing analogue of unreachable!() in Rust — the never type, asserting that the path to φ is blocked in every completion honoring the relevant conditions. The Boolean complement is computed in 𝔹 before forcing. Under a proper class of Woodin cardinals, complements of universally Baire sets are universally Baire. So A_{¬φ} is universally Baire given A_φ is."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 46,
"byteStart": 0
}
},
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
],
"index": {
"byteEnd": 147,
"byteStart": 66
}
}
],
"plaintext": "Successor case — existential quantification: ‖∃xφ‖ = ⋁x ‖φ(x)‖ in 𝔹 — the join over all witnesses, computed before forcing. A{∃xφ} is the projection of A_φ. This is the critical Σ²₁ case. Under a proper class of Woodin cardinals, projections of universally Baire sets are universally Baire. So A_{∃xφ} is universally Baire given A_φ is."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 33,
"byteStart": 0
}
},
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
],
"index": {
"byteEnd": 61,
"byteStart": 41
}
},
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
],
"index": {
"byteEnd": 158,
"byteStart": 140
}
}
],
"plaintext": "Countable limit case — λ = ω: ‖∧{n<ω} φ_n‖ = ⋀{n<ω} ‖φ_n‖ — a countable meet in 𝔹, computed before forcing. A_{∧{n<ω} φ_n} = ∩{n<ω} A_{φ_n}. Countable meets and joins in a complete Boolean algebra are well-defined ground model objects. Countable intersections and unions of universally Baire sets are universally Baire, by closure of the Baire property under countable Boolean operations. No large cardinal assumptions beyond what we already have."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "This corresponds to countably infinite trait hierarchies — ω × ω = ω method obligations total, still countable."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 38,
"byteStart": 0
}
},
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
],
"index": {
"byteEnd": 71,
"byteStart": 46
}
},
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
],
"index": {
"byteEnd": 182,
"byteStart": 159
}
}
],
"plaintext": "Uncountable limit case — λ = ω₁: ‖∧{β<ω₁} φ_β‖ = ⋀{β<ω₁} ‖φ_β‖ — an ω₁-length meet in 𝔹, computed before forcing. A_{∧{β<ω₁} φ_β} = ∩{β<ω₁} A_{φ_β}. The total coherence burden is ω₁ × ω₁ — uncountable in a genuinely two-dimensional way, qualitatively different from the countable case."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "This corresponds to uncountably infinite trait hierarchies — ω₁ × ω = ω₁ method obligations total. A proper class of Woodin cardinals is insufficient here. A supercompact cardinal κ with the closure property M^{ω₁} ⊆ M guarantees that ω₁-length meets in 𝔹 correspond to universally Baire sets — because the inner model M generated by the supercompact embedding contains all ω₁-sequences of its elements, making the ω₁-length meet visible as a single coherent ground model object."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 19,
"byteStart": 0
}
}
],
"plaintext": "General limit case: For limit ordinals λ beyond ω₁, the same argument applies. The supercompact cardinal provides M^λ ⊆ M closure for each relevant λ, covering all lengths simultaneously. Every transfinite meet in 𝔹 is a ground model object whose corresponding witness set is universally Baire. The induction goes through at every limit stage."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.horizontalRule"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"plaintext": "The conclusion"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "By transfinite induction, A_φ is universally Baire for every sentence φ in the analytical hierarchy. The witnesses are ground model objects — Boolean values in V^𝔹, represented as sets of reals in ω^ω — constructed before any forcing occurs. Every Ω-valid sentence has a universally Baire witness. The Ω Conjecture holds."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The large cardinal assumptions used are:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.unorderedList",
"children": [
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "A proper class of Woodin cardinals — for the successor cases: negation, existential quantification, and the critical Σ²₁ projection argument"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "A supercompact cardinal — for the uncountable limit cases: ω₁-length and longer meets in 𝔹"
}
}
]
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "These are exactly the assumptions underlying Woodin's Ultimate L program, which assumes an extendible cardinal — one level above supercompact — giving the proof comfortable room within Woodin's own framework."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.horizontalRule"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 2,
"plaintext": "What remains"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "This is a proof sketch, not a complete proof. The following gaps require further work:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.orderedList",
"children": [
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The logical relation R(p, φ), defined as ‖φ‖ ≥ p in 𝔹, needs to be shown equivalent to Woodin's specific certification condition for Ω-provability — that the universally Baire set A_φ certifies φ in Woodin's precise technical sense."
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The truth value coding via complete theories — representing ‖φ‖ as a set of reals in ω^ω — needs to be verified as producing universally Baire sets at each stage of the induction, and not merely sets of reals."
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The transfinite induction needs a formal well-foundedness argument."
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The supercompact cardinal argument at the uncountable limit case needs to be made fully precise — specifically, that M^{ω₁} ⊆ M is exactly the closure property needed for ω₁-length meets in 𝔹 to correspond to universally Baire sets of reals."
}
}
],
"startIndex": 1
}
}
],
"id": "019e6485-119c-700e-99be-459db5d3b0d8"
}
]
},
"description": "Set theoretic forcing is a type system.",
"path": "/3mmr4vlz42c2z",
"publishedAt": "2026-05-26T13:45:57.837Z",
"site": "https://leaflet.pub/p/did:plc:g5hiaok54wc2rpigewi75kdu",
"tags": [
"type system",
"Rust",
"large cardinals",
"woodin",
"Ω conjecture",
"continuum hypothesis",
"math"
],
"title": "Proof sketch of Hugh Woodin's Ω conjecture"
}