Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Shelah's Baire-Property Model and Inner-Model Lower Bounds

1 · Prerequisites

2 · Summary

This pair runs two independent consistency arguments through one page. The upper branch builds Shelah's model of the Baire property from ZFC alone; the lower branch shows that universal Lebesgue measurability is equiconsistent with an inaccessible cardinal. Both branches are stated with their exact choice costs, and neither consumes a recorded result.

Quotient convention used throughout. Several items below write $q \in Q / P$ for a complete suborder $P$ of $B A (Q)$ , following Shelah's Section 7.1: the quotient $Q / P = {q \in Q : q$ is compatible in $Q$ with every condition of the generic filter on $P}$ is a $P$ -name of a forcing notion below $Q$ , and $p ⊩ q \in Q / P$ holds exactly when every $p^{'} \in P$ with $p^{'} \leq p$ is compatible with $q$ (Forcing preorders, compatibility and filters). Two elementary consequences are used repeatedly: the assertion is upward closed in $q$ , and it is monotone in $p$ , so $p^{'} ⊩ q \in Q / P$ for every $p^{'} \leq p$ with $p ⊩ q \in Q / P$ and $p^{'} ⊩ q^{'} \in Q / P$ for every $q^{'} \in Q$ with $q \leq q^{'}$ . The convention enters in Sweet density transfers along complete suborders, Shelah amalgamation preserves sweetness and Composition with universal-meagre forcing preserves sweetness, and it is the only sense in which the expression $Q / P$ is used on this page.

The upper branch starts from sweetness models for forcing: a dense set with countably many classes per level, directed classes, sequential lower bounds and the transfer clause, together with the extension relation between models. Sweet forcings are countable unions of directed sets and hence ccc; Claim 7.4's uniform density transfer and the amalgamation theorem build new conditions along a complete suborder; universal-meagre forcing and, under AC, its two-step composition preserve sweetness and absorb all old closed nowhere-dense sets into one coded meagre envelope. Continuous countable unions, the partial-isomorphism extension and a CH-length bookkeeping recursion then produce one ccc complete Boolean algebra of size $ω_{1}$ whose countably generated complete subalgebras are homogeneous enough to turn generic truth about a countable ordinal sequence into an open approximation modulo meagre error. The hereditary ordinal-sequence-definable inner model $N = H O D (S)$ satisfies ZF+DC, has the same reals and ordinals, and every set of reals in it has the Baire property; Shelah's published conclusion gives the equiconsistency of ZFC and ZF+DC plus universal Baire property with no inaccessible hypothesis. The full-extension definable-Baire clause comes directly from the same source theorem, not by transferring witnesses upward from $N$ .

The lower branch works from RAISONNIER filters: rapid filters extending the Fréchet filter are non-measurable by Mokobodzki's argument, the Raisonnier family $F (x)$ is a $Σ_{3}^{1} (x)$ filter, and the $Σ_{2}^{1} (x)$ null-code order together with Fubini makes the constructible null union null, which makes $F (x)$ rapid. Hence boldface $Σ_{3}^{1}$ measurability forces the ambient $ω_{1}$ to be inaccessible in $L$ ; with the published Solovay Levy-collapse construction this is exactly the consistency strength of an inaccessible, and the separating model shows that universal Baire property does not imply universal measurability. The equiconsistency statements separately calibrate the sufficient hypotheses for the two constructions; they are not used to assert an unproved nonimplication between bare consistency statements.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Shelah sweetness models for forcing

Definition

The library order convention is used throughout: a forcing preorder $P$ carries a reflexive transitive relation in which $q \leq p$ means that $q$ is stronger than $p$ (Forcing preorders, compatibility and filters).

A Shelah sweetness model is a triple $(P, D, (E_{n})_{n < ω})$ such that

$P$ is a forcing preorder with a distinguished weakest condition $1_{P}$ (so $p \leq 1_{P}$ for every $p \in P$ ), and $D \subseteq P$ is dense; the weak condition need not belong to $D$ ;
each $E_{n}$ is an equivalence relation on $D$ with countably many classes, and $E_{n + 1}$ refines $E_{n}$ , that is, $p E_{n + 1} p^{'}$ implies $p E_{n} p^{'}$ ;
every $E_{n}$ -class is downward directed: any two members of the class have a common lower bound that also belongs to the class;

and the two clauses below hold.

Sequential clause. If $p_{i} \in D$ for every $i \leq ω$ and $p_{i} E_{i} p_{ω}$ for every $i < ω$ , then ${p_{i} : i \leq ω}$ has a common lower bound; moreover for every $n < ω$ the tail ${p_{i} : n \leq i \leq ω}$ has a common lower bound that lies in the $E_{n}$ -class of $p_{ω}$ .

Transfer clause. For all $p, q \in D$ and every $n < ω$ there is $k < ω$ such that for every $p^{'} E_{k} p$ : if some $r E_{n} q$ satisfies $r \leq p$ , then some $r^{'} E_{n} q$ satisfies $r^{'} \leq p^{'}$ .

Comparable form. The transfer clause is equivalent to the following statement, which is the form used below whenever a condition has to be synchronized with a comparable one. If $q \leq p$ in $D$ and $n < ω$ , then for some $k < ω$ every $p^{'} E_{k} p$ has a common strengthening inside the $E_{n}$ -class of $q$ : there is $q^{'} E_{n} q$ with $q^{'} \leq q$ and $q^{'} \leq p^{'}$ . For the forward implication apply the transfer clause to $p, q, n$ , using $r = q$ as the required witness that some member of the $E_{n}$ -class of $q$ lies below $p$ ; it yields $r^{'} E_{n} q$ with $r^{'} \leq p^{'}$ , and downward directedness of the class applied to the pair $q, r^{'}$ supplies $q^{'} E_{n} q$ with $q^{'} \leq q, r^{'}$ . For the converse reading, suppose the hypothesis of the transfer clause holds for a triple $p, q, n$ and a witness $r E_{n} q$ with $r \leq p$ ; applying the comparable form to the pair $r \leq p$ and to $n$ gives a single $k$ such that every $p^{'} E_{k} p$ has a common strengthening with $r$ inside the class of $r$ , which is also the class of $q$ , and this $k$ serves the transfer clause, because $E_{n}$ -equivalent conditions determine the same $E_{n}$ -class. If there is no witness $r$ , the transfer implication is vacuous and $k = 0$ suffices.

Extension of sweetness models. A sweetness model $M_{2} = (P_{2}, D_{2}, (E_{n}^{2}))$ extends $M_{1} = (P_{1}, D_{1}, (E_{n}^{1}))$ when

$P_{1}$ is a complete suborder of $P_{2}$ , that is, $P_{1} \subseteq P_{2}$ , the order and incompatibility relations on $P_{1}$ are the restrictions of those on $P_{2}$ , and every maximal antichain of $P_{1}$ is maximal in $P_{2}$ . This is not a density requirement: an arbitrary condition of $P_{2}$ need not have a stronger condition in $P_{1}$ ;
$D_{1} \subseteq D_{2}$ ;
each old $E_{n}^{1}$ is the restriction of $E_{n}^{2}$ to $D_{1}$ ;
for every $p \in D_{1}$ and every $n < ω$ , its $E_{n}^{2}$ -class is contained in $P_{1}$ ;
whenever $p \in D_{2}$ , $q \in P_{1}$ and $q \leq p$ , then $p \in D_{1}$ .

The last clause is equivalent to restricting $q$ to $D_{1}$ , as in the source: if $q \in P_{1}$ strengthens $p$ , density of $D_{1}$ in $P_{1}$ gives a $d \in D_{1}$ with $d \leq q \leq p$ , to which the restricted clause applies. Thus in particular $D_{2} \cap P_{1} = D_{1}$ , and the preceding class-containment clause may equivalently say that every $E_{n}^{2}$ -class meeting $D_{1}$ is contained in $D_{1}$ . Standard iteration-stage inclusions are complete suborders in this sense.

Boolean-algebra language. By Forcing equivalence and Boolean completion, $P$ is forcing-equivalent to the nonzero part $B^{+} = B ∖ {0_{B}}$ of its regular-open completion (Completeness, regular opens, and order continuity). This assertion concerns forcing and generic extensions; it does not by itself identify the conditions of $D$ or transport their equivalence relations through a possibly noninjective separative quotient. When $BA (P)$ is used as shorthand for a sweetness presentation, the original $P, D, (E_{n})$ data are retained unless a transport has been specified.

In particular, if $e : P \to B^{+}$ is a dense order embedding (injective and preserving and reflecting order), one may use $e [D]$ as the dense set and transport each $E_{n}$ along the bijection $e ∣_{D}$ . Density follows by first refining a Boolean condition into $e [P]$ and then refining its preimage into $D$ . Countability, refinement and class directedness are preserved. In the sequential clause an original lower bound $r \in P$ gives the nonzero lower bound $e (r)$ ; the class-tail bounds similarly map into the required classes. The transfer clause is preserved because its comparisons between members of $D$ are equivalent to their image comparisons under the order embedding. Thus these data give a sweetness model on $B^{+}$ . This sufficient hypothesis is not imposed on arbitrary forcing preorders, whose canonical completion map may identify distinct conditions or fail to reflect the original order.

If a model is specified directly on a complete Boolean algebra, it means a model on $B^{+}$ with the displayed sweetness clauses checked there. Every common lower bound in these clauses must be nonzero: zero lies below even a Boolean element and its complement, and cannot witness compatibility. The one-element Boolean algebra has empty $B^{+}$ and hence cannot underlie a forcing preorder under the library's nonemptiness convention.

The weak-condition requirement is part of the forcing interface used by the source constructions, not a consequence of sweetness. In particular it rules out a bare antichain with no common weak condition as an input to the amalgam construction. In products, canonical copies and twisted amalgams below, an unmentioned coordinate is filled with its distinguished weak condition.

LemmaStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

Sweet forcings are countable unions of directed sets and ccc

Statement

If $(P, D, (E_{n}))$ is a sweetness model, then $D$ , and hence $P$ , is a countable union of directed subsets. Consequently every antichain in $P$ is countable, so $P$ satisfies the countable chain condition.

Facts & Assumptions

Given: A sweetness model $(P, D, (E_{n})_{n < ω})$ as in the Statement.

[F1]

Shelah sweetness models for forcing: $D$ is dense in $P$ , the relation $E_{0}$ has countably many classes, and each $E_{0}$ -class is downward directed.

[F2]

Closure, distributivity, and chain conditions for forcing orders: a forcing order is ccc when every antichain has cardinality below $ℵ_{1}$ , and this counts as $ℵ_{1}$ -cc.

Proof

1.1

The classes of $E_{0}$ form a countable partition of $D$ into nonempty sets, so fix a surjection $m \mapsto C_{m}$ from $ω$ onto the set of classes, which exists because a countable set of nonempty sets is the image of a function on $ω$ ; for $m < ω$ let $A_{m} = {p \in P : some q \in C_{m} satisfies q \leq p}$ be the upward closure of $C_{m}$ inside $P$ .

2.1

Each $A_{m}$ is directed: if $p_{1}, p_{2} \in A_{m}$ are witnessed by $q_{1}, q_{2} \in C_{m}$ with $q_{j} \leq p_{j}$ , then downward directedness of the class supplies $q \in C_{m}$ with $q \leq q_{1}, q_{2}$ , hence $q \leq p_{1}, p_{2}$ and $q \in A_{m}$ is the required common lower bound.

F1step 1.1

2.2

$P = ⋃_{m < ω} A_{m}$ : given $p \in P$ , density of $D$ supplies $q \in D$ with $q \leq p$ , the classes cover $D$ , so $q \in C_{m}$ for some $m$ , and then $p \in A_{m}$ by definition.

F1step 1.1

3.1

$D = ⋃_{m < ω} C_{m}$ exhibits $D$ as a countable union of directed sets, since each class $C_{m}$ is downward directed; combined with step 2.2 this shows that both $D$ and $P$ are countable unions of directed subsets.

F1step 2.1step 2.2

3.2

Let $A \subseteq P$ be an antichain, that is, a set of pairwise incompatible conditions: by step 2.2 each $a \in A$ lies in some $A_{m}$ , so $f (a) = \min {m < ω : a \in A_{m}}$ is defined on $A$ , and it is injective, since $f (a) = f (b) = m$ with $a \neq b$ would put $a, b$ in the directed set $A_{m}$ and give them a common lower bound; hence $A$ injects into $ω$ and is countable.

step 2.1step 2.2

4.1

Every antichain of $P$ is countable by step 3.2, so $P$ is ccc in the sense of [F2], which is $ℵ_{1}$ -cc.

F2step 3.2∎

LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

Sweet density transfers along complete suborders

Statement

Assume ZFC. Let $P$ be a complete suborder of $B^{+} = B A (Q) ∖ {0_{B}}$ (write $B = B A (Q)$ ), let $(Q, D, (E_{n}))$ be a sweetness model, and let $(A_{j})_{j < ω}$ be subsets of $P$ whose union is dense in $P$ . Write $e : Q \to B ∖ {0_{B}}$ for the canonical dense completion map, and use Shelah's quotient convention

$p ⊩_{P} q \in Q / P ⟺ every p_{0} \in P with p_{0} \leq p is compatible in B with e (q) .$

Suppose $q \in D$ and $p \in P$ forces $q \in Q / P$ . Then some $j, k < ω$ have the following uniform property: for every $q^{'} E_{k} q$ there is $p^{'} \in A_{j}$ with $p^{'} \leq p$ which forces $q^{'} \in Q / P$ . Moreover, the union of all $A_{j}$ for which such a $k$ exists is dense below $p$ . This is the full two-part conclusion of Claim 7.4 of the source, in the library order.

Facts & Assumptions

Given: ZFC and the objects and quotient convention in the Statement.

[F1]

Shelah sweetness models for forcing: $(Q, D, (E_{n}))$ satisfies the sequential clause and the transfer clause, and its $E_{n}$ -classes are downward directed. The same definition says that $P$ is a complete suborder of $B$ when its order and incompatibility are inherited from $B^{+}$ and every maximal antichain of $P$ remains maximal in $B^{+}$ .

[F2]

Choice-free regular open completion of forcing preorders (with forcing equivalence as in Forcing equivalence and Boolean completion) and Completeness, regular opens, and order continuity: the canonical map $e : Q \to B ∖ {0_{B}}$ preserves order, preserves and reflects compatibility, and has order-dense image. It need not be injective or reflect the original order.

[F3]

By the displayed quotient convention, $p ⊩_{P} q \in Q / P$ is monotone in $p$ and upward closed in $q$ : if $p^{'} \leq p$ and $q^{'} \leq q$ , then $p ⊩_{P} q^{'} \in Q / P$ implies $p^{'} ⊩_{P} q \in Q / P$ .

[F4]

The Axiom of Choice supplies choices from nonempty witness sets. Under this assumption Zorn's lemma gives a maximal element of any nonempty poset in which every chain has an upper bound.

[F5]

$N \times N \approx N$ gives the unique decomposition of every positive natural into $2^{m} (2 r + 1)$ . Thus define $n (i) = m$ from $i + 1 = 2^{m} (2 r + 1)$ for every $i \in N$ .

Proof

1.1

Fix the canonical surjection $n (i) = m$ where $i + 1 = 2^{m} (2 r + 1)$ , For fixed $m$ , the indices $i = 2^{m} (2 r + 1) - 1$ as $r$ varies are unbounded, so $m$ occurs arbitrarily late; in particular $n (0) = 0$ .

1.2

The Boolean conditions $p$ and $e (q)$ are compatible in $B$ : the quotient hypothesis applied to $p_{0} = p$ says exactly that they are compatible.

2.1

For each $i < ω$ , use [F4] to choose $q_{i} \in D$ with $q_{i} E_{i} q$ so that, whenever there exists $q^{'} E_{i} q$ for which no $p^{'} \in A_{n (i)}$ satisfies $p^{'} \leq p$ and $p^{'} ⊩ q^{'} \in Q / P$ , the chosen $q_{i}$ has that property. The admissible set is nonempty: choose a bad witness if one exists, and otherwise use $q$ itself.

F1F4step 1.1

2.2

There is $r \in D$ with $r \leq q$ and $e (r) \leq p$ . Indeed step 1.2 gives a nonzero $b \leq p \land e (q)$ in $B$ . Density of $e [Q]$ supplies $s \in Q$ with $e (s) \leq b$ . Then $e (s)$ and $e (q)$ are compatible, so compatibility reflection in [F2] supplies a common strengthening $t \leq s, q$ in $Q$ . Finally density of $D$ supplies $r \in D$ with $r \leq t$ . Order preservation gives $e (r) \leq e (s) \leq p$ , while $r \leq q$ .

F1F2step 1.2

3.1

There is $k < ω$ such that every $q^{'} E_{k} q$ has $e (q^{'})$ compatible with $p$ . Apply the comparable form of the transfer clause to $r \leq q$ at $n = 0$ . It supplies $k$ such that every $q^{'} E_{k} q$ has some $r^{'} E_{0} r$ with $r^{'} \leq r, q^{'}$ . Hence $e (r^{'}) \leq e (r) \leq p$ and $e (r^{'}) \leq e (q^{'})$ , so $e (r^{'})$ witnesses the required Boolean compatibility.

F1F2step 2.2

3.2

The sequence $(q_{i})$ extends to the diagonal witness: since $q_{i} E_{i} q$ and $E_{i}$ refines $E_{k}$ for all $i \geq k$ , the sequential clause applied to the sequence with last term $q$ gives $q^{*} \in D$ with $q^{*} E_{k} q$ and $q^{*} \leq q_{i}$ for every $i \geq k$ .

F1step 2.1

4.1

Since $q^{*} E_{k} q$ , step 3.1 makes $e (q^{*})$ compatible with $p$ . We claim that some $p^{''} \leq p$ in $P$ forces $q^{*} \in Q / P$ . Otherwise the quotient convention makes $C = {s \in P : s \leq p and s ⊥_{B} e (q^{*})}$ dense below $p$ in $P$ . Apply [F4] to the poset of antichains contained in $C$ , ordered by inclusion: the empty antichain is present and unions bound chains because any two elements of a chain union occur together in one antichain. Obtain a maximal such $A$ . It is predense below $p$ : otherwise a condition below $p$ incompatible with all of $A$ has a strengthening in $C$ that could be added. Apply the same argument to antichains of $P$ containing $A$ to obtain a maximal antichain $M$ of $P$ . Every member of $M ∖ A$ is incompatible with $p$ : if such an $m$ were compatible with $p$ , a common strengthening in $P$ would be compatible with some member of the predense antichain $A$ below $p$ , contradicting that $M$ is an antichain. By completeness of the suborder [F1], $M$ is maximal in $B$ . But a common Boolean strengthening of $p$ and $e (q^{*})$ is incompatible with every member of $A$ (by the definition of $C$ ) and every member of $M ∖ A$ (because they are incompatible with $p$ ), contradicting maximality in $B$ . This proves the claim. Now choose $p^{'} \in A_{j}$ below $p^{''}$ from the dense union of the $A_{j}$ . Then $p^{'} \leq p$ and $p^{'} ⊩ q^{*} \in Q / P$ ; by upward closure in [F3], it also forces every $q^{'} \in Q$ with $q^{*} \leq q^{'}$ into the quotient.

F1F3F4step 3.1step 3.2

5.1

Choose $i \geq k$ with $n (i) = j$ , possible by step 1.1. Then $p^{'} \in A_{n (i)}$ satisfies $p^{'} \leq p$ and, since $q^{*} \leq q_{i}$ , forces $q_{i} \in Q / P$ ; so $q_{i}$ is not bad at level $i$ . By step 2.1 the existence of a bad witness at level $i$ would have forced $q_{i}$ to be bad, hence no $q^{'} E_{i} q$ is bad for $A_{n (i)}$ : for every $q^{'} E_{i} q$ there is $p^{'} \in A_{j}$ with $p^{'} \leq p$ and $p^{'} ⊩ q^{'} \in Q / P$ . Thus the pair $(A_{j}, i)$ has the uniform property required in part (1) of the Statement.

step 1.1step 2.1step 4.1

6.1

Let $A^{*} = ⋃ {A_{j} : for some k, A_{j} has the uniform property for k}$ . Given $p_{0} \leq p$ , the hypothesis $p_{0} ⊩ q \in Q / P$ holds by monotonicity [F3], so the argument of steps 1.2 through 5.1 with $p_{0}$ in place of $p$ produces $j, k$ such that every $q^{'} E_{k} q$ , in particular $q^{'} = q$ , has a condition $p^{'} \in A_{j}$ below $p_{0}$ forcing $q^{'} \in Q / P$ ; The uniform property below $p_{0}$ implies the one below $p$ since every witness below $p_{0}$ is below $p$ , so this $A_{j}$ is included in $A^{*}$ . Hence $A^{*}$ meets every strengthening of $p$ and is dense below $p$ .

F3step 5.1

7.1

The steps above establish both conclusions of the Statement.

step 5.1step 6.1∎

TheoremStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Shelah amalgamation preserves sweetness

Statement

Let $Q_{1}$ and $Q_{2}$ be sweet forcings and let $P_{0}$ be completely embedded in $B A (Q_{1})$ and in $B A (Q_{2})$ . Their Boolean amalgam $Q_{1} *_{P_{0}} Q_{2}$ is sweet and contains complete canonical copies of $Q_{1}$ and $Q_{2}$ . If the sweetness model on $Q_{2}$ extends a fixed model on $Q_{1}$ in the sense of the extension clauses, the amalgam can be equipped with a sweetness model extending that fixed model. The formulation also permits two named complete embeddings of $P_{0}$ , by identifying their images before taking the amalgam.

Facts & Assumptions

Given: Work in ZFC. Let $(Q_{ℓ}, D_{ℓ}, (E_{n}^{ℓ})_{n < ω})$ , $ℓ = 1, 2$ , be sweetness models, and let $i_{ℓ} : P_{0} \to B A (Q_{ℓ})^{+}$ be named complete embeddings. Identify the two images of $P_{0}$ . A pair $(q_{1}, q_{2}) \in Q_{1} \times Q_{2}$ is admitted when some $p_{0} \in P_{0}$ satisfies $p_{0} ⊩ q_{ℓ} \in Q_{ℓ} / P_{0}$ for both $ℓ = 1, 2$ ; write $O = Q_{1} *_{P_{0}} Q_{2}$ for the admitted pairs with the coordinatewise order. This is the source's Definition 7.1, so admission is an intrinsic existential property of the pair, not extra witness data carried by a condition.

[F1]

Shelah sweetness models for forcing: both $(Q_{ℓ}, D_{ℓ}, (E_{n}^{ℓ}))$ satisfy the sequential and transfer clauses with downward directed classes, and the extension relation between sweetness models is the five-clause relation of the Definition.

[F2]

Sweet forcings are countable unions of directed sets and ccc: a sweet forcing itself is a countable union of directed sets and is ccc.

[F3]

Shelah, Claim 7.3(1): if $P < B A (Q)$ and $Q$ is sweet, then $P$ is a countable union of directed subsets. Applied to $P_{0} < B A (Q_{1})$ , this supplies $(A_{j})_{j < ω}$ with $P_{0} = ⋃_{j} A_{j}$ and every $A_{j}$ directed. Definition 7.1 also states the standard amalgam facts: $O$ is forcing-equivalent to $P_{0} * (Q_{1} / P_{0} \times Q_{2} / P_{0})$ and the maps $q_{1} \mapsto (q_{1}, 1_{Q_{2}})$ and $q_{2} \mapsto (1_{Q_{1}}, q_{2})$ are complete embeddings. The weak-coordinate symbols are the distinguished weakest conditions from [F1].

[F4]

Sweet density transfers along complete suborders: the two-part uniform conclusion of the corresponding source claim, in the form that for a condition $q \in D_{ℓ}$ and $p_{0} ⊩ q \in Q_{ℓ} / P_{0}$ there are $j$ and $k$ such that every $q^{'} E_{k}^{ℓ} q$ has some $p_{0}^{'} \in A_{j}$ with $p_{0}^{'} \leq p_{0}$ and $p_{0}^{'} ⊩ q^{'} \in Q_{ℓ} / P_{0}$ , and the union of those $A_{j}$ having this property is dense below $p_{0}$ .

[F5]

The Axiom of Choice: the ambient ZFC assumption permits the witness choices used in Claims 7.3 and 7.4.

[F6]

Shelah's Lemma 7.5 proves the sweetness construction from the displayed least modulus, and Claim 7.12 proves the fixed-model extension construction. Both are cited in the source locator above. [source]

Proof

1.1

Put $D = {(q_{1}, q_{2}) \in O : q_{1} \in D_{1} and q_{2} \in D_{2}} .$ The source amalgamation lemma recorded in [F6] first proves that $D$ is dense. Its proof keeps the admission witness until after both coordinates have been strengthened: below a witness $p_{0}$ , apply the dense conclusion of [F4] to the first coordinate; reindex the resulting subfamily of the directed cover $(A_{j})$ , whose union remains dense below $p_{0}$ ; then apply [F4] to the second coordinate. Directedness inside one $A_{j}$ produces a common strengthening of the two quotient witnesses. Thus the result is still an admitted pair, rather than merely two independently dense coordinates.

F3F4F5F6

1.2

The same two applications prove the intrinsic assertion

$(*)_{x} \exists m < ω \forall q_{1}^{'} E_{m}^{1} q_{1} \forall q_{2}^{'} E_{m}^{2} q_{2} (q_{1}^{'}, q_{2}^{'}) \in O$

for every $x = (q_{1}, q_{2}) \in D$ . Define $m (x)$ to be the least such $m$ . No chosen witness, index $j$ , or reduction is part of $m (x)$ . If $q_{ℓ}^{'} E_{m (x)}^{ℓ} q_{ℓ}$ for both coordinates and $x^{'} = (q_{1}^{'}, q_{2}^{'}) \in D$ , then the $E_{m (x)}^{ℓ}$ -classes of the old and new coordinates coincide, so $(*)_{x^{'}}$ holds at $m (x)$ . Conversely, if it held at some $r < m (x)$ for $x^{'}$ , refinement gives $q_{ℓ}^{'} E_{r}^{ℓ} q_{ℓ}$ , hence the two $E_{r}^{ℓ}$ -classes coincide and it would hold for $x$ , contradicting minimality. Therefore

$(* *)_{x} m (x^{'}) = m (x) .$

This is exactly the least-modulus convention and the displayed observation in the source amalgamation lemma [F6]. [F1, F3, F4, F5, F6]

2.1

On $D$ define $x E_{n} x^{'} ⟺ m (x) = m (x^{'}) = : m and q_{ℓ} E_{m + n}^{ℓ} q_{ℓ}^{'} (ℓ = 1, 2) .$ The relation is intrinsic because $m$ is intrinsic. The observation $(* *)$ gives reflexivity and makes the common- $m$ condition stable under the coordinate equivalences; symmetry and transitivity then follow from the old relations. Refinement is immediate. An $E_{n}$ -class is encoded by $m$ and one $E_{m + n}^{1}$ -class and one $E_{m + n}^{2}$ -class, so there are countably many classes.

F1step 1.2

3.1

The remaining sweetness checks are those of the source amalgamation lemma [F6] with precisely this definition. For directedness, take coordinatewise common lower bounds inside the two $E_{m + n}^{ℓ}$ -classes; since they still lie in the corresponding $E_{m}^{ℓ}$ -classes, $(*)_{x}$ admits the resulting pair, and $(* *)_{x}$ keeps its modulus equal to $m$ . For a diagonal sequence, apply the sequential clause in each coordinate; the tail bounds lie in the required $E_{m + n}^{ℓ}$ -classes, so the same $(*), (* *)$ argument makes them admitted $E_{n}$ -bounds. For transfer, use the two coordinate transfer moduli and then the common-admission conclusion obtained in step 1.1 from [F4]; $(* *)$ again keeps the output in the prescribed amalgam class. These checks prove the directed, sequential and transfer clauses without selecting a witness as part of a condition. Thus $(O, D, (E_{n}))$ is a sweetness model.

F1F4F6step 1.1step 1.2step 2.1

4.1

By the standard amalgam facts recorded in [F3], the weak-coordinate maps $q_{1} \mapsto (q_{1}, 1_{Q_{2}})$ and $q_{2} \mapsto (1_{Q_{1}}, q_{2})$ are complete embeddings into $O$ . This conclusion is about the canonical copies in the full amalgam; it does not require those copies to lie in the particular dense presentation $D$ . Sweetness also implies ccc by [F2].

F2F3step 3.1

4.2

Now suppose $(Q_{1}, D_{1}, (E_{n}^{1})) < (Q_{2}, D_{2}, (E_{n}^{2}))$ in the exact five-clause sense of [F1]. The fixed-model source result [F6] applies to the same named embeddings and the preceding amalgam. It first replaces the initial dense presentation by an equivalent dense-open presentation $D^{*}$ separated from the canonical old dense set, then sets $D^{'} = D^{*} \cup D_{1}$ . On $D^{*}$ it uses the new relations and on $D_{1}$ it uses exactly the old $E_{n}^{1}$ ; there are no cross-piece classes. The mixed case of the transfer clause is checked by the comparable transfer form in [F1], as in the source's preceding fixed-model argument. The source result then verifies: the canonical $Q_{1}$ is a complete suborder, $D_{1} \subseteq D^{'}$ , the old relations are the restrictions, every new class meeting $D_{1}$ remains in $Q_{1}$ , and if an old condition strengthens a member of $D^{'}$ , that member already lies in $D_{1}$ . Hence this is a sweetness model on $O$ extending the fixed model on $Q_{1}$ .

F1F6step 3.1

5.1

Steps 3.1--4.2 prove every assertion in the Statement, including the named canonical-copy and fixed-model interfaces.

step 3.1step 4.1step 4.2∎

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-09-22Open item page →

Shelah's universal-meagre forcing

Definition

Work in ZF with the usual cylinder topology on Cantor space $2^{ω}$ . For a finite word $s$ , its cylinder consists of all infinite binary extensions of $s$ . The universal-meagre forcing $U M$ has a distinguished weakest condition $1_{U M}$ and the following nontrivial conditions. A nontrivial condition is a pair $(t, T)$ where $T \subseteq 2^{< ω}$ is a nonempty subtree in the sense of Trees and their bodies that is perfect — every node of $T$ has two incomparable extensions in $T$ — and whose body $[T]$ is nowhere dense in the sense of Nowhere dense, meagre, residual, and comeagre subsets of a topological space; and $t = T \cap 2^{\leq n}$ is its finite initial tree through some height $n < ω$ . Because $T$ is nonempty, downward closed and perfect, it contains the empty node and has a node at every level. Thus $n$ is recovered from $t$ as $ht (t) : = \max {∣ s ∣ : s \in t}$ ; this is the meaning of the height of a recorded tree below. In the library order of Forcing preorders, compatibility and filters, Dense open sets and generic filters over a model, every condition is below $1_{U M}$ , and the order between nontrivial conditions is

$(t_{2}, T_{2}) \leq (t_{1}, T_{1}) ⟺ T_{1} \subseteq T_{2} and t_{1} = t_{2} \cap 2^{\leq ht (t_{1})} .$

The symbol $1_{U M}$ is not represented by an empty tree. This is the separately adjoined weak condition used for zero coordinates in Shelah's canonical embeddings; excluding an empty recorded tree prevents the vacuous ``perfectness'' convention from creating a second, absorbing condition.

Thus a stronger condition enlarges the witness tree while permanently preserving the recorded finite initial tree. A condition is determined by its witness tree and its height; the recorded tree is a sub-tree of every witness tree extending it, so the extension relation is reflexive and transitive. $U M$ is nonempty: the perfect tree $T_{0} = {σ \in 2^{< ω} : σ$ contains no two consecutive $1$ s $}$ is nowhere dense, because every cylinder contains a string with two consecutive $1$ s and hence no cylinder is contained in $[T_{0}]$ .

Basic properties used below. Let $(t_{1}, T_{1})$ , $(t_{2}, T_{2})$ be nontrivial conditions with $ht (t_{1}) \leq ht (t_{2})$ . A common strengthening $(\tilde{t}, \tilde{T})$ satisfies $\tilde{T} \supseteq T_{1} \cup T_{2}$ and $\tilde{t} \cap 2^{\leq ht (t_{1})} = t_{1}$ , $\tilde{t} \cap 2^{\leq ht (t_{2})} = t_{2}$ ; hence two conditions are necessary for compatibility: $t_{1} = t_{2} \cap 2^{\leq ht (t_{1})}$ , and every node of $T_{1}$ of height at most $ht (t_{2})$ belongs to $t_{2}$ . These two conditions are also sufficient: if $T : = T_{1} \cup T_{2}$ , then $T$ is a subtree, it is perfect because every node of $T$ splits inside whichever of $T_{1}, T_{2}$ contains it, its body $[T] = [T_{1}] \cup [T_{2}]$ is nowhere dense as a finite union of closed nowhere-dense sets, and $T \cap 2^{\leq ht (t_{2})} = t_{2}$ , so $(t_{2}, T)$ is a common strengthening of $(t_{1}, T_{1})$ and $(t_{2}, T_{2})$ . The first condition alone is not sufficient: for $T_{1}$ the tree of strings with no two consecutive $0$ s and $T_{2}$ the tree of strings with no two consecutive $1$ s one has $ht (t_{1}) = 1$ , $ht (t_{2}) = 2$ , $t_{1} = t_{2} \cap 2^{\leq 1} = {\emptyset, 0, 1}$ , yet $11 \in T_{1} \cap 2^{\leq 2}$ while $11 \notin t_{2}$ , so the two conditions have no common strengthening. In particular the conditions carrying one fixed recorded tree $t$ are pairwise compatible: their witness trees agree on $2^{\leq ht (t)}$ , so their union is again a witness tree, it is perfect because every node splits inside one of the two trees, it is nowhere dense as a finite union of closed nowhere-dense sets, and its initial tree through height $ht (t)$ is $t$ . Two conditions whose recorded trees disagree on the levels common to both heights are incomparable, since a common strengthening would have to record both trees below the shorter height; distinct perfect nowhere-dense trees can disagree on such a level, so compatibility of $U M$ is not automatic. For a condition $(t, T)$ and a node $σ \in T$ , the conditions below $(t, T)$ whose recorded tree contains $σ$ are dense in the cone below $(t, T)$ , because one extends the height past $∣ σ ∣$ . They need not be dense in all of $U M$ , since conditions incompatible with $(t, T)$ have no such extension. For the generic-object assertion, compute $U M$ in a transitive ZF ground model $M$ and let $G$ be an $M$ -generic filter as in Dense open sets and generic filters over a model. A set $D \in M$ dense below $p \in G$ is met by $G$ : adjoining all conditions incompatible with $p$ makes it dense in the whole forcing, and directedness excludes those incompatible conditions from $G$ . Consequently, every witness tree of a nontrivial condition in $G$ is contained in the generic tree

$U_{G} = ⋃ {t : some (t, T) \in G} = ⋃ {T : (t, T) \in G},$

This union is nonempty because nontrivial conditions are dense. It is a tree, and each of its nodes lies in a witness tree contained in the union; that witness supplies two incomparable extensions, proving perfection. Its body is closed: a real outside the body has a finite prefix absent from the tree and the corresponding cylinder misses the body.

Nowhere density needs a separate dense-set argument. Given any finite word $s$ and nontrivial condition $(t, T)$ , the closed nowhere-dense body $[T]$ has a cylinder $[v] \subseteq [s]$ disjoint from it. Here $v \notin T$ : every node of the pruned binary tree $T$ lies on a branch, obtained by recursively taking the least available child. Increase the recorded height to at least $∣ v ∣$ , keeping $T$ unchanged. All stronger conditions now omit $v$ from their witness trees. Thus the conditions recording such a missing extension of $s$ form a ground-model dense set (also below $1_{U M}$ ). Genericity meets it, and filter directedness ensures that $v$ belongs to no witness tree from $G$ . Every cylinder therefore contains a cylinder disjoint from $[U_{G}]$ , proving that $[U_{G}]$ is nowhere dense. These arguments use finite binary recursion, not a choice principle.

The finite-prefix rearrangements are precisely the maps $π_{ρ} (s ⌢ x) = ρ (s) ⌢ x$ , for $s \in 2^{n}$ , $x \in 2^{ω}$ , and a permutation $ρ$ of the finite set $2^{n}$ , for some $n < ω$ . Each map is a homeomorphism preserving the tail after coordinate $n$ . There are countably many such maps, since these permutations have finite codes. A partial bijection on $2^{n}$ extends to one by matching unused domain and range words in lexicographic order; it is this full permutation, not an arbitrary homeomorphic extension, that defines the rearrangement.

The forcing is ccc, since it is the union of countably many directed sets: the singleton ${1_{U M}}$ is one such set, and for each finite tree $t$ the class of conditions of $U M$ carrying the recorded tree $t$ is directed by the paragraph above, and there are only countably many finite trees $t$ . Hence $U M$ is a countable union of directed sets, and an antichain meets each directed class in at most one element because any two members of one class are compatible. Assigning each antichain member the least code of a class containing it gives an injection into $ω$ , including for the empty antichain. This proves ccc without choice.

Remarks

The point of the forcing is not that the generic tree contains an arbitrary old nowhere-dense tree: the old sets are absorbed at the next stage, by the countable union of finite-prefix rearrangements of $[U_{G}]$ constructed in A universal-meagre generic absorbs old nowhere-dense sets, and the assertion $[S] \subseteq [U_{G}]$ for an arbitrary old tree $S$ is never used.

LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

A universal-meagre generic absorbs old nowhere-dense sets

Statement

Forcing with $U M$ makes the union of all ground-model closed nowhere-dense subsets of Cantor space meagre. Therefore every ground-model meagre set is contained in one meagre set coded by the $U M$ generic. The meagre envelope is a countable union of finite-prefix rearrangements of $[U_{G}]$ , not $[U_{G}]$ alone.

Facts & Assumptions

Given: A transitive ZF ground model $M$ containing the data and an $M$ -generic filter $G \subseteq U M$ with generic tree $U_{G}$ .

[F1]

Shelah's universal-meagre forcing: conditions, order, the generic tree $U_{G}$ , the countable family of finite-prefix rearrangements, and the fact that each witness tree of a condition in $G$ is contained in $U_{G}$ .

[F2]

Trees and their bodies with Nowhere dense, meagre, residual, and comeagre subsets of a topological space: $[T]$ is closed for every tree, a closed set $C$ has prefix tree $S_{C} = {s : C \cap [s] \neq \emptyset}$ and equals $[S_{C}]$ , since a point outside $C$ has a cylinder disjoint from $C$ . This tree need not be perfect. A homeomorphism carries closed nowhere-dense sets to closed nowhere-dense sets.

[F3]

The meagre subsets of a topological space form a sigma-ideal supplies subset closure. A displayed sequence of closed nowhere-dense sets has meagre union directly by Nowhere dense, meagre, residual, and comeagre subsets of a topological space; replacing each term of one given nowhere-dense cover by its closure gives a closed nowhere-dense cover. We do not use the supplier's Countable Choice clause for selecting covers of countably many unrelated meagre sets.

[F4]

Forcing theorem: truth and definability of forcing, so that dense-below arguments and the forcing relation certify statements about the extension.

Proof

1.1

Fix in $M$ a canonical enumeration $(π_{m})_{m < ω}$ of the finite-prefix rearrangements of $2^{ω}$ : each is determined by a finite partial bijection between level- $n$ cylinders for some $n$ , and there are only countably many such finite data, so the enumeration is definable without choice.

1.2

Perfect enlargement: let $C$ be any old nonempty closed nowhere-dense set. For every finite binary word $s$ with $C \cap [s] \neq \emptyset$ , choose the first finite extension $t_{s}$ of $s$ , in length-lexicographic order, for which $[t_{s}] \cap C = \emptyset$ . Such an extension exists by nowhere density. Put $K_{s} = {t_{s} ⌢ y : (\forall j) y (2 j) = 0}$ . This set is nonempty, closed, has no isolated points because arbitrarily late odd coordinates are free, and is nowhere dense because an arbitrarily late even coordinate can be set to $1$ . Define $K = C \cup ⋃_{s} K_{s}$ . These are prescribed least choices and a set union, available in $M$ without Choice.

1.3

Grafting step: let $S$ be an old perfect nowhere-dense tree and let $(t, T)$ be a nontrivial condition. Below $1_{U M}$ , first take the explicit nontrivial condition supplied by F1. Choose any $n > ht (t)$ and any $η \in T \cap 2^{n}$ ; perfection of $T$ guarantees such a node. Enumerate the finite nonempty level $S \cap 2^{n}$ as ${s_{1}, \dots, s_{k}}$ . For each $i \leq k$ , put $C_{i} = {η ⌢ τ : s_{i} ⌢ τ \in S}$ , including all initial segments, and put $T^{''} = T \cup ⋃_{i \leq k} C_{i}$ . Thus all the level- $n$ sections of $S$ are grafted below the same node $η$ ; no comparison between the widths of $S$ and $T$ is needed. Every newly added node not already in $T$ has length greater than $n$ , so $T^{''} \cap 2^{\leq n} = T \cap 2^{\leq n}$ and in particular $T^{''} \cap 2^{\leq ht (t)} = t$ . Moreover $T \subseteq T^{''}$ , and $T^{''}$ is perfect: nodes of $T$ keep their splitting extensions, while every node added from $C_{i}$ inherits splitting extensions from the section of the perfect tree $S$ below $s_{i}$ . Hence $(t, T^{''}) \leq (t, T)$ provided its body is nowhere dense, as checked below.

F1F2

1.4

For completeness, $[U_{G}]$ is nowhere dense for an explicit dense-set reason. Given a word $s$ and a nontrivial condition $(t, T)$ , choose an extension $v$ of $s$ with $[v] \cap [T] = \emptyset$ . Since $T$ is pruned binary, any node of $T$ has a branch by recursively taking the least available child; hence $v \notin T$ . Increase the recorded height to at least $∣ v ∣$ . Every stronger condition omits $v$ permanently. These conditions are dense for each $s$ , including below the weakest condition. The generic meets all these ground dense sets, so every cylinder has a subcylinder disjoint from $[U_{G}]$ . The body is closed by F2, as required.

F1F2F4

2.1

If a cylinder $[u]$ misses $C$ , it meets no $K_{s}$ with $∣ s ∣ \geq ∣ u ∣$ : intersecting cylinders would give $[s] \subseteq [u]$ , contrary to $[s] \cap C \neq \emptyset$ . It therefore meets only the finitely many $K_{s}$ indexed by shorter words. For any point outside $K$ , first take such a cylinder around it and then avoid those finitely many closed sets, proving $K$ closed. Inside any cylinder first find a subcylinder missing $C$ , then successively avoid the finitely many closed nowhere-dense $K_{s}$ meeting it; thus $K$ is nowhere dense. Every cylinder about a point of $C$ contains its corresponding nonempty $K_{s}$ , disjoint from $C$ , so no point of $C$ is isolated in $K$ ; points of the $K_{s}$ are not isolated either. Its prefix tree $S$ is consequently nonempty and perfect: any node meeting $K$ has two distinct extensions witnessed by two points of $K$ in its cylinder. F2 gives $[S] = K \supseteq C$ . For $C = \emptyset$ , absorption is immediate and no enlargement is needed. Inclusion of the old prefix tree in $S$ implies inclusion of their bodies even for new branches in an extension.

F2step 1.2

2.2

The body of $T^{''}$ is $[T^{''}] = [T] \cup ⋃_{i \leq k} γ_{i} ([S] \cap [s_{i}])$ , where $γ_{i} (s_{i} ⌢ y) = η ⌢ y$ . Each displayed image is closed and has empty interior relative to the clopen cylinder $[η]$ , hence is closed nowhere dense in $2^{ω}$ . The union is finite, so together with the closed nowhere-dense set $[T]$ it is again closed nowhere dense. Thus $T^{''}$ is a legitimate witness tree and $(t, T^{''})$ is a condition below $(t, T)$ .

F2step 1.3

3.1

Absorption below the condition: for each $i \leq k$ , choose a permutation of $2^{n}$ sending $η$ to $s_{i}$ , and let $π_{i}$ be its induced finite-prefix rearrangement, which keeps the tail after the length- $n$ prefix unchanged. If $x \in [S]$ , then uniquely $x = s_{i} ⌢ y$ for some $i$ , while $η ⌢ y \in [T^{''}]$ by construction and $π_{i} (η ⌢ y) = s_{i} ⌢ y = x$ . Any generic filter containing $(t, T^{''})$ has $[T^{''}] \subseteq [U_{G}]$ by [F1]. Consequently $(t, T^{''})$ forces $[S] \subseteq π_{1} ([U_{G}]) \cup \dots \cup π_{k} ([U_{G}])$ . The $π_{i}$ occur in the fixed enumeration from step 1.1.

F1F2step 2.2

4.1

The conditions of the form $(t, T^{''})$ of step 1.3 are dense below every condition: given $(t, T)$ and an old $S$ , the grafting construction produces such a strengthening directly. For a nonempty old closed nowhere-dense set first apply the perfect-enlargement construction above to obtain its perfect enlargement; the empty set is automatic. Hence every condition forces that every old closed nowhere-dense set is contained in a finite subunion of the countable family ${π_{m} ([U_{G}]) : m < ω}$ .

F1F4step 2.1step 3.1

5.1

In the extension, put $E = ⋃_{m < ω} π_{m} ([U_{G}])$ . By step 4.1 and genericity, every old closed nowhere-dense set is contained in $E$ ; each $π_{m} ([U_{G}])$ is closed nowhere dense because a homeomorphism preserves closedness and empty interior, so $E$ is a countable union of closed nowhere-dense sets and is meagre by [F3]. The code of $E$ is the generic tree together with the ground-model enumeration $(π_{m})$ of step 1.1, so $E$ is coded by the $U M$ generic.

F2F3F4step 4.1step 1.4

6.1

Let $A \in M$ be meagre. By [F3] there are old closed nowhere-dense sets $[S_{n}]$ with $A \subseteq ⋃_{n} [S_{n}]$ , and by step 5.1 the union $⋃_{n} [S_{n}]$ is contained in $E$ . Hence $A \subseteq E$ : every old meagre set is contained in one meagre set coded by the generic.

F3step 5.1

7.1

The steps above establish both assertions of the Statement: the union of all old closed nowhere-dense sets is meagre, and every old meagre set is absorbed into the single coded meagre envelope $E$ .

step 5.1step 6.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

Composition with universal-meagre forcing preserves sweetness

Statement

Assume ZFC. If $P$ has a sweetness model and $P$ forces that $Q$ is $U M$ , then the two-step iteration $P * Q$ has a sweetness model extending that of $P$ . This remains true in the strengthened extension-of-models form used at successor stages.

Facts & Assumptions

Given: Work in ZFC. A sweetness model $(P, D, E_{n}^{P})$ and the canonical two-step iteration $P * \dot{U M}$ of Two-step forcing iterations, where $P$ forces that the second coordinate is the forcing defined in Shelah's universal-meagre forcing. Equivalently, a specified $P$ -forced order isomorphism with that canonical forcing may be used to rename the second-coordinate conditions. Mere forcing equivalence, without such an order isomorphism carrying the conditions and traces below, is not used.

[F1]

Shelah sweetness models for forcing: the sequential and transfer clauses of $(P, D, E_{n})$ and the extension relation between sweetness models.

[F2]

Shelah's universal-meagre forcing: $U M$ and its order; the union $T_{1} \cup T_{2}$ of two conditions' witness trees with a common initial tree is again a perfect nowhere-dense tree with that initial tree.

[F3]

By the transfer clause in [F1], if $A_{m} = q_{m} / E_{j}^{P}$ is an old equivalence class and $p \in D$ , there is $k$ such that every $p^{'} E_{k}^{P} p$ has a member of $A_{m}$ below it whenever $p$ does. This is an application of the old sweetness model itself, not of a complete-suborder density theorem.

[F4]

Forcing theorem: definability and truth for forcing, used for the node-membership traces and the conditional tree names in the proof.

[A1]

The Axiom of Choice licenses the enumeration of the old class families, all countable dependent witness selections below, and—crucially—the maximal-antichain mixing that replaces every local second-coordinate name by a name in the set $R$ fixed by Two-step forcing iterations. This is the exact additional hypothesis needed to transport Shelah's local-name proof to that restricted set-sized carrier.

[F5]

Shelah's Composition Lemma 7.6 defines the relations by clauses $(α)$ -- $(ε)$ and proves all sweetness clauses; Subclaim 7.8 is the strengthening lemma used in their proof. Claim 7.11 then adjoins the old dense presentation and proves the extension-of-models form. [source]

Proof

1.1

Enumerate, with repetitions allowed, all old equivalence classes as ${A_{m} : m < ω}$ . For $p \in D$ define $k_{m} (p)$ to be the least $k$ such that every $p^{'} E_{k}^{P} p$ has the following property: $A_{m} \cap (P ↓ p) \neq \emptyset ⟹ A_{m} \cap (P ↓ p^{'}) \neq \emptyset .$ If the left side is empty this is vacuous. Otherwise, writing $A_{m}$ as an old equivalence class, the transfer clause gives such a $k$ . This is the source's clause $(ε)$ modulus.

F1F3A1

1.2

Shelah's source works with local conditions $(p, (t, \dot{T}))$ satisfying only $p ⊩ (t, \dot{T}) \in U M$ . Strengthen any iteration condition to decide the finite record $t$ , make the second coordinate nontrivial, and put the first coordinate in $D$ . By [A1] and the normalization theorem in Two-step forcing iterations, replace the resulting local second-coordinate name by a name in its set $R$ that is forced equal below $p$ . Do this after every later conditional union as well, always below the constructed first coordinate. Substitution for forced equality shows that these normalized representatives have exactly the local order comparisons used in the source, so they form a dense presentation $D^{*}$ of the restricted iteration. In particular, no name is required to be a UM condition under $1_{P}$ . For $x_{j} = (p_{j}, (t_{j}, {\dot{T}}_{j}))$ , $j = 1, 2$ , define $x_{1} E_{n}^{*} x_{2}$ by the following five clauses from the source composition result [F5]:

$(α)$ $p_{1} E_{n}^{P} p_{2}$ ;
$(β)$ $t_{1} = t_{2}$ ;
$(γ)$ for every $m < n$ , the cone below $p_{1}$ meets $A_{m}$ iff the cone below $p_{2}$ meets $A_{m}$ ;
$(δ)$ for every $m < n$ , whenever the equivalent cone-meeting condition in $(γ)$ holds for $A_{m}$ , then for every $η \in 2^{n}$ , $\exists q \in A_{m} (q ⊩ η \notin {\dot{T}}_{1}) ⟺ \exists q \in A_{m} (q ⊩ η \notin {\dot{T}}_{2});$
$(ε)$ for every $m < n$ , $k_{m} (p_{1}) = k_{m} (p_{2})$ and $p_{1} E_{k_{m} (p_{1})}^{P} p_{2}$ .

The implication in $(δ)$ is deliberately conditional on $(γ)$ , and the tree trace records forced nonmembership. These are the exclusion traces in the source; membership traces cannot replace them. These two finite traces and the strengthening moduli are the interfaces needed in the diagonal proof. The normalization changes no trace used by the proof: when $(γ)$ is active, directedness of $A_{m}$ combines any trace witness with a member below $p_{j}$ , where the original and normalized names are forced equal. [F4, F5, A1, step 1.1]

2.1

The five clauses define refining equivalence relations with countably many classes. At a fixed $n$ they record an old $E_{n}^{P}$ -class, one finite tree, finitely many cone-meeting bits, finitely many nonmembership bits on $2^{n}$ , and finitely many natural-number moduli and old classes. Transitivity of $(δ)$ uses $(γ)$ to ensure that the same active $A_{m}$ is being compared; transitivity of $(ε)$ uses directedness of $A_{m}$ together with the definition of $k_{m}$ . For refinement, exclusion of a length- $n$ word from a pruned binary tree is equivalent to exclusion of both its children. If separate members of an active directed $A_{m}$ force the two exclusions, a common strengthening inside $A_{m}$ forces both. Thus equality of the length- $(n + 1)$ exclusion traces implies equality at length $n$ ; all other recorded data restrict directly.

F1F5step 1.2

2.2

The stability subclaim recorded in [F5] is the fixed-model strengthening interface used repeatedly below. Put $K = \max ({n} \cup {k_{m} (p) : m < n})$ . If $p^{'} E_{K}^{P} p$ and $p^{'} \leq p$ , then for every canonical UM condition $(p, (t, \dot{T})) \in D^{*}$ one has $(p^{'}, (t, \dot{T})) \in D^{*}$ and $(p^{'}, (t, \dot{T})) E_{n}^{*} (p, (t, \dot{T}))$ ; moreover the cone below $p^{'}$ meets $A_{m}$ iff the cone below $p$ meets $A_{m}$ for every $m < n$ . The forward direction is immediate from $p^{'} \leq p$ , and the reverse direction is exactly the defining property of $k_{m} (p)$ .

F1F5step 1.1step 1.2

3.1

Downward directedness now has a legitimate common condition. For two $E_{n}^{*}$ -equivalent members, use the old directed class at the maximum of $n$ and their finitely many common $k_{m}$ values to obtain $p^{*} \leq p_{1}, p_{2}$ . The stability subclaim [F5] preserves all active $A_{m}$ traces. Clause $(β)$ gives one recorded tree $t$ , while $(δ)$ ensures that the two witness-tree names have compatible finite membership requirements. Their union below $p^{*}$ is a perfect nowhere-dense witness tree with recorded part $t$ , by the exact UM compatibility calculation in [F2]. Normalize this local union name below $p^{*}$ as in step 1.2; the resulting member of $D^{*}$ is a common lower bound in the same $E_{n}^{*}$ -class.

F1F2F5A1step 1.2step 2.2

3.2

For the sequential clause, suppose $x_{i} E_{i}^{*} x_{ω}$ for every $i < ω$ and fix a tail $i \geq n$ . Put $K = \max ({n} \cup {k_{m} (p_{ω}) : m < n})$ . All first coordinates in the tail lie in the $E_{K}^{P}$ -class of $p_{ω}$ by the five clauses. The old sequential clause supplies a bound of the tail from index $K$ in that class; class directedness combines it with the finitely many first coordinates with $n \leq i < K$ . This gives $p^{*} \in D$ below all first coordinates in the tail and in the required old class. All recorded trees equal one finite $t$ . Define the source's local conditional name ${\dot{T}}^{*} = {\begin{cases} ⋃_{n \leq i \leq ω} {\dot{T}}_{i}, & p^{*} \in {\dot{G}}_{P}, \\ {\dot{T}}_{ω}, & p^{*} \notin {\dot{G}}_{P} . \end{cases}$ The finite initial-tree and perfectness clauses are immediate. Nowhere density is not inferred from the finite data. Given a ground node $η$ and a condition below $p^{*}$ , first strengthen it to force some extension $ν \supseteq η$ out of ${\dot{T}}_{ω}$ . For each sufficiently large $i$ , choose the largest old equivalence level $ℓ (i) < i$ represented by a class $A_{m (i)}$ with $m (i) < i$ through that strengthening. The sequence $ℓ (i)$ is nondecreasing and unbounded. Clauses $(γ)$ and $(δ)$ transfer the exclusion of all finitely many length- $i$ extensions of $ν$ to a condition in $A_{m (i)}$ below $p_{i}$ . On each finite block where $ℓ (i)$ is constant, directedness gives one condition in the corresponding old class; the old sequential clause diagonalises those block conditions to one lower bound. Finally finitely many early indices are handled successively using the nowhere density of their individual tree names. The resulting condition forces one extension of $η$ outside every ${\dot{T}}_{i}$ , hence outside ${\dot{T}}^{*}$ . This is the full source diagonal recorded in [F5], and it proves that $(p^{*}, (t, {\dot{T}}^{*}))$ is a local UM condition below the whole tail. Normalize it below $p^{*}$ by step 1.2. Repeating the finite trace argument verifies clauses $(γ)$ and $(δ)$ against $x_{ω}$ , so the normalized bound lies in its $E_{n}^{*}$ -class.

F1F2F4F5A1step 1.2step 2.2

3.3

For transfer, take $(q, (s, \dot{S})) \leq (p, (t, \dot{T}))$ and a target level $n$ . The source proof [F5] first chooses the old transfer modulus for $p, q$ after incorporating the finitely many $k_{m} (q)$ , then enlarges it past the index of the old class containing $q$ and past the height of $s$ . For an $E_{k}^{*}$ -perturbation $(p^{'}, (t, {\dot{T}}^{'}))$ , the old transfer clause produces $p^{*}$ in the required old class below $p^{'}$ and $q$ . The source uses the local conditional name ${\dot{S}}^{*} = {\begin{cases} \dot{S} \cup {\dot{T}}^{'}, & p^{*} \in {\dot{G}}_{P}, \\ \dot{S}, & p^{*} \notin {\dot{G}}_{P} . \end{cases}$ The extra height qualification ensures that every node outside the recorded tree $s$ is tested by the level- $k$ $(δ)$ trace. Together with $(γ)$ , directedness of the active $A_{m}$ , and the stability subclaim [F5], this proves that $(p^{*}, (s, {\dot{S}}^{*}))$ is a local UM condition, lies below both inputs, and is $E_{n}^{*}$ -equivalent to $(q, (s, \dot{S}))$ . Normalize it below $p^{*}$ by step 1.2 to obtain the required restricted-iteration condition. This is the source transfer argument; the qualification cannot be replaced by agreement of initial trees alone.

F1F2F4F5A1step 1.2step 2.2

4.1

Steps 2.1--3.3 prove that $(P * \dot{U M}, D^{*}, (E_{n}^{*}))$ is sweet. They do not yet prove that this presentation extends the fixed old model. The fixed-model result recorded in [F5] supplies that separate step: replace $D^{*}$ by a dense-open presentation disjoint from the canonical old dense set, adjoin the old $D$ , and use $E_{n}^{*}$ on the new piece and $E_{n}^{P}$ on the old piece, with no cross-piece equivalences. The only mixed transfer case is settled using the stability subclaim [F5] and the comparable transfer clause of [F1]. The fixed-model result then checks all five extension conditions, including that a new class meeting $D$ is contained in $P$ and that a member of the new dense set lying above an old condition was already old. Thus the resulting sweetness model extends the given one.

F1F5step 2.2step 3.3

5.1

If the second forcing is presented under a specified $P$ -forced order isomorphism with canonical UM, pull the concrete conditions, nonmembership traces, and the five clauses back along that isomorphism. No inference from bare forcing equivalence to sweetness is made. Steps 3.1--4.1 establish the two conclusions of the Statement.

F4step 1.2step 4.1∎

LemmaStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Continuous countable unions of sweetness models remain sweet

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $(P_{i}, D_{i}, (E_{n}^{i}))_{i < δ}$ be a continuous increasing chain of sweetness models, where $δ$ has countable cofinality and every successor extends its predecessor in the exact sweetness-model sense, and all stages have the same distinguished weakest condition. Then the direct union forcing, dense set, and stabilized equivalence relations form a sweetness model, and every $P_{i}$ is a complete subforcing of the union.

Facts & Assumptions

Given: Countable Choice and a continuous increasing chain of sweetness models with a common distinguished weakest condition $1$ , indexed by an ordinal $δ$ of countable cofinality, with extension relations as in the definition. Increasing means that for every $i \leq j < δ$ , the stage $j$ extends stage $i$ in that relation; the cofinal sequence is fixed from the hypothesis $cf (δ) = ω$ .

[F1]

Shelah sweetness models for forcing: the sweetness clauses, and the five extension clauses, in particular that every new class meeting an old dense set is contained in it and that the old relations are the restrictions of the new ones.

[F2]

Under The Axiom of Countable Choice ( ${A C}_{ω}$ ), a natural-number-indexed union of at most countable sets is at most countable (Countable unions of at most countable sets, assuming ${A C}_{ω}$ ).

Proof

1.1

Fix an increasing cofinal sequence $γ_{0} < γ_{1} < \dots$ in $δ$ and replace the chain by its cofinal subsequence: every stage lies below some $γ_{k}$ , so the union forcing, dense set and relations are unchanged. Put $P = ⋃_{k} P_{γ_{k}}$ , $D = ⋃_{k} D_{γ_{k}}$ and $E_{n} = ⋃_{k} E_{n}^{γ_{k}}$ . The inherited order is reflexive and transitive: each finite collection of conditions and comparisons lies in one later stage. The union is nonempty since each forcing stage is nonempty. Its distinguished condition $1$ is weakest: every $p$ lies in a stage where $p \leq 1$ , and this comparison persists in the union. For $p \in P$ take a stage containing it and a strengthening $d$ in that stage's dense set. Then $d \in D$ and $d \leq p$ , proving $D$ dense in $P$ .

2.1

Every $P_{i}$ is complete in the union. The order on $P_{i}$ is the restriction of the union order by the extension clauses. If two conditions of $P_{i}$ have a common lower bound in the union, that lower bound belongs to some later stage $P_{γ_{k}}$ , and completeness of $P_{i}$ in that stage reflects compatibility back to $P_{i}$ ; thus incompatibility is also the restriction. Finally let $A$ be a maximal antichain of $P_{i}$ and $p \in P$ . Choose a later stage $P_{γ_{k}}$ containing both $P_{i}$ and $p$ . The extension relation makes $A$ maximal in $P_{γ_{k}}$ , so some $a \in A$ is compatible with $p$ there and hence in the union. Thus every maximal antichain of $P_{i}$ remains maximal in $P$ , which is exactly completeness in [F1].

F1step 1.1

2.2

The relations are well defined: $E_{n}^{γ_{k}}$ is the restriction of $E_{n}^{γ_{j}}$ for $j \geq k$ by [F1], so the union relation is an equivalence relation on $D$ extending each stage relation and satisfying $E_{n + 1} \subseteq E_{n}$ .

F1step 1.1

3.1

At most countably many classes. First, for stages $i \leq j$ , if $r \in D_{j} \cap P_{i}$ , density gives $d \in D_{i}$ with $d \leq r$ . The last extension clause implies $r \in D_{i}$ , so $D_{j} \cap P_{i} = D_{i}$ . If $p \in D_{i}$ and $r E_{n}^{j} p$ , the class-containment clause gives $r \in P_{i}$ , and the preceding identity gives $r \in D_{i}$ . Restriction of the relations now gives $r E_{n}^{i} p$ . Consequently the class of $q \in D_{γ_{k}}$ under $E_{n}$ is the union of its classes at the stages, and it equals its $E_{n}^{γ_{k}}$ -class, because every later class meeting $D_{γ_{k}}$ is contained in $D_{γ_{k}}$ and restricts to the old relation. Since every $E_{n}^{γ_{k}}$ has countably many classes and countable choice counts countable unions of countable sets, $E_{n}$ has countably many classes.

F1F2step 2.2

3.2

Downward directedness: if $x_{1}, x_{2}$ lie in one $E_{n}$ -class, take a stage $γ_{k}$ containing both and realizing their relations; the $E_{n}^{γ_{k}}$ -class of $x_{1}$ equals the $E_{n}$ -class, and the stage model is directed, so a common lower bound exists inside that stage class, hence inside the union class.

F1step 2.2

4.1

Sequential clause: let $q_{i} E_{i} q_{ω}$ for $i < ω$ , and choose a stage $P_{γ_{k}}$ containing $q_{ω}$ . By step 3.1, for every $i$ the entire union $E_{i}$ -class of $q_{ω}$ is its old $E_{i}^{γ_{k}}$ -class and is contained in $D_{γ_{k}}$ . Hence every $q_{i}$ already belongs to that one stage and satisfies $q_{i} E_{i}^{γ_{k}} q_{ω}$ there. The sequential clause of the stage model supplies a common lower bound of the whole sequence and, for every $n$ , a common lower bound of the tail in the $E_{n}^{γ_{k}}$ -class of $q_{ω}$ ; these are also valid lower bounds and the same classes in the union.

F1step 3.1

4.2

Transfer clause: given $p, q \in D$ and $n$ , take a stage $γ_{j}$ containing both. The transfer clause of that stage model supplies a modulus $k$ . If $p^{'} E_{k} p$ in the union, step 3.1 puts $p^{'}$ in the same old $E_{k}^{γ_{j}}$ -class, hence in $D_{γ_{j}}$ ; and any assumed witness from the union $E_{n}$ -class of $q$ is likewise already in its old stage class. The stage transfer clause therefore supplies the required witness, which also serves in the union.

F1step 3.1

5.1

Steps 2.1 through 4.2 verify the four sweetness clauses and completeness of the stage embeddings for $(P, D, (E_{n}))$ , which is the assertion of the Statement.

step 4.1step 4.2step 2.1∎

TheoremStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

Sweet amalgamation extends partial Boolean isomorphisms

Statement

Let $B_{0}$ and $B_{1}$ be countably generated complete subalgebras of a sweet complete Boolean algebra $B$ , and let $h : B_{0} \to B_{1}$ be a complete Boolean isomorphism. There is a sweet complete Boolean algebra $B^{*}$ containing $B$ completely in which $h$ extends to an automorphism of $B^{*}$ . The extension may be chosen compatibly with any previously fixed sweetness-model embedding.

Facts & Assumptions

Given: A sweetness model on $B$ , complete subalgebras $B_{0}, B_{1} \leq B$ generated by countable sets of generators, and a complete Boolean isomorphism $h : B_{0} \to B_{1}$ .

[F1]

Shelah amalgamation preserves sweetness: the amalgam uses two named complete embeddings of the common algebra, is sweet, and contains complete canonical copies of both factors. The named-embedding interface, rather than an untwisted amalgam of two inclusions, is what extends a partial isomorphism.

[F2]

Continuous countable unions of sweetness models remain sweet: the direct union of an increasing $ω$ -chain of sweetness models is sweet and each stage is complete in the union.

[F3]

Completeness, regular opens, and order continuity: a Boolean completion is an order-dense Boolean embedding into a complete Boolean algebra. The definition itself does not assert that maps extend to completions.

[F4]

The Axiom of Choice: used exactly for the simultaneous selection of the countably many data that code the requests in the induction.

[F5]

Shelah, Claims 7.12-7.13: Claim 7.12 equips an amalgam of two arbitrary sweetness models with a sweetness model extending the first factor; it does not require the second factor to extend the first. Claim 7.13 then alternates that one-sided construction, and the union map extends uniquely to an automorphism of the Boolean completion.

Proof

1.1

First record the one-sided extension from the source result [F5]. Given a sweetness model on $P$ , complete subalgebras $C_{0}, C_{1} \leq B A (P)$ and a complete isomorphism $g : C_{0} \to C_{1}$ , take a disjoint copy $P^{'}$ with its copy isomorphism $c : B A (P) \to B A (P^{'})$ . Amalgamate the old copy and the new copy over $C_{1}$ , using the two complete embeddings $C_{1} ↪ B A (P), b ⟼ c (g^{- 1} (b)) \in B A (P^{'}) .$ If $j_{0}, j_{1}$ are the canonical embeddings into the amalgam, then $j_{0} (g (a)) = j_{1} (c (a)) (a \in C_{0}) .$ Consequently the map $g^{'} (j_{0} (x)) = j_{1} (c (x))$ is a complete isomorphism from the entire old $B A (P)$ onto the second canonical copy and satisfies $g^{'} (j_{0} (a)) = j_{0} (g (a))$ for $a \in C_{0}$ . The one-sided source conclusion recorded in [F5] equips this amalgam with a sweetness model extending the first, old factor. It places no extension requirement on the disjoint second factor. This is the twisted two-embedding construction; an untwisted identity amalgam would not extend $g$ .

F1F5

2.1

Starting from $(U_{0}, h_{0}) = (P, h)$ , alternate this one-sided construction with the same construction applied to the inverse. Thus obtain an increasing $ω$ -chain of sweetness models $U_{l}$ , complete subalgebras $B_{l}^{1}, B_{l}^{2} \leq B A (U_{l})$ and coherent complete isomorphisms $h_{l} : B_{l}^{1} \to B_{l}^{2}$ such that $B_{2 l + 1}^{1} = B A (U_{2 l}), B_{2 l + 2}^{2} = B A (U_{2 l + 1}),$ and every $h_{l + 1}$ extends $h_{l}$ . Each successor sweetness model extends the previous fixed model, not merely its forcing-equivalence class.

F4F5step 1.1

3.1

Coherence is the displayed identity in step 1.1 at each even step and its inverse analogue at each odd step. The canonical old copy is complete at every successor and its sweetness presentation is fixed by the one-sided extension conclusion in [F5].

F5step 1.1step 2.1

3.2

Each $U_{l}$ is sweet and $U_{l + 1}$ extends the model of $U_{l}$ . Therefore the direct union forcing $P^{*} = ⋃_{l} U_{l}$ , with the union dense set and stabilised relations, is sweet, and every $U_{l}$ is complete in $P^{*}$ by [F2].

F2step 2.1

3.3

The same construction is compatible with a previously fixed sweetness-model embedding: start with that presentation and use [F5]'s first-factor extension conclusion at every successor.

F5step 1.1step 2.1

4.1

Put $C = ⋃_{l} B A (U_{l})$ through the coherent complete embeddings and $f_{0} = ⋃_{l} h_{l}$ . The algebra $C$ is a Boolean algebra, but is not asserted to be complete: every finite Boolean calculation occurs in one stage, whereas an arbitrary subset of $C$ need not. Coherence makes $f_{0}$ well defined. The domain is all of $C$ because every element of $B A (U_{2 l})$ lies in $B_{2 l + 1}^{1}$ , and the range is all of $C$ because every element of $B A (U_{2 l + 1})$ lies in $B_{2 l + 2}^{2}$ . Thus $f_{0}$ is a Boolean automorphism of $C$ extending $h$ .

step 2.1step 3.1

5.1

Let $B^{*} = B A (P^{*})$ . The canonical image of $P^{*}$ is order-dense in $B^{*}$ and lies in $C$ , so $C$ is order-dense in $B^{*}$ . The source completion clause recorded in [F5] gives the unique extension of $f_{0}$ to a complete Boolean automorphism $f$ of $B^{*}$ . Explicitly it is determined by $f (b) = ⋁ {f_{0} (c) : c \in C, c \leq b},$ and the corresponding formula for $f_{0}^{- 1}$ supplies the inverse. This is a completion step after the alternating direct union; it does not identify $C$ with a complete direct limit.

F3F5step 3.2step 4.1

6.1

The complete algebra $B^{*}$ has the sweet dense forcing presentation $P^{*}$ ; no unsupported transport of the equivalence relations through the possibly noninjective completion map is used. Completeness of the stage embeddings puts the original $B$ completely inside $B^{*}$ . Hence $B^{*}$ is a sweet complete Boolean algebra in this retained-presentation sense, and $f$ is the required automorphism, compatible with the previously fixed model.

F1F2step 3.2step 3.3step 5.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

Shelah's CH-length homogeneous sweet construction

Statement

Assume ZFC and CH, explicitly $∣ P (ω) ∣ = ℵ_{1}$ . There is a continuous increasing chain of sweetness models $(P_{α}, D_{α}, E_{n}^{α})_{α < ω_{1}}$ . Put $B_{α} = B A (P_{α})$ and $P = ⋃_{α < ω_{1}} P_{α}$ . Then the $B_{α}$ form an increasing chain of complete Boolean algebras of size at most $ω_{1}$ , and the final completion $B = B A (P) = ⋃_{α < ω_{1}} B_{α}$ is ccc and has size $ω_{1}$ , such that (i) every complete isomorphism between countably generated complete subalgebras of $B$ extends to an automorphism of $B$ , and (ii) every task scheduled by the construction is met: every free-amalgamation task whose data appear at a stage is answered at a later stage, and above every stage there is a later quotient with the canonical $U M$ presentation (equivalently, its Boolean completion is identified with the quotient completion). This is Shelah's continuous sweet construction (Main Lemma 7.14(b),(d)); it is not identified with an ordinary finite-support iteration.

Facts & Assumptions

Given: ZFC and CH in the form $∣ P (ω) ∣ = ℵ_{1}$ .

[F1]

The Axiom of Choice: well-orderings of the sets of task codes used in the set-length recursion. No global choice principle is assumed.

[F2]

The successor cardinal $κ^{+}$ , the alephs $ℵ_{α}$ , the beths $ℶ_{α}$ , successor and limit cardinals, and the identifications $ℵ_{0} = ω$ and $ℵ_{1} = ω_{1}$ with Assuming the Axiom of Choice, $2^{κ} = ∣ P (κ) ∣$ , and Cantor's theorem in cardinal form: $κ < 2^{κ}$ and CH: every countable object built from $ω_{1}$ -many data has an $ω_{1}$ -bounded code, and the number of countable subsets of $ω_{1}$ is at most $ω_{1}$ .

[F3]

Sweet amalgamation extends partial Boolean isomorphisms: every complete isomorphism between countably generated complete subalgebras of a sweet algebra extends to an automorphism after one extension step.

[F4]

Shelah amalgamation preserves sweetness and Composition with universal-meagre forcing preserves sweetness: the named amalgam and canonical UM composition give sweetness models extending the fixed old model.

[F5]

Continuous countable unions of sweetness models remain sweet: sweet models are preserved at limits of countable cofinality, with every earlier stage complete in the union.

[F6]

Sweet forcings are countable unions of directed sets and ccc: every sweet stage is ccc. Under CH, $(ω_{1})^{ℵ_{0}} = (2^{ℵ_{0}})^{ℵ_{0}} = 2^{ℵ_{0}} = ω_{1}$ ; hence a ccc forcing of size at most $ω_{1}$ has a Boolean completion of size at most $ω_{1}$ , because each completion element is the join of a countable maximal antichain from a dense copy of the forcing.

[F7]

Shelah's Main Lemma 7.14 supplies the final-union clauses that are not consequences of [F5]: for the constructed chain, if $P = ⋃_{α < ω_{1}} P_{α}$ and $B = BA (P)$ , then $B$ is ccc and $B = ⋃_{α < ω_{1}} BA (P_{α}) .$ It also states the union-level automorphism-extension and free-amalgamation clauses and identifies arbitrarily late quotients with the canonical $U M$ forcing in the relevant intermediate extension. [source]

[F8]

Shelah's Claim 7.13 permits arbitrary complete subalgebras, not only countably generated ones: any isomorphism between two complete subalgebras of a sweet completion extends to an automorphism after an extension of the fixed sweetness model. This stronger source interface is used when continuing a previously extended map whose domain is an entire stage completion. [source]

Proof

1.1

Well-order all countable task codes: complete isomorphisms between countably generated complete subalgebras, pairs $C_{0} \subseteq C_{1}$ of such subalgebras requiring a free copy over $C_{0}$ , and canonical UM-extension requests. Under CH the set of countable sequences from $ω_{1}$ has size $ω_{1}$ by [F2], so use $ω_{1}$ bookkeeping that repeats every task cofinally often. A homogeneity task retains its last partial extension; later occurrences extend that coherent map over the then-current stage.

F1F2

1.2

Begin with the trivial sweetness model. At a successor, perform the named task only after all of its data have appeared. For an isomorphism task use [F8] to extend the current coherent map over the whole current completion. For $C_{0} \subseteq C_{1}$ , first use the named amalgam [F4] to create a second canonical copy of $C_{1}$ freely amalgamated with the first over $C_{0}$ , then use [F3] to extend the copy isomorphism to the required automorphism. For a UM task use the fixed-model composition in [F4]. Every successor is therefore an extension of sweetness models.

F3F4F8

1.3

At a nonzero limit $λ < ω_{1}$ , put $P_{λ} = ⋃_{α < λ} P_{α}, D_{λ} = ⋃_{α < λ} D_{α}, E_{n}^{λ} = ⋃_{α < λ} E_{n}^{α} .$ Since every such limit is countable and has countable cofinality, [F5] makes this a sweetness model extending every earlier stage. Only after forming this direct union forcing set $B_{λ} = B A (P_{λ})$ . In general $B_{λ}$ is not asserted to equal $⋃_{α < λ} B_{α}$ ; completing the direct union is a separate operation.

2.1

The recursion is well defined, every $P_{α}$ is sweet, and each earlier $P_{α}$ is complete in every later $P_{β}$ . Consequently the induced maps make $B_{α}$ a complete subalgebra of $B_{β}$ . The word "continuous" refers to the forcing/sweetness-model chain of step 1.3, not to an unproved direct union of complete algebras.

F3F4F5step 1.2step 1.3

2.2

Inductively keep $∣ P_{α} ∣ \leq ω_{1}$ : each successor construction is made from at most $ω_{1}$ conditions, and each limit below $ω_{1}$ is a countable union. Every $P_{α}$ is ccc by [F6]. A completion element is the join of a maximal antichain from the dense image of $P_{α}$ , that antichain is countable, and [F6] gives at most $(ω_{1})^{ℵ_{0}} = ω_{1}$ such codes. Hence $∣ B_{α} ∣ \leq ω_{1}$ at every stage without treating the construction as a finite-support iteration.

F2F6step 1.2step 1.3

2.3

Every countable task has a bounded set of birth stages, hence is active at all sufficiently late occurrences of its code. Repeated occurrences of an isomorphism task form a coherent cofinal chain of extensions. A free-amalgamation requirement, once realised, remains realised in all later complete extensions. UM requests occur unboundedly often, so arbitrarily late successor quotients are the canonical UM forcing.

F1F2F3F4step 1.1step 1.2

3.1

Let $P = ⋃_{α < ω_{1}} P_{α}$ and put $B = B A (P)$ . This is an $ω_{1}$ -length union, so [F5] does not apply. Instead the special final-union conclusion recorded in [F7] proves the identity $B = ⋃_{α < ω_{1}} B A (P_{α})$ and proves that $B$ is ccc. The identity and step 2.2 give $∣ B ∣ \leq ω_{1}$ . The unboundedly many nontrivial UM quotients make the chain strictly increase unboundedly often, so $∣ B ∣ \geq ω_{1}$ . Hence $∣ B ∣ = ω_{1}$ .

F4F7step 2.2step 2.3

4.1

Let $f : A \to A^{'}$ be a complete isomorphism between countably generated complete subalgebras of $B$ . By the final identity in step 3.1, the countable generating data occur at a bounded stage. Its repeated bookkeeping thread extends coherently over unboundedly many later stages, and its union is an automorphism of $B$ extending $f$ . This is clause (b) of [F7], not the unsupported extension of a single-stage automorphism. Clause (c) gives the final free-amalgamation property, and clause (d) gives the arbitrarily late UM quotients.

F2F3F7step 1.1step 2.3step 3.1

5.1

Steps 1.1--2.3 construct the continuous chain of sweetness models; step 3.1 performs the distinct final Boolean-completion argument; and step 4.1 gives the union-level homogeneity, free-amalgamation and UM clauses. This proves the Statement.

step 2.3step 3.1step 4.1∎

LemmaStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

Real names are captured and coded meagre unions are absorbed

Statement

In the generic extension by the final algebra $B$ of the CH-length construction, every name for a real, for a Borel code, or for a countable sequence of ordinals is equivalent to a name over some $B_{α}$ . Consequently, for every such sequence $s$ , a later $U M$ quotient makes the union of all meagre Borel sets coded in $V [s]$ meagre. When the construction starts over $L$ , the choices made by the generic on the countably many deciding antichains for $s$ are coded by one real, while the ground-model name and antichain enumerations have ordinal codes; hence $s$ is definable from that real and finitely many ordinals.

Facts & Assumptions

Given: A $B$ -generic filter $G$ over a ground model $V$ , the CH-length chain $(B_{α})_{α < ω_{1}}$ of Shelah's CH-length homogeneous sweet construction with union $B$ , and a $B$ -name $\dot{s}$ for a real, a Borel code, or a countable sequence of ordinals.

[F1]

Shelah's CH-length homogeneous sweet construction: the sweetness-model chain is continuous, each $B_{α} = B A (P_{α})$ is a complete subalgebra of $B$ , the final identity is $B = ⋃_{α < ω_{1}} B_{α}$ , and $B$ is ccc. Arbitrarily late successor quotients carry the canonical UM presentation; in particular, every antichain in $B$ is countable.

[F2]

Forcing theorem: forcing is definable and satisfies the truth lemma.

[F3]

Monotonicity, density, and decision for forcing: for each formula the conditions deciding it are dense; with The Axiom of Choice, one may extend a maximal antichain inside each such dense set.

[F4]

Assuming countable choice: every at most countable subset of $ω_{1}$ is bounded below $ω_{1}$ , so no at most countable subset of $ω_{1}$ is cofinal in it, and a supremum of at most countably many at most countable ordinals is at most countable with The Axiom of Choice: a countable set of ordinals below $ω_{1}$ is bounded, and the countably many birth stages of the data of a name can be enumerated.

[F5]

A universal-meagre generic absorbs old nowhere-dense sets: a $U M$ quotient absorbs all ground-model closed nowhere-dense sets into a single coded meagre envelope.

[F6]

The canonical definable global well-order of L: in a constructible ground every forcing name, antichain and enumeration used below has a canonical ordinal code; the same well-order is computed internally in $L$ .

Proof

1.1

Capture of reals: let $\dot{x}$ be a $B$ -name for a real. For each $n < ω$ , [F3] makes the set of conditions deciding the value of $\dot{x} (n)$ dense; use Choice to take a maximal antichain $A_{n}$ in that dense set, labelled by the decided value $0$ or $1$ . Each $A_{n}$ is countable by the ccc in [F1]. Thus $A = ⋃_{n < ω} A_{n}$ is countable, and the set of stages in which its members occur is countable and bounded by some $α < ω_{1}$ by [F4]. Since $B_{α}$ is complete in $B$ , every $A_{n}$ remains maximal in $B_{α}$ . The labelled antichains therefore define a $B_{α}$ -name ${\dot{x}}_{α}$ ; for every generic $G$ , the unique member of $A_{n} \cap G$ gives both ${\dot{x}}_{G} (n)$ and $({\dot{x}}_{α})_{G \cap B_{α}} (n)$ , so the two names have the same value coordinatewise. Hence every real name is equivalent to a $B_{α}$ -name.

F1F2F3F4

2.1

Capture of countable ordinal sequences and Borel codes: for a name forced to be a function from $ω$ to the ordinals, apply [F3] to each coordinate and choose a maximal antichain every member of which decides that coordinate as a check ordinal. The forcing theorem guarantees that this deciding set is dense; no upper bound on the decided ordinals is assumed in advance. The union of the antichains is countable by [F1] and Choice, so [F4] bounds the birth stages of all its Boolean conditions below one $α$ . The ordinal labels are ground objects and may be used unchanged in the resulting $B_{α}$ -name. A Borel-code name is a name for a hereditarily countable code; decide the entries of a fixed real/ordinal coding in the same way.

F1F2F3F4step 1.1

3.1

Suppose now that the ground is $L$ . The original name $\dot{s}$ is a ground set, and [F6] assigns it an ordinal code. For every coordinate choose the $<_{L}$ -least maximal deciding antichain and its $<_{L}$ -least enumeration $⟨ a_{n, k} : k < ω ⟩$ (padding a finite antichain). The entire sequence of labelled enumerations is a constructible set and therefore has one further ordinal code. The generic meets exactly one $a_{n, k}$ for each $n$ ; encode the resulting sequence of indices $k (n)$ by one real $r$ . From $r$ and the two ordinal codes, the canonical $L$ well-order reconstructs the name, every labelled antichain, and hence every value $s (n)$ . Thus $s$ is definable from one real and finitely many ordinals. This argument uses the complete stage embeddings to locate the antichains; it does not claim that an ultrafilter on an arbitrary countably generated complete algebra is generated by algebra generators.

F1F2F6step 2.1

3.2

Absorption at a later UM quotient: let $α$ capture $s$ , so $s \in V [G \cap B_{α}]$ . Choose $β \geq α$ for which the next quotient has the canonical UM presentation from [F1]. Then every closed nowhere-dense code in $V [s] \subseteq V [G \cap B_{β}]$ is old for that exact UM forcing. By [F5], their union is contained in one meagre $F_{σ}$ envelope coded by the quotient generic. Every meagre Borel code includes a countable closed-nowhere-dense cover, so the same envelope contains the union of all meagre Borel sets coded in $V [s]$ . No transport of absorption through bare forcing equivalence is invoked.

F1F5step 2.1

4.1

The steps above prove the capture clauses and the absorption clause, and step 3.1 gives the constructible real-and-ordinal presentation; this is the Statement.

step 3.1step 3.2∎

LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

Strongly homogeneous truth has Baire representatives

Statement

Let $B$ be the final Boolean algebra of the Shelah construction. For every formula $φ (x, s, \vec{γ})$ with a countable ordinal-sequence parameter $s$ and finitely many ordinal parameters $\vec{γ}$ , the set of reals $x$ for which the $B$ -generic extension satisfies $φ (x, s, \vec{γ})$ differs from a Borel set by a meagre set. In particular this holds for real-and-ordinal parameters. The Borel code and meagre-error code belong to the final extension.

Facts & Assumptions

Given: The final algebra $B$ of the CH-length construction with generic $G$ , a formula $φ$ , a countable ordinal-sequence parameter $s$ , ordinal parameters $\vec{γ}$ , and the set $A = {x : φ (x, s, \vec{γ}) holds in V [G]}$ .

[F1]

Real names are captured and coded meagre unions are absorbed: $s$ is captured at some stage, and a later $U M$ quotient absorbs the union of all meagre Borel sets coded in $V [s]$ into one coded meagre envelope.

[F2]

Shelah's CH-length homogeneous sweet construction with Sweet amalgamation extends partial Boolean isomorphisms: complete isomorphisms between countably generated complete subalgebras extend to automorphisms of $B$ , and the final free-amalgamation clause supplies independent copies over a fixed captured subalgebra. These are the quotient-homogeneity interfaces used in Shelah's application of Solovay's argument; no assertion that arbitrary Cohen conditions are directly conjugate is made.

[F3]

The property of Baire: a set has the Baire property when it differs from an open set by a meagre set.

[F4]

Borel-code, measure, category, and perfect-set absoluteness: Borel codes evaluate identically on shared reals; every Borel code uniformly yields an open representative modulo an explicitly coded sequence of closed nowhere-dense sets; and coded category witnesses transfer at the stated same-real interfaces.

[F5]

Forcing theorem: truth and forcing agree for generic filters, so the Cohen-generic points determine the truth value of $φ$ at the canonical Cohen name.

[F6]

Shelah's Main Lemma 7.14(b),(c) gives automorphism extension and free amalgamation for countably generated complete subalgebras, and Theorem 7.16 invokes Solovay's argument from these clauses and the meagre-set absorption. Solovay's Part III §§1.4--1.6 first localizes at a forcing condition and then uses the category analogue of Theorem II.2.8 to obtain one Borel reading on all Cohen generics over the intermediate model. Thus the relevant interface is a compatible family of local Cohen-cone readings, not a complete embedding obtained from an arbitrary name merely forced to be Cohen-generic. [source]

Proof

1.1

By [F1], choose a stage $α$ containing a name for $s$ and all Boolean values used below. Enlarge to a later stage $β$ so that the next designated quotient has the canonical UM presentation. Put $M = V [s]$ , not $V [G \cap B_{β}]$ . Then every meagre Borel set coded in $M$ is among the sets absorbed by that quotient, exactly as [F1] states. The ordinal parameters already belong to $V$ and hence to $M$ . Every relevant countably generated complete subalgebra and name can be placed in a later stage because its countable set of Boolean data is bounded in the $ω_{1}$ construction.

F1F2

2.1

In the ground model choose, for each coordinate of the fixed name $\dot{s}$ , a countable maximal antichain labelled by its decided ordinal value, and let $C_{s}$ be the completion of the countable Boolean algebra generated by all members of those antichains. The labelled antichains make $\dot{s}$ a $C_{s}$ -name. Conversely, $s$ determines which member of every labelled antichain lies in $G$ : combine equal labels first, so distinct antichain members have distinct labels. Those antichains generate a countable dense subalgebra of $C_{s}$ , and a generic ultrafilter is determined by its trace on a dense subalgebra. Consequently $V [G \cap C_{s}] = V [s] = M .$ Choose the stage in step 1.1 to contain the countably many generators; completeness then contains $C_{s}$ . For every dense open $D \subseteq 2^{< ω}$ in $M$ , the reals whose initial-segment filters miss $D$ form a closed nowhere-dense set coded in $M$ . By [F1], the later UM quotient puts the union of all these sets inside one meagre set. Thus the final extension contains Cohen reals over $M$ , by its ZFC Baire theorem. This existence assertion is not promoted to a claim that an arbitrary name for one of those reals canonically embeds the full Cohen algebra.

F1F2step 1.1

3.1

Work in $M$ and let $C$ be the Cohen category algebra. A local Cohen chart consists of a nonzero $a \in B$ , a $B$ -name $\dot{x}$ , and $a ⊩ \dot{x}$ is Cohen-generic over the canonical $C_{s}$ -extension. The map $j_{a, \dot{x}} (u) = a \land ∥ \dot{x} \in u ∥_{B} (u \in C)$ is a complete Boolean homomorphism into $B ↾ a$ , but need not be injective: prepending $0$ to a Cohen name kills the nonzero cylinder $[1]$ . Its kernel is a complete ideal, hence is $C ↾ \neg d$ for a unique nonzero support $d \in C$ , and the restriction $j_{a, \dot{x}} : C ↾ d ⟶ j_{a, \dot{x}} [C]$ is a complete isomorphism with top $a$ . The complete subalgebra generated by $C_{s}$ , this range, and $a$ is countably generated. This is the required localization; no full Cohen copy is inferred from genericity of the name.

F5F6step 2.1

4.1

Put $b_{a} = a \land ∥ φ (\dot{x}, \dot{s}, \overset{ˇ}{\vec{γ}}) ∥_{B}$ and let $C$ be the chart algebra from step 3.1. Inside the relative algebra below $a$ , repeat Shelah's free-amalgamation argument. If $D$ is generated by $C \cup {b_{a}}$ , a free copy of $D$ over $C$ extends to an automorphism fixing $C$ . It fixes $a$ , the parameter name, and every Boolean value of the coordinate name below $a$ , so it fixes $b_{a}$ . If the two projections of $b_{a}$ and $a ∖ b_{a}$ to $C ↾ a$ overlapped, freeness would make $b_{a}$ compatible with the image of its complement, a contradiction. Hence $b_{a} \in C ↾ a$ . Via the isomorphism in step 3.1 it has a unique reading $c_{a, \dot{x}} \leq d$ in the Cohen algebra, represented by a regular open, and therefore Borel, subset of $d$ .

F2F5F6step 3.1

5.1

These local readings are coherent. On a nonzero overlap of two support elements, restrict both chart algebras to that overlap. Their coordinate isomorphism fixes $C_{s}$ and sends one restricted Cohen name to the other; [F2] extends it to an automorphism of $B$ . Since the parameters are fixed, invariance of Boolean truth sends one restricted value from step 4.1 to the other, so the two Cohen readings agree on the overlap. The family of chart supports is dense in $C$ : from one Cohen real supplied by step 2.1, an $M$ -coded category-algebra isomorphism into any prescribed nonzero regular open set produces a chart supported below that set. Choose a maximal antichain of chart supports. It is countable, and the coherent local readings paste to one $c \in C$ , hence to one Borel code in $M$ . Every $M$ -Cohen-generic real meets this antichain and, by applying the same overlap argument to a chart containing its chosen name and forcing condition, satisfies $V [G] ⊨ φ (x, s, \vec{γ}) ⟺ x \in C_{c} .$ Consequently $A △ C_{c}$ is contained in the set $X$ of reals not Cohen-generic over $M$ . This is precisely the local-cone step in Solovay's argument cited in [F6]; it does not assert a canonical complete copy for every generic name.

F2F5F6step 2.1step 3.1step 4.1

6.1

For each dense open $D \subseteq 2^{< ω}$ in $M = V [s]$ , the set of reals whose initial-segment filter misses $D$ is a closed nowhere-dense set coded in $V [s]$ . Their union is exactly $X$ . The family need not be countable in $M$ , but every member is among the meagre Borel sets whose codes [F1] absorbs at the designated UM quotient chosen in step 1.1. The absorption clause therefore gives in the final extension one coded meagre $F_{σ}$ set $E$ containing all of $X$ . Hence $A △ C_{c} \subseteq E .$

F1step 1.1step 2.1step 5.1

7.1

The conclusion so far is a Borel representative, not necessarily an open one. Apply the uniform construction in [F4] to $c$ : it gives an open code $u$ and a coded meagre set $E_{c}$ with $C_{c} △ U_{u} \subseteq E_{c}$ . Therefore $A △ U_{u} \subseteq E \cup E_{c},$ and the right side is meagre. All three codes belong to the final extension. This is the explicit Borel-to-open step required by the definition of the Baire property.

F3F4step 6.1

8.1

A real is a countable ordinal sequence, so real-and-ordinal parameters are a special case. Conversely, the proof began with an arbitrary captured countable ordinal sequence $s$ , so it does not rely on replacing $s$ by a real unless the constructible-ground coding of [F1] is invoked later. Steps 6.1--7.1 prove the Statement.

F1step 6.1step 7.1∎

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-22Open item page →

The Shelah HOD(S) model and its real-ordinal presentation

Definition

Work in the generic extension $V [G]$ of the CH-length Shelah construction Shelah's CH-length homogeneous sweet construction started over the constructible universe $L$ . Let $S = ⋃_{α \in O r d}^{ω} α$ be the class of all countable sequences of ordinals, exactly as in the Solovay $H O D (S)$ presentation The hereditarily ordinal-sequence-definable Solovay model, and define

$N = H O D (S) = {x : tc ({x}) \subseteq O D (S)},$

where $O D (S)$ is the class of sets uniquely definable in a rank from one $s \in S$ , finitely many ordinals and a formula, in the sense of Ordinal definability and HOD. The definition is the same uniform first-order class as in the Solovay presentation, with the ambient model now being the Shelah extension rather than a Lévy collapse.

Conventions proved in this pair. Finite and countable tuples of members of $S$ interleave into one member of $S$ by a fixed pairing function on $ω$ , so "one $S$ -parameter" loses no generality; a real, viewed as a binary sequence of ordinals, is itself a member of $S$ ; and every real belongs to $N$ , because a real is definable from itself as an $S$ -parameter.

Real-ordinal presentation. In this branch the ambient ground model is $L$ . By the countably-generated-support coding of Real names are captured and coded meagre unions are absorbed, every set $A \subseteq R$ in $N$ is definable from one real together with finitely many ordinals: take the $B$ -name of the $S$ -parameter defining $A$ , capture its countably many deciding antichains in a stage $B_{α}$ , record the generic's chosen index in each of them by a single real, and code the ground-model name and the canonical enumerations by ordinals, which lie in $L$ . Conversely, a real together with finitely many ordinals interleaves into one member of $S$ . This is the real-and-ordinal presentation required by the equiconsistency statement; it is asserted only in the branch over $L$ and is not claimed for an arbitrary ground extension.

No equality with $L (R)$ , with $H O D (R)$ , or with any class built from all $ω_{1}$ -sequences of ordinals is asserted. The ambient $ω_{1}$ is not collapsed: the construction is ccc and adds no new ordinals, so the ordinal height of $N$ is that of $V [G]$ .

LemmaStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

The Shelah inner model is closed under ambient omega-sequences

Statement

If $f$ belongs to the ambient ZFC forcing extension and maps $ω$ into $N = H O D (S)$ , then $f$ itself belongs to $N$ .

Facts & Assumptions

Given: The class $N = H O D (S)$ of The Shelah HOD(S) model and its real-ordinal presentation and an ambient function $f : ω \to N$ .

[F1]

The Shelah HOD(S) model and its real-ordinal presentation with Ordinal definability and HOD: membership in $N$ means hereditary $O D (S)$ -definability, so every $y \in N$ has a code consisting of a formula, a rank, finitely many ordinals and one member of $S$ .

[F2]

$N \times N \approx N$ supplies a fixed definable bijection $b : ω \times ω \to ω$ .

[F3]

The Axiom of Choice supplies a choice function on a set of nonempty sets; Collection first bounds the witnesses used below.

[F4]

Montague–Lévy reflection for a finite formula family reflects each fixed finite family of formulas, with arbitrary set parameters in the reflecting rank. Thus an ambient unique definition from an $S$ -parameter and finitely many ordinals gives a rank definition with the same parameters.

Proof

1.1

A valid definition code is a tuple $c = (e, θ, k, ⟨ a_{j} : j < k ⟩, s)$ , where $e, k < ω$ , $θ > 0$ is an ordinal, $s \in S \cap V_{θ}$ , each $a_{j} < θ$ , and the formula with code $e$ has a unique solution $y \in V_{θ}$ with parameters $s, a_{0}, \dots, a_{k - 1}$ . Write $R (c, y)$ for this assertion. Set satisfaction makes $R$ a single first-order relation; no truth predicate for the universe is used. For every $y \in N$ , hereditary membership includes $y \in O D (S)$ , so [F1] supplies such a code. Retain all its components rather than treating the rank as a code for the formula and tuple.

2.1

For every $n < ω$ some set code $c$ satisfies $R (c, f (n))$ . Collection yields a set $C$ containing a witness for each $n$ . Separation gives nonempty sets $C_{n} = {c \in C : R (c, f (n))}$ . Apply [F3] once to the set ${C_{n} : n < ω}$ , and compose its choice function with $n \mapsto C_{n}$ to obtain $c_{n} = (e_{n}, θ_{n}, k_{n}, ⟨ a_{n, j} : j < k_{n} ⟩, s_{n}) \in C_{n}$ . This selects from sets, not proper classes.

F3step 1.1

3.1

For each $n$ define an ordinal sequence $t_{n}$ by $t_{n} (0) = e_{n}$ , $t_{n} (1) = θ_{n}$ , $t_{n} (2) = k_{n}$ , $t_{n} (3 + 2 j) = a_{n, j}$ for $j < k_{n}$ and $t_{n} (3 + 2 j) = 0$ otherwise, and $t_{n} (4 + 2 j) = s_{n} (j)$ for every $j < ω$ . Define $s^{*} (b (n, j)) = t_{n} (j)$ using [F2]. Replacement produces this function on $ω$ ; the supremum of its set of ordinal values, plus one, bounds its range, so $s^{*} \in S$ . Decoding recovers all five components of every $c_{n}$ , including the empty tuple when $k_{n} = 0$ .

F1F2step 2.1

4.1

The fixed first-order condition on a set $g$ saying that $g$ is a function with domain $ω$ and $R (c_{n}, g (n))$ holds for each $n$ , with $c_{n}$ decoded from $s^{*}$ as in step 3.1, has the unique solution $g = f$ . Existence follows from the selected codes and uniqueness from their unique solutions. Reflect this formula and its uniqueness assertion to a rank containing $f$ and $s^{*}$ by [F4]. Thus $f \in O D (S)$ under the rank-definition convention. Its graph consists of the ordered pairs $(n, f (n))$ , not $(f (n), n)$ ; its values need not be ordinals.

F1F4step 1.1step 3.1

5.1

Finite sets of $O D (S)$ objects are again in $O D (S)$ . Indeed combine finitely many of their valid codes into one ordinal sequence by the coding of step 3.1; the fixed relation $R$ uniquely reconstructs each object, and an ambient formula uniquely specifies their finite set. Reflection as in step 4.1 gives a rank definition. Every ordinal is ordinal definable using itself as parameter. Since $f (n) \in N$ , each $f (n)$ and all its descendants are in $O D (S)$ by [F1]. For the Kuratowski pair $(n, f (n)) = {{n}, {n, f (n)}}$ , the pair and its two members are in $O D (S)$ by finite-set closure; their further descendants are ordinals below $n$ , or $f (n)$ and its descendants. Together with $f \in O D (S)$ , this accounts for every member of $tc ({f})$ . Hence $f \in N$ .

F1F2F4step 3.1step 4.1

6.1

The selected codes, explicit decoding and hereditary check prove that every ambient function $f : ω \to N$ belongs to $N$ . The argument uses only the defining class $H O D (S)$ in the ambient ZFC universe, not any homogeneity or regularity assertion about the Shelah forcing.

step 2.1step 5.1∎

TheoremStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

The Shelah inner model satisfies ZF and Dependent Choice

Statement

$N = H O D (S)$ is a transitive inner model with the same ordinals and reals as the ambient Shelah extension, satisfies every axiom of ZF, and satisfies the serial-relation form of Dependent Choice.

Facts & Assumptions

Given: The class $N$ of the definition item in the ambient Shelah extension.

[F1]

The Shelah HOD(S) model and its real-ordinal presentation: membership in $N$ is hereditary unique definability in a rank from one countable ordinal sequence and finitely many ordinals; the class is first-order and contains all reals and all ordinals; finite tuples of $S$ -parameters interleave.

[F2]

The Shelah inner model is closed under ambient omega-sequences: every ambient $ω$ -sequence with values in $N$ belongs to $N$ .

[F3]

The Solovay inner model satisfies ZF and every real set has a real–ordinal definition and The Solovay inner model satisfies Dependent Choice: the corresponding ZF and DC clauses are already proved for the Solovay $H O D (S)$ model at exactly this interface.

[F4]

The serial-relation Dependent Choice principle over ZF: DC says that for every nonempty set $A$ and every serial relation $R$ on $A$ , there is a sequence $⟨ a_{n} : n < ω ⟩$ in $A$ with $R (a_{n}, a_{n + 1})$ for all $n$ . The definition expressly distinguishes this from the prescribed-start form.

[F5]

The Axiom of Choice: ambient AC, used only to produce the ambient recursive chain below.

Proof

1.1

$N$ is transitive and contains all ordinals and all reals: the transitive closure of a member of $N$ consists of $O D (S)$ -sets by hereditaryness, and every ordinal and every real is definable in a rank from itself as a parameter, so both lie in $N$ . Since the sheaf of definitions is rank-bounded, $N$ is a transitive class, exactly at the HOD(S) interface of [F3].

F1F3

1.2

Extensionality, Foundation, Pairing, Union and Infinity hold: each axiom's witness is definable in a rank from the same parameters as its inputs, and the definitions close under these operations because a finite tuple of $S$ -parameters interleaves into one.

1.3

Separation: for $A \in N$ and a formula $ψ$ , the set $A \cap ψ^{N}$ is defined in a rank from the definition of $A$ conjoined with $ψ$ and the rank bound of the separating instance, so it lies in $N$ .

1.4

Replacement: if $F$ is a definable function on $A \in N$ with values in $N$ , then the image is defined from the same $S$ -parameter and ordinals as $A$ and $F$ , without selecting a code for each value: one quantifies in a rank over the unique value of $F$ . Hence the image belongs to $N$ .

1.5

Power set: for $A \in N$ , the uniform predicate " $y$ is a subset of $A$ " is ranked and definable from the parameters defining $A$ , so the power set of $A$ as computed in $N$ is a set of $N$ . Together with steps 1.2 through 1.4 this verifies all axioms of ZF in $N$ .

1.6

Dependent Choice: let $A \in N$ be nonempty and let $R \in N$ be serial on $A$ . In the ambient model, AC first selects some $a_{0} \in A$ and then recursively chooses $a_{n + 1} \in A$ with $R (a_{n}, a_{n + 1})$ , which is possible by seriality. The resulting $ω$ -sequence lies in $N$ by [F2]; transitivity and the absoluteness of membership in the set $R$ give $N ⊨ R (a_{n}, a_{n + 1})$ for all $n$ . Thus the starting-point-free serial-relation form of DC stated in [F4] holds in $N$ ; no equivalence with the separately named prescribed-start form is used.

F2F4F5

2.1

$N$ has the same ordinals and reals as the ambient extension, since it contains them all and is transitive.

F1step 1.1

3.1

Steps 1.1 through 1.6 verify the ZF and same-ordinals-and-reals clauses, and step 1.6 verifies DC; this is the Statement.

step 2.1step 1.6∎

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

Every real set in the Shelah inner model has the Baire property

Statement

$N$ satisfies: every subset of the reals has the property of Baire. Here the set-theoretic reals are represented first by Cantor space $2^{ω}$ ; the same assertion for the usual real line follows through comeagre homeomorphic coding subspaces. Explicitly, for each real set $A \in N$ there are in $N$ an open set $U$ and a meagre set $M$ in the relevant space such that $A △ U \subseteq M$ .

Facts & Assumptions

Given: A set $A \subseteq R$ with $A \in N$ in the ambient Shelah extension.

[F1]

The Shelah HOD(S) model and its real-ordinal presentation: $A$ has a rank-bounded definition from one $s \in S$ and finitely many ordinals; over the constructible ground this is equivalent to definability from one real and finitely many ordinals.

[F2]

Strongly homogeneous truth has Baire representatives: for every formula with a countable ordinal-sequence parameter, the set of binary reals satisfying it differs from a Borel set by a coded meagre set; its proof places the Boolean truth value in the countably generated parameter-and-Cohen algebra by free amalgamation and transports its Borel reading by automorphism extension.

[F3]

The Shelah inner model satisfies ZF and Dependent Choice: $N$ is transitive and has the same reals as the ambient extension.

[F4]

The property of Baire: the property of Baire is the existence of an open set differing from the given set by a meagre set.

[F5]

Borel-code, measure, category, and perfect-set absoluteness: from a Borel code one uniformly obtains an open code and a coded sequence of closed nowhere-dense sets covering their symmetric difference. Its stated evaluation-absoluteness interface is restricted to Solovay intermediate models, so the proof below does not apply that clause to $N$ .

[F6]

Cantor and Baire sequence spaces and coordinate codings gives a homeomorphism from $ω^{ω}$ onto the subspace $D \subseteq 2^{ω}$ of sequences with infinitely many $1$ s, with countable complement. Baire sequence space is homeomorphic to the irrational real numbers identifies $ω^{ω}$ with $R ∖ Q$ , and $Q$ is countably infinite makes the omitted rational set countable.

[F7]

Well-founded Borel evaluation codes: a Borel code is a real-coded countable labelled tree whose child relation is well-founded, and evaluation proceeds through leaf, complement and countable-union nodes.

Proof

1.1

First let $A \subseteq 2^{ω}$ belong to $N$ . By [F1], $A$ has a rank-bounded definition from one parameter $s \in S$ and finitely many ordinals. Applying [F2] to that exact defining formula gives a Borel code $c$ and a coded meagre set $E_{0}$ in the ambient extension with $A △ C_{c} \subseteq E_{0}$ . This uses the claim as written; no open set is read directly from the Borel representative.

F1F2

1.2

This proves the all-Baire-property assertion for the standard set-theoretic real space $2^{ω}$ . To compare with the usual real line, let $D \subseteq 2^{ω}$ be the infinitely-many- $1$ s subspace of [F6]. Its complement is explicitly at most countable and hence meagre; likewise $Q$ is countable and meagre in $R$ . Composing the two homeomorphisms in [F6] gives $h : D ⟶ R ∖ Q .$

F3F6

2.1

Apply only the uniform construction clause of [F5] to $c$ . It yields an open code $u$ and a coded sequence of closed nowhere-dense sets covering $C_{c} △ U_{u}$ . Pair the Borel/open code and both meagre-error sequences into finitely many binary reals. By [F3], every such code real belongs to $N$ .

F3F5step 1.1

3.1

We verify the needed absoluteness directly, rather than use the Solovay-intermediate-model clause of [F5]. A code from [F7] is a labelled tree on $ω^{< ω}$ and hence a real. If its child relation were ill-founded in either of the two transitive same-real models, DC in $N$ (and Choice in the ambient extension) would produce a descending sequence of nodes, itself a real; therefore well-foundedness agrees. For a shared real $x$ , if the two evaluations first differed at a node, an $R$ -minimal such node would have agreeing child evaluations, and the leaf, complement and union rules would force agreement at that node, a contradiction. Thus $C_{c}$ and $U_{u}$ have identical evaluations on the common reals. For a binary tree code, closedness is immediate and nowhere density is the arithmetic finite-cylinder test: every finite word has an extension above which some finite level has no tree node. That test is absolute, so every displayed closed-nowhere-dense code remains such in $N$ .

F3F7step 2.1

4.1

Membership in $A \in N$ is absolute between the transitive model $N$ and the ambient extension. Hence the ambient inclusions from steps 1.1 and 2.1, together with step 3.1, give $N ⊨ A △ U_{u} \subseteq E_{0} \cup E_{c} .$ Dependent Choice in [F3] supplies Countable Choice, and the two actual coded sequences of nowhere-dense sets therefore witness in $N$ that the right side is meagre.

F3F4step 1.1step 2.1step 3.1

5.1

Let $A \subseteq R$ belong to $N$ . The coded set $A^{*} = h^{- 1} [A \cap (R ∖ Q)] \subseteq D$ , viewed as a subset of $2^{ω}$ by putting no points outside $D$ , belongs to $N$ . Step 4.1 gives $A^{*} △ U$ meagre in $2^{ω}$ . Restrict to the dense subspace $D$ and transport by $h$ : the image differs from the relatively open set $h [U \cap D]$ by a meagre subset of $R ∖ Q$ . A nowhere-dense subset of a dense subspace is nowhere dense in the whole space after taking ambient closure, so that error is meagre in $R$ . Write the relatively open image as $W \cap (R ∖ Q)$ for an open $W \subseteq R$ . Adding the countable rational set shows $A △ W$ is meagre in $R$ . All maps, countable complements and codes used here are the fixed objects of [F6] and belong to $N$ .

F3F4F6step 4.1step 1.2

6.1

Since $A$ was arbitrary, steps 4.1 and 5.1 prove the assertion for both the set-theoretic and usual-real conventions, with witnesses in $N$ . This is the Statement.

F3step 4.1step 5.1∎

TheoremStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

The exact equiconsistency of ZFC and the all-Baire-property model

Statement

The following theories are equiconsistent: ZFC; ZFC plus "every real set first-order definable from a real and an ordinal parameter has the Baire property"; and ZF+DC plus "every set of reals has the Baire property". In particular, $Con (Z F C)$ is equivalent to $Con (Z F + D C + all real sets have BP)$ , with no inaccessible-cardinal hypothesis.

Facts & Assumptions

Given: Fixed arithmetizations of the three theories and of ZFC as in the formal-consistency items.

[F1]

Formal consistency of ZFC plus GCH relative to ZF: a verified proof transformation gives $Con (Z F) \to Con (Z F C + G C H)$ , without a transitive model assumption.

[F2]

Shelah's CH-length homogeneous sweet construction: under ZFC+CH there is a CH-length sweet construction whose final algebra is ccc and has the stated homogeneity, free-amalgamation and $U M$ -quotient properties. This interface supplies that mathematical construction, not a uniform formal forcing verification.

[F3]

Shelah's numbered conclusion cited in the source block states exactly that ZFC, ZFC plus the real-and-ordinal-definable Baire-property assertion, and ZF+DC plus universal Baire property are equiconsistent. Its proof remark supplies both forward models: Theorem 7.16 gives the definable-set Baire property in the full forcing extension, while $H O D (S)$ gives the ZF+DC model with universal Baire property. It invokes Gödel's $L$ for the reverse implications. This item uses that published equiconsistency theorem directly; it does not infer a proof-code compiler from [F2].

[F4]

The Shelah inner model satisfies ZF and Dependent Choice with Every real set in the Shelah inner model has the Baire property: inside the extension, $N$ satisfies ZF+DC and every set of reals in $N$ has the Baire property. This interface supplies only the inner model; it is not used to transfer Baire-property witnesses or arbitrary definable sets upward to the full extension.

[F5]

Semantic and formal inner-model theorem for L with The constructible universe satisfies AC: for every model of any of the three theories, its constructible universe satisfies ZFC internally.

Proof

1.1

The exact three-way equiconsistency assertion is Shelah's cited conclusion by [F3]. We record how its two directions match the semantic interfaces developed on this page.

1.2

For the forward construction, the standard $L$ reduction and [F1] provide the CH ground assumed by [F2]. The source theorem and proof remark incorporated in [F3] give the real-and-ordinal-definable Baire-property clause in the full forcing extension. Separately, [F4] gives the inner model $N ⊨ Z F + D C +$ universal Baire property. These are the two models named in [F3]; no inference from the inner model's witnesses to the full extension is made.

F1F2F3F4

1.3

For the reverse direction, [F3] invokes Gödel's work on $L$ ; [F5] is the library's semantic counterpart: the constructible universe internally satisfies ZFC, and the Baire-property clause plays no role.

F3F5

1.4

No inaccessible cardinal is used: the forward route of [F3] is the ccc sweet construction over CH, and the reverse route is $L$ .

F1F2F3

2.1

Thus the published equiconsistency theorem [F3], with steps 1.2--1.3 identifying its constructions with the exact semantic results proved on this page, gives the Statement. Nothing here claims that [F2] alone supplies the uniform proof-code verification required by a formal forcing compiler.

F3step 1.2step 1.3step 1.4∎

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-22Open item page →

Boldface Sigma-one-three measurability

Definition

Work in Cantor space $C = 2^{N}$ , with auxiliary real quantifiers ranging over Baire space $N = N^{N}$ as in Cantor and Baire sequence spaces and coordinate codings. Fix a real parameter $x$ .

A set $A \subseteq C$ is $Σ_{3}^{1} (x)$ when membership in $A$ has the form

$a \in A ⟺ \exists y \forall z \exists w θ (a, y, z, w, x),$

where $y, z, w$ range over Baire space and $θ$ is arithmetic: all its quantifiers are number quantifiers and its atomic statements are those of a fixed recursive decoding of the sequences involved. Thus the leading real quantifiers are one existential, one universal and one existential, the last being the one that may be dummy. A set is boldface $Σ_{3}^{1}$ when it is $Σ_{3}^{1} (x)$ for some real $x$ , and the regularity assertion boldface $Σ_{3}^{1}$ -measurability means that every such set belongs to the completed coin-measure domain specified below.

The measured domain. In applications assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). The proof of Dyadic coding supplies coin measure and its completed Lebesgue transfer uses DC only in its step 1.2 to derive Countable Choice; after that step, its cylinder-pullback construction of the Borel coin probability $ν$ uses only the resulting Countable Choice hypotheses. Thus the same construction is available directly under the present assumption. Write $B$ for its Borel sigma-algebra. Define $\overline{B} : = {E \subseteq C : E = B \cup N, B, Z \in B, N \subseteq Z, ν (Z) = 0} .$ For such a representation put $\overline{ν} (E) : = ν (B)$ . This is exactly the completion construction of The completion domain and proposed completed set function of a measure space, so Assuming countable choice, every measure space has a unique complete extension to its completion proves that this value is independent of the representation and is a complete measure on the displayed sigma-algebra. Thus the regularity assertion is precisely $\forall x \in N \forall A \subseteq C (A \in Σ_{3}^{1} (x) ⟹ A \in \overline{B}) .$ The dyadic lemma supplies the Borel measure; the completion theorem supplies its completed domain and measure. No completion or measure transport is inferred from a homeomorphism between sequence spaces.

Elementary codings. Coordinate pairing gives the homeomorphisms $C ≅ C^{N}$ and $N ≅ N^{N}$ , so finite or countable tuples of the respective real codes may be folded into one code. The published map from $N$ is a homeomorphism only onto the subspace $D \subseteq C$ of sequences with infinitely many $1$ s; no homeomorphism $N ≅ C$ and no measure transport along that subspace map is asserted here. Adding a dummy final existential real quantifier shows that every $Σ_{2}^{1} (x)$ subset of $C$ is $Σ_{3}^{1} (x)$ : prefix a redundant $\exists w$ and ignore $w$ in $θ$ . This inclusion is the one used below when a $Σ_{3}^{1}$ -measurability hypothesis is applied to the $Σ_{2}^{1} (x)$ null-code order. The quantifier-prefix definition uses no choice. The measured interpretation above is used under Countable Choice, which licenses both the Borel coin-measure construction and its completion.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-22Open item page →

Rapid filters and the Raisonnier family

Definition

Work in ZF. Here increasing means nondecreasing unless strictly increasing is written, and $f (n)$ denotes the finite ordinal ${0, \dots, f (n) - 1}$ . A filter $F$ on $ω$ in the sense of Filter on a set extends the Fréchet filter when it contains every cofinite set. A filter extending the Fréchet filter is rapid when for every increasing $f : ω \to ω$ there is $a \in F$ with

$∣ a \cap f (n) ∣ \leq n for every n < ω .$

Uniform-bounding form. The rapidity condition is equivalent to the following one, whose uniformity is what later estimates use: there is a single strictly increasing $g : ω \to ω$ such that for every increasing $f : ω \to ω$ there is $a \in F$ with $∣ a \cap f (n) ∣ \leq g (n)$ for all $n$ . The forward direction takes $g (n) = n$ . For the converse, given $g$ and an increasing $f$ , apply the hypothesis to $f^{*} (n) = f (g (n + 1))$ to obtain $a \in F$ with $∣ a \cap f (g (n + 1)) ∣ \leq g (n)$ for all $n$ ; then for $k \in [g (n), g (n + 1))$ the monotonicity of $f$ gives $∣ a \cap f (k) ∣ \leq ∣ a \cap f (g (n + 1)) ∣ \leq g (n) \leq k$ , and replacing $a$ by $a^{*} = a ∖ f (g (0))$ , which preserves membership in $F$ because the Fréchet filter is contained in $F$ , gives the exact inequality $∣ a^{*} \cap f (k) ∣ \leq k$ for all $k$ (the values below $g (0)$ being empty). Rapidity is thus witnessed by a single bounding function.

First differing prefix lengths and the Raisonnier family. For distinct $u, v \in 2^{ω}$ let $h (u, v) = \min {n : u ↾ n \neq v ↾ n}$ be their first differing prefix length. If the first differing coordinate is $k$ , this length is $k + 1$ , because restriction to $n$ uses the coordinates strictly below $n$ . Thus $h (u, v) \geq 1$ . We retain this prefix-length convention from Ishii Definition 3.3 throughout $H$ and $F (x)$ . For $X \subseteq 2^{ω}$ put

$H (X) = {h (u, v) : u, v \in X, u \neq v} .$

The closure of a set does not change $H$ : if $u, v \in \overline{X}$ are distinct and $m = h (u, v)$ , the length- $m$ cylinders about $u, v$ each meet $X$ . Choose $u^{'}, v^{'}$ in these two intersections. Their prefixes agree below $m - 1$ and differ at $m - 1$ , so $h (u^{'}, v^{'}) = m$ . This proves $H (\overline{X}) \subseteq H (X)$ ; the reverse inclusion follows from $X \subseteq \overline{X}$ . Only two existential witnesses are used, not a sequence of choices.

For precision, if $x \in ω^{ω}$ is a real, use its graph as a set predicate in the relativized constructible hierarchy. For nonempty $A$ , ${Def}_{x} (A)$ consists of subsets of $A$ definable with finitely many parameters in $(A, \in, x \cap A)$ ; set ${Def}_{x} (\emptyset) = {\emptyset}$ . This is the predicate version of Definable subsets of a membership structure: uniform set satisfaction for the membership relation and one unary predicate is supplied by Existence and uniqueness of set satisfaction, and Separation and Replacement collect the subsets defined by the set of formula codes and finite tuples. Define $L_{0} [x] = \emptyset$ , $L_{α + 1} [x] = {Def}_{x} (L_{α} [x])$ and take unions at nonzero limits. Transfinite recursion constructs each set-length segment uniquely; uniqueness makes the segments agree, just as in The constructible hierarchy and constructible rank. Write $y \in L [x]$ for existence of an ordinal stage containing $y$ , a class predicate rather than a set union over all ordinals. With $L [x] \cap 2^{ω}$ viewed in Cantor sequence space, the Raisonnier family $F (x) \subseteq P (ω)$ is defined, for $a \subseteq ω$ , by

$a \in F (x) ⟺ there is a countable cover ⟨ F_{n} : n < ω ⟩ of L [x] \cap 2^{ω} with ⋃_{n < ω} H (F_{n}) \subseteq a .$

The cover members range over subsets of $2^{ω}$ ; replacing them by their closures does not change the union of the $H (F_{n})$ , so the witnessing covers may always be taken to consist of closed sets. Replacement forms the sequence of closures directly. The definition uses no choice; the later filter and rapidity assertions about $F (x)$ are proved separately from it.

LemmaStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

The Raisonnier family is a Sigma-one-three filter

Statement

Assume Countable Choice and $ω_{1}^{L [x]} = ω_{1}$ . Then $F (x)$ is a proper filter on $ω$ extending the Fréchet filter, and membership $a \in F (x)$ is a $Σ_{3}^{1} (x)$ property of the real $a$ .

Facts & Assumptions

Given: Countable Choice, a real $x$ with $ω_{1}^{L [x]} = ω_{1}$ , and the Raisonnier family $F (x)$ of the definition item.

[F1]

Rapid filters and the Raisonnier family: the definition of $F (x)$ by countable covers of $L [x] \cap 2^{ω}$ , the first-difference function $h$ , the set $H (X)$ , and the invariance $H (\overline{X}) = H (X)$ .

[F2]

Filter on a set: the filter axioms: upward closure, closure under intersections of two members, and properness.

[F3]

The relativized hierarchy of [F1] carries the coherent definition-code order obtained from The canonical definable global well-order of L. Countable well-founded level certificates show in ZF that $z \in L [x]$ is $Σ_{2}^{1} (x)$ , and canonical least codes of the $L [x]$ -countable ordinals inject $ω_{1}^{L [x]}$ into $L [x] \cap 2^{ω}$ ; both facts are proved where used below.

[F4]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) with Countable choice makes omega-one regular: Countable Choice makes $ω_{1}$ regular, and a countable union of countable sets is countable.

[F5]

Closed subsets of Baire space are tree bodies with Cantor and Baire sequence spaces and coordinate codings: closed subsets of the sequence spaces are bodies of trees, and a countable sequence of reals can be coded by a single real.

[F6]

Boldface Sigma-one-three measurability: the pointclass $Σ_{3}^{1} (x)$ and the fact that a $Σ_{2}^{1} (x)$ matrix preceded by one real existential is $Σ_{3}^{1} (x)$ .

Proof

1.1

Upward closure: if $a \in F (x)$ is witnessed by a cover $⟨ F_{n} ⟩$ and $a \subseteq b$ , the same cover witnesses $b \in F (x)$ .

F1F2

1.2

For later use, here is the choice-free relativized coding fact in [F3]. A real $p$ can code a well-founded extensional relation on $ω$ whose collapse is a correct countable level $L_{β} [x]$ containing a specified real $z$ . Well-foundedness is $Π_{1}^{1}$ , and the definition recursion, satisfaction relation and distinguished element checks are arithmetic. Every $z \in L [x] \cap ω^{ω}$ has such a certificate: take the canonical Skolem hull of $ω \cup {x, z}$ in a sufficiently large level and collapse it; least Skolem witnesses canonically enumerate the hull, so no choice is used. Conversely collapse and induction through the hierarchy make every certificate correct. Thus $z \in L [x]$ is $Σ_{2}^{1} (x)$ .

F1F3

2.1

Closure under intersections: if $a, b \in F (x)$ are witnessed by covers $⟨ F_{n}^{a} : n < ω ⟩$ , $⟨ F_{m}^{b} : m < ω ⟩$ , fix a bijection $π : ω \to ω \times ω$ and, for $π (k) = (n, m)$ , put $F_{k} : = F_{n}^{a} \cap F_{m}^{b}$ . These pairwise intersections cover $L [x] \cap 2^{ω}$ : for any $z$ in that set, choose $n$ and $m$ with $z \in F_{n}^{a}$ and $z \in F_{m}^{b}$ , and then $z \in F_{k}$ for the unique $k$ with $π (k) = (n, m)$ . Moreover $H (F_{k}) \subseteq H (F_{n}^{a}) \cap H (F_{m}^{b})$ , because a first difference of two points lying in the intersection is a first difference of points of each factor. Hence $⋃_{k} H (F_{k}) \subseteq a \cap b$ and $a \cap b \in F (x)$ .

F1step 1.1

2.2

By [F1] and [F5] replace each cover member by a closed body $[T_{n}]$ of a binary tree $T_{n} \subseteq 2^{< ω}$ and code the sequence by one real $y$ . Membership $a \in F (x)$ is equivalent to the existence of $y$ such that (i) every binary constructible real lies in some $[T_{n}]$ , that is, $\forall z \in 2^{ω} (z \in L [x] ⟶ z \in ⋃_{n} [T_{n}])$ , and (ii) every first difference of two points of one $[T_{n}]$ lies in $a$ . Using the certificate form from step 1.2, clause (i) is $Π_{2}^{1} (x)$ : universally quantify a binary real and a proposed certificate, and require either failure of its $Π_{1}^{1}$ certificate or membership in one tree body. Clause (ii) is $Π_{1}^{1}$ , not arithmetic: universally quantify two binary proposed branches and then check the arithmetic first-difference implication. It is therefore also $Π_{2}^{1}$ . Their conjunction preceded by the existential tree-sequence code $y$ is $Σ_{3}^{1} (x)$ in the sense of [F6].

F1F5F6step 1.2

3.1

For every $α < ω_{1}^{L [x]}$ , $L [x]$ contains a real coding a well-order of a subset of $ω$ of type $α$ : use the domain $α$ for finite $α$ (including the empty domain for $0$ ), and a bijective enumeration by $ω$ for infinite $α$ . Encode both the domain and the relation by binary coordinates using the fixed pairing. Choose the $<_{L [x]}$ -least such code; uniqueness gives an injection $α \mapsto c_{α}$ from $ω_{1}^{L [x]}$ into $L [x] \cap 2^{ω}$ without any simultaneous choice. Hence the Given equality makes $L [x] \cap 2^{ω}$ uncountable in the ambient universe. If $\emptyset \in F (x)$ , a witnessing cover would have $H (F_{n}) = \emptyset$ for every $n$ , so every $F_{n}$ would have at most one point; Countable Choice would make their union countable, contradicting that uncountability. Thus $F (x)$ is proper.

F1F3F4step 2.1

3.2

The Fréchet filter is contained in $F (x)$ : fix $n$ and let the cover consist of the $2^{n}$ cylinders $[s]$ , $s \in 2^{n}$ , padded by empty sets. Two distinct reals in one cylinder agree on the first $n$ coordinates, so their first differing coordinate is at least $n$ and their prefix length $h$ is at least $n + 1$ . In particular $⋃_{s} H ([s]) \subseteq {k : k \geq n} = ω ∖ n$ , so the cofinite set $ω ∖ n$ belongs to $F (x)$ . Together with the steps above this makes $F (x)$ a proper filter extending the Fréchet filter.

F1F2step 2.1

4.1

The steps above establish that $F (x)$ is a proper filter extending the Fréchet filter, and step 2.2 that membership is $Σ_{3}^{1} (x)$ ; this is the Statement.

step 3.2step 2.2∎

TheoremStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

Rapid filters are not Lebesgue measurable

Statement

Every rapid filter on $ω$ , regarded through characteristic functions as a subset of Cantor space with coin measure (and hence through the standard coding as a real set), is not Lebesgue measurable.

Facts & Assumptions

Given: A filter $F$ on $ω$ extending the Fréchet filter that is rapid in the sense of the definition item, viewed as ${χ_{a} : a \in F} \subseteq 2^{ω}$ .

[F1]

Rapid filters and the Raisonnier family: rapidity and its uniform-bounding form.

[F2]

Dyadic coding supplies coin measure and its completed Lebesgue transfer: the coin measure $ν$ on Cantor space, its completion, and the transfer to Lebesgue measure through the standard coding.

[F3]

Filter on a set: $F$ is upward closed, closed under intersections, and does not contain $\emptyset$ .

[F4]

Lebesgue density theorem: almost every point of a measurable set of positive measure is a density point, so for every measurable $B$ and $ε > 0$ the open set ${s : ν (B \cap [s]) > (1 - ε) ν ([s])}$ covers $B$ modulo a null set.

[F5]

Lambda-systems, or Dynkin systems with Dynkin's pi-lambda theorem: Dynkin's $π$ - $λ$ theorem, used for the zero-one law below. Countable additivity and continuity from below are part of [F2].

[F6]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): the ambient choice hypothesis of this page, used through [F2] and [F4].

Proof

1.1

Assume for contradiction that $F$ is measurable for the coin measure $ν$ . Since $F$ extends the Fréchet filter, it is closed under finite changes: if $a \in F$ and $a^{'}$ differs from $a$ only below $k$ , then $a \cap (ω ∖ k) \in F$ and is contained in $a^{'}$ , so $a^{'} \in F$ . Membership in $F$ therefore depends only on the coordinates at and above any fixed level $n$ .

assume-contraF3F6

1.2

To contradict nullity, fix an arbitrary closed $B \subseteq 2^{ω}$ with $ν (B) > 0$ . The density theorem supplies a finite nonempty family $T_{0}$ of binary strings such that every $s \in T_{0}$ satisfies $ν (B \cap [s]) > (1 - 2^{- 2}) ν ([s]) .$ For example, enumerate canonically the positive-length strings satisfying the display and take the first one whose cylinder meets $B$ . Put $n_{0} = \max {lh (s) : s \in T_{0}}$ .

2.1

Zero-one law: for each $n$ , the measurable tail event $F$ is independent of the sigma-algebra generated by the first $n$ coordinates. Hence the family of measurable $A$ satisfying $ν (F \cap A) = ν (F) ν (A)$ contains every finite-coordinate cylinder. It is a lambda-system, while the cylinders are a generating pi-system, so [F5] makes the family the whole Borel sigma-algebra and then its completion. Taking $A = F$ gives $ν (F) = ν (F)^{2}$ , hence $ν (F) \in {0, 1}$ .

F2F5step 1.1

2.2

Recursively, after finite nonempty $T_{i}$ and $n_{i}$ are fixed, let $S_{i}$ be the canonically enumerated set of strings $t$ with $lh (t) > n_{i}$ and $ν (B \cap [t]) > (1 - 2^{- (i + 3)}) ν ([t]) .$ The density theorem gives $ν (B ∖ ⋃_{t \in S_{i}} [t]) = 0$ . Let $T_{i + 1}$ be the first finite initial segment of this enumeration for which $ν (B ∖ ⋃_{t \in T_{i + 1}} [t]) < 2^{- (n_{i} + i + 2)},$ and put $n_{i + 1} = \max {lh (t) : t \in T_{i + 1}}$ . These choices are canonical, and every length in $T_{i + 1}$ exceeds $n_{i}$ , so $n_{0} < n_{1} < \dots$ .

F4step 1.2

3.1

The value is not one. The complement map $T (a) = ω ∖ a$ is measure preserving, and $T [F] \cap F = \emptyset$ : otherwise a filter would contain both $a$ and its complement and hence their empty intersection. If $ν (F) = 1$ , then $ν (T [F]) = 1$ , contradicting additivity. Thus the assumed measurable filter is null.

F2F3step 2.1

3.2

Apply rapidity to the increasing function $i \mapsto n_{i + 1}$ . There is $a \in F$ such that $∣ a \cap n_{i + 1} ∣ \leq i$ for every $i$ .

F1step 2.2

4.1

Choose any $s_{0} \in T_{0}$ whose cylinder meets $B$ ; the canonical first such member suffices. Recursively suppose $s_{i} \in T_{i}$ has been chosen and has value $1$ on every coordinate in $a \cap lh (s_{i})$ . Put $H_{i} = {z \in 2^{ω} : z (m) = 1 for every m \in a \cap [lh (s_{i}), n_{i + 1})} .$ The coordinates defining $H_{i}$ lie above those defining $[s_{i}]$ , so the two events are independent, and step 3.2 gives $ν (H_{i}) \geq 2^{- i}$ . The density bound for $s_{i}$ and $lh (s_{i}) \leq n_{i}$ therefore give $\begin{aligned} ν (H_{i} \cap [s_{i}] \cap B) & \geq ν (H_{i}) ν ([s_{i}]) - ν ([s_{i}] ∖ B) \\ > (2^{- i} - 2^{- (i + 2)}) 2^{- lh (s_{i})} \\ \geq 3 \cdot 2^{- (n_{i} + i + 2)} . \end{aligned}$ For $i = 0$ use the $T_{0}$ bound in step 1.2; for $i > 0$ the defining bound on $T_{i}$ in step 2.2 is exactly the displayed $2^{- (i + 2)}$ conditional error. The uncovered part of $B$ at level $T_{i + 1}$ has measure below $2^{- (n_{i} + i + 2)}$ , so choose $z_{i} \in H_{i} \cap [s_{i}] \cap B \cap ⋃_{t \in T_{i + 1}} [t]$ and then the canonical $s_{i + 1} \in T_{i + 1}$ with $z_{i} \in [s_{i + 1}]$ . Since both strings are initial segments of $z_{i}$ and $lh (s_{i + 1}) > n_{i} \geq lh (s_{i})$ , we have $s_{i} ⊊ s_{i + 1}$ ; the definition of $H_{i}$ preserves the induction invariant.

step 1.2step 2.2step 3.2

5.1

Let $b = ⋃_{i} s_{i}$ . The points $z_{i} \in B$ converge to $b$ , because both $z_{i}$ and $b$ extend $s_{i + 1}$ and the string lengths tend to infinity; closedness gives $b \in B$ . The induction invariant and unbounded lengths give $a \subseteq b$ , so $b \in F$ by upward closure. Thus every closed positive-set $B$ meets $F$ .

F3step 4.1

6.1

Hence $F$ has positive outer measure: if it had outer measure zero, an open $O \supseteq F$ with $ν (O) < 1$ would have a closed positive complement missing $F$ , contrary to step 5.1. This contradicts $ν (F) = 0$ from step 3.1. The assumption of measurability is false, and [F2] transfers the conclusion to Lebesgue measure under the standard coding.

discharge-contradictionF2step 3.1step 5.1∎

LemmaStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

A measurable null-code order bounds the constructible null union

Statement

For a real $x$ define $A (x)$ on pairs $(u, v)$ by comparing the least canonical $L [x]$ null $G_{δ}$ codes containing $u$ and $v$ . Then $A (x)$ is $Σ_{2}^{1} (x)$ . Under Countable Choice, if $A (x)$ is measurable, the union $G$ of all null Borel sets coded in $L [x]$ is null in the ambient universe.

Facts & Assumptions

Given: A real $x$ , the completed coin measure $ν$ on $2^{ω}$ , and the family of null $G_{δ}$ subsets of $2^{ω}$ coded in $L [x]$ .

[F1]

Rapid filters and the Raisonnier family supplies the predicate construction of the hierarchy $L [x]$ . The coherent definition-code recursion of The canonical definable global well-order of L applies verbatim with the additional predicate $x$ , producing the canonical setlike order $<_{L [x]}$ ; the countable-level and predecessor certificates needed below are proved in steps 1.1--2.1 rather than inferred from the unrelativized theorem.

[F2]

Boldface Sigma-one-three measurability supplies the projective pointclass convention and, under Countable Choice, the completed Borel coin probability used by the measurability hypothesis.

[F3]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): countable unions of null sets are null. It is also the hypothesis of the completed-product Fubini theorem used below.

[F4]

Tonelli and Fubini for the completed product, with only almost-everywhere section measurability: Fubini for the completed product measure: a measurable subset of $2^{ω} \times 2^{ω}$ whose horizontal sections are almost all null has null vertical-section set, and almost every vertical section of a null measurable set is null.

Proof

1.1

Relativize the definition-code recursion of [F1] to the structures $(L_{α} [x], \in, x \cap L_{α} [x])$ . It gives a coherent setlike well-order $<_{L [x]}$ whose levels are initial segments. Every real $d \in L [x]$ belongs to a countable level: inside $L [x]$ , close $ω \cup {x, d}$ under the canonically least Skolem witnesses of a sufficiently large level. Formula codes and finite tuples canonically enumerate this hull, so no ambient choice is used; collapsing it and inducting through the relativized definition operation gives some countable $L_{β} [x]$ containing $d$ . Consequently the real predecessors of $d$ are countable and all occur in one such level.

F1construct

2.1

A real $e$ can therefore certify that it enumerates exactly ${c \in ω^{ω} : c <_{L [x]} d}$ : it codes a well-founded extensional relation on $ω$ , its collapse as a correct countable $L_{β} [x]$ containing $d$ , the canonical order computed there, and the enumerated predecessor segment. Well-foundedness is $Π_{1}^{1}$ ; extensionality, the staged definition recursion, countable satisfaction and the displayed enumeration check are arithmetic in the code. Thus the certificate predicate ${Pred}_{x} (d, e)$ is $Π_{1}^{1} (x)$ , and $c \in L [x]$ has the analogous form $\exists q {Lev}_{x} (c, q)$ with ${Lev}_{x}$ $Π_{1}^{1} (x)$ . Correctness follows by collapse and induction on the coded hierarchy; completeness of the predecessor list follows from the initial-segment property in step 1.1. This is the choice-free relativized certificate behind the standard $Σ_{2}^{1} (x)$ facts in the cited sources.

F1step 1.1

2.2

Put $G$ equal to the union of the null $G_{δ}$ sets having codes in $L [x]$ . For $u \in G$ , let $d (u)$ be the $<_{L [x]}$ -least such code containing $u$ , and let $ξ (u)$ be its position among the null codes. Disjointifying by least code gives null layers ${\tilde{G}}_{ξ}$ with $G = ⋃_{ξ} {\tilde{G}}_{ξ}$ .

F1step 1.1

3.1

Define $A (x) = {(u, v) \in G \times G : ξ (u) < ξ (v)}$ . Equivalently, $(u, v) \in A (x)$ iff there are reals $c, d, e, q$ such that ${Lev}_{x} (c, q)$ and ${Pred}_{x} (d, e)$ hold, $c$ codes a null $G_{δ}$ containing $v$ , $d$ codes one containing $u$ but not $v$ , and no code enumerated by $e$ codes a null $G_{δ}$ containing $v$ . Indeed these conditions say $d <_{L [x]} d (v)$ while $d$ contains $u$ ; conversely take $d = d (u)$ and $c = d (v)$ . In particular the formula is false off $G \times G$ and on the diagonal.

step 2.1step 2.2

4.1

In the formula of step 3.1, the four real witnesses may be folded into one. The two certificate predicates are $Π_{1}^{1} (x)$ by step 2.1, while recognition and interpretation of the explicit null- $G_{δ}$ codes and the bounded checks through $e$ are arithmetic. A leading existential real followed by this $Π_{1}^{1}$ matrix is $Σ_{2}^{1} (x)$ in the convention of [F2].

F2step 2.1step 3.1

4.2

For $v \in G$ , the horizontal section $A (x)^{v} = {u : ξ (u) < ξ (v)}$ is the union of the null sets coded by the predecessor list for $d (v)$ from step 2.1, hence is null by Countable Choice. For $v \notin G$ the section is empty. Thus every horizontal section is completed-measurable and null.

F3step 2.1step 3.1

5.1

Assume $A (x)$ is measurable for the completed product coin measure. Tonelli applied to its indicator and step 4.2 makes $A (x)$ product-null. The completed Fubini theorem then supplies a completed-measurable null set $Z$ such that for every $u \notin Z$ the vertical section $A (x)_{u}$ is measurable and null. No measure is assigned to exceptional vertical sections.

F4step 4.2

6.1

If $G \subseteq Z$ , then $G$ is null. Otherwise choose $u \in G ∖ Z$ . The lower section $A (x)^{u}$ is null by step 4.2, the middle layer ${\tilde{G}}_{ξ (u)}$ lies in one null $G_{δ}$ , and the upper section $A (x)_{u}$ is null by step 5.1. Since $G = A (x)^{u} \cup {\tilde{G}}_{ξ (u)} \cup A (x)_{u}$ , the finite union is null. This dichotomy never presupposes measurability of $G$ .

F3step 4.2step 5.1

7.1

The steps above prove the complexity and the nullity conclusion, which is the Statement.

step 4.1step 6.1∎

LemmaStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

Uniform null G-delta sets capture block functions

Statement

There are uniformly assigned null $G_{δ}$ sets $N_{f}$ in Cantor space for $f \in ω^{ω}$ and, for each open $U$ whose canonical coin content is below one, finite capture sets $φ_{U} (n)$ of size at most $2^{n + 1}$ , such that $N_{f} \subseteq U$ implies $f (n) \in φ_{U} (n)$ for all sufficiently large $n$ . If $f$ belongs to a transitive model, the code for $N_{f}$ belongs to that model.

Facts & Assumptions

Given: Cantor space $2^{ω}$ .

[F1]

Cantor and Baire sequence spaces and coordinate codings: the cylinder topology, compactness of Cantor space, coordinate pairing and explicit natural-number codes for finite binary words. The choice-free coin content needed here is constructed in step 1.1.

[F2]

The countable Borel hierarchy and its limit convention: the $G_{δ}$ form of a countable intersection of open sets.

[F3]

Closed subspaces of complete metric spaces are complete; the converse under countable choice and [F1]: a closed subspace of Cantor space is complete; choosing the lexicographically least branch through each nonempty cylinder trace supplies a canonical countable dense subset. Hence Separable complete metric spaces are Baire in ZF makes every nonempty closed $K \subseteq 2^{ω}$ a Baire space in ZF.

Proof

1.1

For an open $O \subseteq 2^{ω}$ , let $P_{O}$ be the prefix-free set of shortest finite words $s$ with $[s] \subseteq O$ , and put $ν (O) = \sum_{s \in P_{O}} 2^{- ∣ s ∣}$ , the supremum of its finite partial sums in the fixed word order. Define the closed content $m (K) = 1 - ν (2^{ω} ∖ K)$ and call $E$ null when, for every $k$ , it has an open cover of content below $2^{- k}$ . Refining finitely many cylinders to one common length proves finite additivity on clopen sets, monotonicity, and countable subadditivity for open unions directly from binary-word counts. If $K \subseteq D$ with $K$ closed and $D$ clopen, then $m (K) \leq ν (D)$ . Every definition uses a fixed enumeration or a real supremum and hence exists in ZF.

F1construct

2.1

Using the canonical pairing from [F1], put $C_{n, m} = {⟨ ⟨ n, m ⟩, j ⟩ : j \leq n}$ and $B_{n, m} = {x : \forall c \in C_{n, m} x (c) = 1}$ . The coordinate groups are disjoint and have size $n + 1$ . Refining to a prefix above the finitely many coordinates shows $ν (B_{n, m}) = 2^{- (n + 1)}, ν (⋂_{(n, m) \in J} B_{n, m}^{c}) = \prod_{(n, m) \in J} (1 - 2^{- (n + 1)})$ for every finite $J$ ; this is a finite pattern count, not a product-measure theorem.

F1step 1.1

2.2

Fix open $U$ with $ν (U) < 1$ and put $K_{0} = 2^{ω} ∖ U$ , so $m (K_{0}) > 0$ . Enumerate the finite words as $(s_{i})$ . Let $Z$ be the union of those traces $K_{0} \cap [s_{i}]$ with closed content zero. Such a compact zero-content trace has, for each requested rational error, a finite clopen cover of smaller content: choose a finite clopen subset of its open complement whose content is sufficiently close to one and take the complement. Choose the least finite cover in the fixed code order. Assigning error $2^{- i - k - 2}$ to the pair $(i, k)$ and taking the open union proves directly that $Z$ is null, without Countable Choice. Put $K = K_{0} ∖ Z$ . The set $Z$ is $K_{0}$ intersected with the open union of the corresponding cylinders, so $K$ is closed. Monotonicity gives $m (K) \leq m (K_{0})$ , while the arbitrarily small canonical open covers of $Z$ and the finite/open content inequalities give $m (K_{0}) \leq m (K) + ε$ for every positive rational $ε$ ; hence $m (K) = m (K_{0}) > 0$ . Every nonempty trace $K \cap [s]$ has positive closed content, since otherwise the corresponding $K_{0} \cap [s]$ was removed.

F1step 1.1

3.1

For $f : ω \to ω$ put $N_{f} = ⋂_{k < ω} ⋃_{n \geq k} B_{n, f (n)}$ . It is $G_{δ}$ by [F2]. For every $k$ , its displayed tail union is an open cover of content at most $\sum_{n \geq k} 2^{- (n + 1)} = 2^{- k}$ by step 1.1, so $N_{f}$ is null by the local definition. The assignment is arithmetic in $f$ and the fixed blocks; therefore its code belongs to every transitive model containing $f$ .

F2step 1.1step 2.1

3.2

For $s \in T_{K} = {s : [s] \cap K \neq \emptyset}$ put $A_{s} (n) = {m : K \cap [s] \cap B_{n, m} = \emptyset}$ . For every finite $J \subseteq {(n, m) : m \in A_{s} (n)}$ , steps 1.1--2.2 give $0 < m (K \cap [s]) \leq \prod_{(n, m) \in J} (1 - 2^{- (n + 1)}) \leq \exp (- \sum_{(n, m) \in J} 2^{- (n + 1)}) .$ Taking canonical finite initial subsets shows that $\sum_{n} ∣ A_{s} (n) ∣ / 2^{n + 1}$ converges. Hence every $A_{s} (n)$ is finite and $∣ A_{s} (n) ∣ / 2^{n + 1} \to 0$ .

step 1.1step 2.1step 2.2

4.1

Assume $N_{f} \subseteq U$ , so $K \cap N_{f} = \emptyset$ . If every $K \cap ⋃_{n \geq m} B_{n, f (n)}$ met every nonempty basic open subset of $K$ , these sets would be dense open. The least-branch construction in [F3] makes $K$ separable and complete in ZF, so the Baire theorem would make their intersection $K \cap N_{f}$ nonempty. Therefore some $s \in T_{K}$ and $m$ satisfy $K \cap [s] \cap ⋃_{n \geq m} B_{n, f (n)} = \emptyset$ .

F3step 2.2step 3.1

4.2

Let $i : 2^{< ω} \to ω$ be the fixed bijection, and let $n (s)$ be the least threshold after which $∣ A_{s} (n^{'}) ∣ / 2^{n^{'} + 1} \leq 2^{- i (s) - 1}$ . Put $φ_{U} (n) = ⋃ {A_{s} (n) : s \in T_{K}, n (s) \leq n}$ . For any finite $E \subseteq φ_{U} (n)$ , assign to each $m \in E$ the least witnessing $s$ in the fixed word order. Then $\frac{∣ E ∣}{2^{n + 1}} \leq \sum_{s : n (s) \leq n} \frac{∣ A_{s} (n) ∣}{2^{n + 1}} \leq \sum_{s} 2^{- i (s) - 1} \leq 1.$ If $φ_{U} (n)$ had more than $2^{n + 1}$ elements, its first $2^{n + 1} + 1$ elements would contradict this bound. Thus it is finite and has the required size.

F1step 3.2

5.1

With $s, m$ as in step 4.1 and $ℓ = \max {m, n (s)}$ , every $n \geq ℓ$ satisfies $K \cap [s] \cap B_{n, f (n)} = \emptyset$ , hence $f (n) \in A_{s} (n) \subseteq φ_{U} (n)$ . Together with steps 3.1 and 4.2 this proves capture, the size bound and model-membership of the codes.

step 3.1step 4.1step 4.2

6.1

The steps above provide the uniformly assigned null $G_{δ}$ sets and the capture sets with all stated properties, which is the Statement.

step 3.1step 5.1∎

TheoremStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

Uniform null-code measurability makes the Raisonnier filter rapid

Statement

Assume Countable Choice and $ω_{1}^{L [x]} = ω_{1}$ . Suppose moreover that for every real $r$ , the null-code order $A (x \oplus r)$ is measurable, where $x \oplus r$ is the usual interleaving join. Then the Raisonnier filter $F (x)$ is rapid. In particular, boldface $Σ_{2}^{1}$ measurability supplies this uniform hypothesis.

Facts & Assumptions

Given: Countable Choice, a real $x$ with $ω_{1}^{L [x]} = ω_{1}$ , and measurability of $A (x \oplus r)$ for every real $r$ .

[F1]

A measurable null-code order bounds the constructible null union: for every real $y$ , measurability of $A (y)$ makes the union of all null Borel sets coded in $L [y]$ null in the ambient universe.

[F2]

Uniform null G-delta sets capture block functions: the uniformly assigned null $G_{δ}$ sets $N_{f}$ for $f \in ω^{ω}$ and the finite capture sets $φ_{U} (n)$ of size at most $2^{n + 1}$ with $N_{f} \subseteq U$ implying $f (n) \in φ_{U} (n)$ eventually; codes of $N_{f}$ lie in any transitive model containing $f$ .

[F3]

Rapid filters and the Raisonnier family: the definition of $F (z)$ by covers of $L [z] \cap 2^{ω}$ , for any real $z$ , and the uniform-bounding form of rapidity.

[F4]

The Raisonnier family is a Sigma-one-three filter: $F (x)$ is a filter; in particular it is upward closed.

[F5]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) and Assuming countable choice, Borel probability measures on Polish spaces are inner regular: under Countable Choice, if $Z$ is a Borel null set in Cantor space, inner regularity applied to $2^{ω} ∖ Z$ gives a compact $K \subseteq 2^{ω} ∖ Z$ of positive measure; then $U = 2^{ω} ∖ K$ is an open superset of $Z$ with $ν (U) < 1$ .

Proof

1.1

Fix an arbitrary strictly increasing sequence $⟨ n_{i} : i < ω ⟩$ of natural numbers and let $r$ code this sequence. Put $y = x \oplus r$ and $M = L [y]$ . Since $L [x] \subseteq M \subseteq V$ , the inequalities $ω_{1}^{L [x]} \leq ω_{1}^{M} \leq ω_{1}$ and the Given equality show that $ω_{1}^{M} = ω_{1}$ . For $f \in M \cap 2^{ω}$ put $\overset{ˉ}{f} (i) = f ↾ n_{i}$ , using the canonical natural-number code for the finite word. Both $f$ and the sequence $⟨ n_{i} ⟩$ belong to $M$ , so $\overset{ˉ}{f} \in M$ and [F2] puts the code of $N_{\overset{ˉ}{f}}$ in $M$ .

givenF2

1.2

By the uniform measurability hypothesis, $A (y)$ is measurable. Hence [F1] makes the union of all null Borel sets coded in $M = L [y]$ null, and that union contains every $N_{\overset{ˉ}{f}}$ from step 1.1. By the definition of the completed coin measure, the union is contained in a Borel null set $Z$ . Apply [F5] to $2^{ω} ∖ Z$ and choose a compact $K$ there with $ν (K) > 0$ ; then $U = 2^{ω} ∖ K$ is open, contains the union, and has $ν (U) < 1$ . For every $f \in M \cap 2^{ω}$ there is $i_{f}$ such that $f ↾ n_{i} = \overset{ˉ}{f} (i) \in φ_{U} (i)$ for all $i \geq i_{f}$ , by [F2]'s capture clause.

givenstep 1.1F1F2F5

2.1

Let $Ψ_{i}$ be the elements of $φ_{U} (i)$ that decode binary strings of length $n_{i}$ . Define $a \subseteq ω$ by declaring $k \in a$ iff, for $i = \min {j : k \leq n_{j}}$ , there are distinct $s, t \in Ψ_{i}$ whose first differing prefix length $h (s, t)$ is $k$ . Thus the positive lengths in the block $(n_{i - 1}, n_{i}]$ , with $n_{- 1} : = 0$ , are assigned to level $i$ , exactly as required by the prefix-length convention of [F3].

F2F3step 1.2

3.1

The values assigned to level $i$ lie in $(n_{i - 1}, n_{i}]$ and are the first-difference prefix lengths realized by pairs from $Ψ_{i}$ . If a finite set of equal-length binary strings has $k \geq 1$ members, its prefix tree has at most $k - 1$ branching levels; if $k = 0$ , it realizes no first differences. Thus level $i$ contributes at most $\max {∣ Ψ_{i} ∣ - 1, 0} \leq 2^{i + 1} - 1$ values. In particular, even with the harmless overcount of a possible endpoint $n_{i}$ , $∣ a \cap n_{i} ∣ \leq \sum_{j \leq i} (2^{j + 1} - 1) \leq 2^{i + 2} - 2.$

F2step 2.1

3.2

For $k < ω$ and $s \in 2^{n_{k}}$ put $F_{k, s} = {f \in M \cap 2^{ω} : f ↾ n_{k} = s and f ↾ n_{i} \in Ψ_{i} for every i \geq k} .$ These countably many sets cover $M \cap 2^{ω}$ by step 1.2. If distinct $f, g \in F_{k, s}$ and $i$ is least with $f ↾ n_{i} \neq g ↾ n_{i}$ , then $i > k$ , both length- $n_{i}$ prefixes lie in $Ψ_{i}$ , and their first differing prefix length equals $h (f, g)$ and lies in $(n_{i - 1}, n_{i}]$ . Thus $h (f, g) \in a$ by step 2.1, so $H (F_{k, s}) \subseteq a$ . The cover therefore witnesses $a \in F (y)$ . Since $L [x] \cap 2^{ω} \subseteq L [y] \cap 2^{ω}$ , the same cover also witnesses $a \in F (x)$ .

F3F4step 1.2step 2.1

4.1

Given the arbitrary strictly increasing sequence $⟨ n_{i} ⟩$ , step 3.2 produced $a \in F (x)$ with $∣ a \cap n_{i} ∣ \leq 2^{i + 2} - 2 < 2^{i + 2}$ for every $i$ . The same conclusion for a merely nondecreasing sequence follows by replacing it with a pointwise larger strictly increasing one. Since $i \mapsto 2^{i + 2}$ is one fixed bound, the uniform-bounding form of [F3] makes $F (x)$ rapid.

F3step 3.1step 3.2

5.1

The steps above establish the rapidity of $F (x)$ under the stated hypotheses; this is the Statement.

step 4.1∎

LemmaStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

Failure of inaccessibility in L produces a real with correct omega-one

Statement

Work in ZF+Countable Choice. If the ambient $ω_{1}$ is not an inaccessible cardinal of $L$ , then there is a real $x$ such that $ω_{1}^{L [x]}$ equals the ambient $ω_{1}$ .

Facts & Assumptions

Given: Countable Choice and the hypothesis that the ambient $ω_{1}$ is not inaccessible in $L$ .

[F1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) with Countable choice makes omega-one regular: Countable Choice makes the ambient $ω_{1}$ regular, and every countable subset of $ω_{1}$ is bounded.

[F2]

The generalized continuum hypothesis holds in L: $L$ satisfies GCH, so inside $L$ the power-set operation is the cardinal successor and $2^{ℵ_{0}} = ℵ_{1}$ .

[F3]

Absoluteness, idempotence and minimality of L: constructibility is absolute between the relevant transitive models with the same ordinals, and $L \subseteq L [x] \subseteq V$ . No preservation of $L$ -cardinals in $V$ is asserted: in fact, every ordinal below the ambient $ω_{1}$ is countable in $V$ .

[F4]

Inaccessible and Mahlo cardinals: a cardinal is inaccessible when it is uncountable, regular and a strong limit.

Proof

1.1

The ambient $ω_{1}$ is regular by Countable Choice, and it is a cardinal in $L$ : an $L$ -definable surjection from a smaller ordinal onto $ω_{1}$ would still be a surjection in the universe. It is also regular in $L$ , since an $L$ -cofinal map from a smaller ordinal would remain cofinal in the universe.

F1F3

2.1

Hence, if $ω_{1}$ is not inaccessible in $L$ , it fails one of the three clauses of [F4] there. It is uncountable in $L$ (it is uncountable in the universe and $L$ has the same ordinals) and regular in $L$ by step 1.1, so it is not a strong limit cardinal of $L$ : there is a cardinal $μ < ω_{1}$ of $L$ with $(2^{μ})^{L} \geq ω_{1}$ . By GCH in $L$ , $(2^{μ})^{L} = μ^{+}$ , so the ordinal $ω_{1}$ equals $(μ^{+})^{L}$ for some $L$ -cardinal $μ < ω_{1}$ . This $μ$ is infinite, since the $L$ -successor of a finite cardinal is finite whereas the ambient $ω_{1}$ is uncountable.

F2F4step 1.1

3.1

The ordinal $μ$ is countable in the ambient universe because $μ < ω_{1}$ , so there exists a real $x$ coding a bijection $b : ω \to μ$ . This is one existential choice from a nonempty set of codes and needs no family-choice principle.

F1step 2.1

4.1

Let $β < (μ^{+})^{L} = ω_{1}$ . If $β = 0$ , it is countable in $L [x]$ trivially. If $β > 0$ , then Choice in $L$ and the fact that $μ$ is an infinite $L$ -cardinal imply that $L$ contains a surjection from $μ$ onto $β$ ; this map also belongs to $L [x]$ by [F3]. Composing it with the bijection $b$ coded by $x$ makes $β$ countable in $L [x]$ . Thus every ordinal below the ambient $ω_{1}$ is countable in $L [x]$ , so $ω_{1}^{L [x]} \geq ω_{1}$ . Conversely the ambient $ω_{1}$ is uncountable in $L [x]$ , since any bijection with $ω$ in $L [x] \subseteq V$ would contradict its ambient definition; hence $ω_{1}^{L [x]} \leq ω_{1}$ . Therefore equality holds.

F2F3step 2.1step 3.1

5.1

The steps above produce a real $x$ with $ω_{1}^{L [x]} = ω_{1}$ from the failure of inaccessibility in $L$ ; only this existential real is claimed, not the statement for every real.

step 4.1∎

TheoremStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

Sigma-one-three measurability makes omega-one inaccessible in L

Statement

Assume ZF+Countable Choice and boldface $Σ_{3}^{1}$ measurability. Then the ambient $ω_{1}$ is an inaccessible cardinal in $L$ .

Facts & Assumptions

Given: Countable Choice and the hypothesis that every $Σ_{3}^{1} (x)$ set of reals is Lebesgue measurable for every real $x$ .

[F1]

Boldface Sigma-one-three measurability: the pointclass $Σ_{3}^{1} (x)$ , the inclusion of $Σ_{2}^{1} (x)$ in $Σ_{3}^{1} (x)$ by a dummy real quantifier, and the definition of boldface measurability.

[F2]

Failure of inaccessibility in L produces a real with correct omega-one: failure of inaccessibility of the ambient $ω_{1}$ in $L$ yields a real $x$ with $ω_{1}^{L [x]} = ω_{1}$ .

[F3]

A measurable null-code order bounds the constructible null union: the null-code order $A (x)$ is $Σ_{2}^{1} (x)$ , and its measurability makes the union of the constructible null Borel sets null.

[F4]

Uniform null-code measurability makes the Raisonnier filter rapid: under Countable Choice, $ω_{1}^{L [x]} = ω_{1}$ and measurability of $A (x \oplus r)$ for every real $r$ , the filter $F (x)$ is rapid.

[F5]

The Raisonnier family is a Sigma-one-three filter: $F (x)$ is a $Σ_{3}^{1} (x)$ subset of the reals.

[F6]

Rapid filters are not Lebesgue measurable: rapid filters are not Lebesgue measurable.

[F7]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): the ambient choice hypothesis.

Proof

1.1

Assume, for contradiction, that the ambient $ω_{1}$ is not an inaccessible cardinal of $L$ , and let $x$ be a real with $ω_{1}^{L [x]} = ω_{1}$ , as supplied by [F2].

assume-contraF2

2.1

For every real $r$ , the null-code order $A (x \oplus r)$ is $Σ_{2}^{1} (x \oplus r)$ by [F3]. By [F1] it is $Σ_{3}^{1} (x \oplus r)$ , so the boldface measurability hypothesis makes $A (x \oplus r)$ measurable. Thus the uniform hypothesis of [F4] holds, not merely its instance at $r = 0$ .

F1F3step 1.1

3.1

By [F4], applied with Countable Choice [F7], $ω_{1}^{L [x]} = ω_{1}$ and the uniform conclusion of step 2.1, the Raisonnier filter $F (x)$ is rapid.

F4F7step 2.1

4.1

By [F5] the filter $F (x)$ is a $Σ_{3}^{1} (x)$ set of reals, and by [F6] it is not Lebesgue measurable. This contradicts the hypothesis that every $Σ_{3}^{1} (x)$ set is measurable.

F5F6step 3.1

5.1

The contradiction in step 4.1 refutes the assumption of step 1.1, so the ambient $ω_{1}$ is inaccessible in $L$ .

discharge-contradictionstep 4.1∎

TheoremStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

All-real-set measurability yields an inaccessible inner model

Statement

If a universe satisfies ZF+DC and every set of reals is Lebesgue measurable, then its constructible universe $L$ satisfies ZFC and contains an inaccessible cardinal — indeed the ambient $ω_{1}$ is inaccessible in $L$ . Consequently the assumed universe has a definable inner model of ZFC with an inaccessible cardinal. No arithmetized consistency implication is asserted by this item.

Facts & Assumptions

Given: A universe $V$ with ZF+DC in which every set of reals is Lebesgue measurable.

[F1]

AC implies DC implies countable choice: DC implies Countable Choice.

[F2]

Boldface Sigma-one-three measurability: boldface $Σ_{3}^{1}$ measurability means that every $Σ_{3}^{1} (x)$ set is Lebesgue measurable for every real $x$ ; universal measurability of all real sets immediately implies it, since every $Σ_{3}^{1} (x)$ set is a set of reals.

[F3]

Sigma-one-three measurability makes omega-one inaccessible in L: under ZF+Countable Choice and boldface $Σ_{3}^{1}$ measurability, the ambient $ω_{1}$ is inaccessible in $L$ .

[F4]

Semantic and formal inner-model theorem for L with The constructible universe satisfies AC: for each fixed ZFC axiom, ZF proves that axiom relativized to its constructible class $L$ ; in particular the ambient ZF universe proves internally that $L$ satisfies ZFC. The separate external set-model clause of the first supplier is not applied to the proper class $V$ .

[F5]

Inaccessible and Mahlo cardinals: the definition of inaccessibility, so that the same ordinal certified in [F3] is verified to be uncountable, regular and a strong limit inside $L$ .

Proof

1.1

DC implies Countable Choice by [F1], so the choice hypothesis of [F3] holds in $V$ .

1.2

Every set of reals is measurable, hence every $Σ_{3}^{1} (x)$ set is measurable for every real $x$ by [F2]; thus $V$ satisfies boldface $Σ_{3}^{1}$ measurability.

2.1

By [F3] the ambient $ω_{1}$ is inaccessible in $L$ .

F3step 1.1step 1.2

3.1

Apply the fixed-axiom relativization clause of [F4] inside the given ambient ZF universe. It proves that its definable constructible class $L$ satisfies every ZFC axiom. Step 2.1 already says that the ambient $ω_{1}$ , viewed as an ordinal of $L$ , is inaccessible there; equivalently [F5] verifies inside $L$ that it is uncountable, regular and a strong limit. Hence $L ⊨$ "there is an inaccessible cardinal".

F4F5step 2.1

4.1

The steps above give the semantic conclusion that the ambient $ω_{1}$ is inaccessible in the definable inner model $L ⊨ Z F C$ . The formal-inner-model supplier [F4] expressly supplies no arithmetized consistency transfer, so this proof stops at that exact conclusion.

step 2.1step 3.1F4∎

TheoremStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

Exact equiconsistency of universal measurability and an inaccessible

Statement

ZFC plus an inaccessible cardinal and ZF+DC plus every set of reals Lebesgue measurable are equiconsistent. The same lower bound already follows from universal boldface $Σ_{3}^{1}$ measurability under Countable Choice.

Facts & Assumptions

Given: Fixed arithmetizations of the two theories and their finite fragments.

[F1]

Solovay-model regularity is consistent relative to an inaccessible cardinal: by the externally indexed finite-fragment transfer for the Lévy-collapse construction, $Con (Z F C + an inaccessible) ⟹ Con (Z F + D C + universal LM) .$ No uniform arithmetic proof-code transformer is used in that theorem.

[F2]

All-real-set measurability yields an inaccessible inner model: from ZF+DC plus universal measurability, the constructible universe satisfies ZFC and contains an inaccessible cardinal. Relativization to that definable inner model is an interpretation, so it sends every actual finite target refutation to a source refutation (Interpretation transports derivations and inconsistency).

[F3]

Under ZF+Countable Choice plus universal boldface $Σ_{3}^{1}$ measurability, the ambient $ω_{1}$ is inaccessible in $L$ (Sigma-one-three measurability makes omega-one inaccessible in L, The Axiom of Countable Choice ( ${A C}_{ω}$ ), Boldface Sigma-one-three measurability), and $L$ satisfies ZFC (Semantic and formal inner-model theorem for L). Relativization to $L$ therefore gives the same refutation translation as in [F2] (Interpretation transports derivations and inconsistency).

Proof

1.1

Upper bound: assume $Con (Z F C + inaccessible)$ . The exact external finite-fragment consistency implication in [F1] yields $Con (Z F + D C + every set of reals is Lebesgue measurable)$ .

1.2

Lower bound: assume $Con (Z F + D C + universal LM)$ . If ZFC plus an inaccessible had an actual refutation, [F2] would translate it to a refutation of the assumed source theory. Hence $Con (Z F C + inaccessible)$ follows.

1.3

The refinement: if ZF+Countable Choice plus boldface $Σ_{3}^{1}$ measurability is consistent, an actual refutation of ZFC plus an inaccessible would translate by [F3] to a refutation of that source theory. Thus its consistency already implies the consistency of ZFC plus an inaccessible cardinal. This is the stronger form of the lower bound stated.

1.4

The inaccessible hypothesis is needed only on the Solovay branch: steps 1.1 uses it, and steps 1.2 and 1.3 use none; the separation of the two branches is the point of this pair.

F1F2F3

2.1

Steps 1.1 through 1.3 give the two consistency implications in both directions, and step 1.4 records the exact role of the inaccessible; this is the Statement.

step 1.1step 1.2step 1.3∎

TheoremStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

Shelah's model separates universal Baire property from universal measurability

Statement

Relative to $Con (Z F C)$ , it is consistent that ZF+DC holds, every set of reals has the Baire property, and not every set of reals is Lebesgue measurable. Thus universal Baire property does not entail universal Lebesgue measurability over ZF+DC.

Facts & Assumptions

Given: The model-theoretic assumption $Con (Z F C)$ and Shelah's published relative-consistency construction.

[F1]

Absoluteness, idempotence and minimality of L is a theorem of ZF. Its external comparison clause assumes transitivity, but the theorem itself may be evaluated inside any first-order model of ZF. In particular, internally, a definable transitive inner class with all ordinals computes the same $L$ as its ambient model. No external transitivity of the model used below is inferred.

[F2]

Inaccessible and Mahlo cardinals defines inaccessibility, while An inaccessible rank segment models ZFC proves in ZFC that $V_{κ}$ models ZFC when $κ$ is inaccessible and that inaccessibility below $κ$ is absolute to that rank segment. This theorem too can be interpreted internally in an arbitrary first-order model.

[F3]

Shelah's CH-length homogeneous sweet construction constructs the required forcing over every ZFC+CH ground. When the ground also satisfies $V = L$ , Every real set in the Shelah inner model has the Baire property proves at the exact homogeneity and Borel-to-open interfaces that the resulting $N = H O D (S)$ has universal Baire property. The exact equiconsistency of ZFC and the all-Baire-property model is used only for the published metatheoretic comparison, not as the construction interface.

[F4]

The Shelah inner model satisfies ZF and Dependent Choice: $N$ has the same ordinals and reals as the extension and satisfies ZF+DC.

[F5]

Failure of inaccessibility in L produces a real with correct omega-one: in ZF+Countable Choice, if the ambient $ω_{1}$ is not inaccessible in its constructible universe, there is a real $x$ with $ω_{1}^{L [x]} = ω_{1}$ .

[F6]

Uniform null-code measurability makes the Raisonnier filter rapid: under Countable Choice and $ω_{1}^{L [x]} = ω_{1}$ , measurability of every $A (x \oplus r)$ , for all reals $r$ , makes $F (x)$ rapid.

[F7]

The Raisonnier family is a Sigma-one-three filter and Rapid filters are not Lebesgue measurable: $F (x)$ is a set of reals, and if rapid it is not Lebesgue measurable. Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain) implies Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F8]

Completeness for explicitly countable set languages supplies a countable model of the consistent countable theory ZFC. The fixed-formula definability induction in Forcing theorem is a ZF proof scheme. Although that item's external semantic formulation assumes a transitive ground, an arbitrary model of ZFC satisfies the corresponding internal Boolean-valued truth theorem. Since the model below is externally countable, a generic ultrafilter exists by recursively meeting its externally countable list of internal dense sets; the extension is formed as the quotient of internal names by that ultrafilter, using internal Boolean values, rather than by an external well-founded recursion on names.

Proof

1.1

By [F8], take a countable first-order model $M ⊨ Z F C$ ; it may be externally ill-founded. Perform the following construction internally to $M$ . Its constructible universe $L^{M}$ satisfies ZFC+GCH. If $M$ thinks that $L^{M}$ has no inaccessible, set $N_{0} = L^{M}$ . Otherwise let $κ$ be what $L^{M}$ regards as its least inaccessible and set $N_{0} = (V_{κ})^{L^{M}} .$ The internal instance of [F2] says that this rank segment satisfies ZFC and that every internally inaccessible ordinal below $κ$ would already be inaccessible in $L^{M}$ , contrary to the internal minimality of $κ$ . Since $L^{M} ⊨ V = L$ and internally every member of this inaccessible rank segment has transitive closure of size below $κ$ , its constructible rank is below $κ$ ; the internal constructibility recursion [F1] therefore gives $N_{0} ⊨ V = L$ . Thus in both cases $N_{0}$ is an externally countable first-order model of ZFC+ $V = L$ +"there is no inaccessible cardinal", and hence of ZFC+CH. This is an internal model construction; no external well-foundedness or transitivity of $M$ or $N_{0}$ is asserted.

F1F2F8

2.1

Inside $N_{0}$ , apply the direct ZFC+CH construction theorem in [F3] and let $P$ be the forcing it produces. Externally enumerate all dense subsets of the Boolean completion of $P$ that belong to the countable structure $N_{0}$ , recursively meet them, and let $G$ be the generated $N_{0}$ -generic ultrafilter. Form $N_{0} [G]$ as the Boolean-valued quotient of the internal $N_{0}$ -names: equality and membership of two quotient classes are determined by whether their internal Boolean values lie in $G$ . The internal fixed-formula truth theorem from [F8] validates every standard formula and axiom used here; no external recursion through the possibly ill-founded name relation is required. In $N_{0} [G]$ form the definable inner class $N = H O D (S)$ . Because step 1.1 arranged $N_{0} ⊨ V = L$ , the inner-model conclusions in [F3] and [F4] apply and make $N$ a first-order model of ZF+DC in which every set of reals has the Baire property.

F3F4F8step 1.1

3.1

In addition, [F4] says internally in $N_{0} [G]$ that $N$ is transitive and has all of the extension's ordinals and reals. This is the hypothesis needed for the internal constructibility comparison below.

F4step 2.1

3.2

We first compute $L$ across the forcing extension without invoking the external transitivity clause of [F1]. The standard ZFC proof formalised by the forcing theorem says that set forcing adds no ordinals. It then proves, by internal induction on the common ordinals, that $L_{α}^{N_{0} [G]} = L_{α}^{N_{0}}$ for every internal ordinal $α$ : the zero and limit steps are immediate, and at a successor both sides take the definable subsets of the same preceding set structure, whose first-order satisfaction relation is unchanged. Since $N_{0} ⊨ V = L$ , the union of the ground levels is all of $N_{0}$ . Therefore $N_{0} [G]$ internally satisfies $L^{N_{0} [G]} = N_{0} .$ This is a theorem proved and evaluated inside the arbitrary model, not an external absoluteness comparison between transitive universes.

F1F8step 1.1step 2.1

4.1

Now reason inside $N_{0} [G]$ . The class $N$ is there a definable transitive ZF inner model containing every ordinal by step 3.1. The internal instance of the ZF theorem [F1] therefore gives $L^{N} = L^{N_{0} [G]} = N_{0} .$ Consequently $N$ satisfies that its constructible universe has no inaccessible cardinal, because that is exactly the first-order property arranged internally in $N_{0}$ at step 1.1. This establishes the same- $L$ invariant without ever treating the externally ill-founded structures as transitive.

F1step 1.1step 3.1step 3.2

5.1

Suppose toward a contradiction that every set of reals in $N$ is Lebesgue measurable. DC gives Countable Choice by [F7]. Since step 4.1 makes $ω_{1}^{N}$ noninaccessible in $L^{N}$ , [F5] supplies a real $x \in N$ with $ω_{1}^{L [x]} = ω_{1}^{N}$ . For every real $r \in N$ , the set $A (x \oplus r)$ is a set of reals in $N$ and is therefore measurable by the supposition. This is the full uniform premise of [F6], not just its instance at $r = 0$ , so $F (x)$ is rapid. But $F (x)$ is itself a set of reals by [F7] and a rapid filter is not Lebesgue measurable, contradicting the supposition. Hence $N$ contains a nonmeasurable set of reals.

F5F6F7step 4.1

6.1

Starting from the countable arbitrary model supplied by consistency, steps 1.1--5.1 construct a first-order model $N$ of $Z F + D C + all BP + \neg all LM$ . Hence $Con (Z F C) \to Con (Z F + D C + all BP + \neg all LM) .$ No transitive-model consequence of bare consistency is used.

F3F8step 1.1step 2.1step 5.1

7.1

The steps above establish the relative consistency and the failure of the implication from universal BP to universal LM over ZF+DC; this is the Statement.

step 3.1step 5.1step 6.1∎

5 · Examples, counterexamples and false statements

None yet.