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.
Chain conditions preserve high cofinalities and ccc preserves cardinals
Statement
In ZFC, if is regular and is -cc, then forcing with preserves every ground-model cofinality at least and every ground-model cardinal at least . In particular ccc forcing preserves all cofinalities and cardinals.
Facts & Assumptions
Given: AC, regular , and a -cc forcing .
Forcing theorem lets maximal antichains decide values of names.
; and ; for a limit ordinal the value is an infinite cardinal with , so it is regular; and every cofinal subset of has cardinality at least , a value that is attained reduces cofinality questions to regular initial ordinals.
Absorption: for cardinals with infinite and , , and when bounds unions and products of infinite well-orderable cardinals.
Forcing preserves ordinals keeps the ordinal scale fixed.
Proof
If , choose for each a maximal antichain below deciding . Each has size , so the ground-model set of possible values has size . Then . AC is used for maximal antichains and their simultaneous selection.
Let be regular and . If a condition forced cofinal, step 1.1 and regularity would put its range inside a ground set of size , which is bounded in , contradiction. Thus regular cofinalities at least are preserved; F2 transfers this to every ground cofinality at least .
Suppose a ground cardinal were collapsed. By F4, some and a condition would force a surjection . Step 1.1 puts its range inside the ground set , with . If , regularity of gives ; if , cardinal arithmetic under AC gives (with the finite cases immediate). Either way cannot force onto . Thus every ground cardinal at least remains a cardinal. For ccc, ; finite and countable cardinals and cofinalities are absolute, so steps 2.1 and 3.1 cover all of them.
Depends on
- Closure, distributivity, and chain conditions for forcing orders
- Forcing theorem
- Forcing preserves ordinals
- $\operatorname{cf}(\alpha) \le \alpha$; $\operatorname{cf}(0) = 0$ and $\operatorname{cf}(\alpha + 1) = 1$; for a limit ordinal $\lambda$ the value $\operatorname{cf}(\lambda)$ is an infinite cardinal with $\operatorname{cf}(\operatorname{cf}(\lambda)) = \operatorname{cf}(\lambda)$, so it is regular; and every cofinal subset of $\lambda$ has cardinality at least $\operatorname{cf}(\lambda)$, a value that is attained
- Absorption: for cardinals $\kappa, \lambda$ with $\kappa$ infinite and $\lambda \le \kappa$, $\kappa \oplus \lambda = \kappa$, and $\kappa \otimes \lambda = \kappa$ when $\lambda \ne 0$
- The Axiom of Choice
Used by
- Small sets of ground ordinals are captured at a bounded iteration stage Lemma
- Cardinal effects of collapse and Lévy-collapse forcing Theorem
- Cohen forcing raises and, under a name count, fixes the continuum Theorem
- Generic factorization and ccc preservation for two-step iterations Theorem
- Higher Cohen forcing violates GCH at a regular cardinal Theorem
- The omega₂ iteration forces MA and continuum aleph₂ Theorem
Dependency tree · two levels
37 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
- Karagila, Forcing & Symmetric Extensions, Chapter 3 preservation theorem (standard reference, not scraped)