LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedaudited 2026-09-22

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.

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∎

Depends on

Used by

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Saharon Shelah, Can You Take Solovay's Inaccessible Away? (standard reference, not scraped)