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.
Cardinal effects of collapse and Lévy-collapse forcing
Statement
In ZFC, if is infinite regular and , is -closed and its generic union is a surjection onto . If is regular uncountable, is -cc, collapses every nonzero to countable size, preserves , and therefore forces .
Facts & Assumptions
Given: AC and the stated regularity hypotheses.
Cohen, collapse, and Lévy-collapse forcing orders gives both partial-function orders.
Closure, distributivity, and absence of new short sequences and Chain conditions preserve high cofinalities and ccc preserves cardinals give the preservation consequences.
The finite delta-system lemma at a regular uncountable cardinal thins finite supports.
Forcing theorem turns dense-set calculations into extension assertions.
Proof
A descending sequence of fewer than collapse conditions has union of domain size below , so is -closed. For each and , the sets requiring in the domain and in the range are dense (using a fresh coordinate for the latter). Hence the generic union is a total surjection .
Given many Lévy conditions, F3 thins their finite domains to a delta system with a fixed finite root. At each root coordinate there are only possible values; regularity and finiteness of the root therefore leave fewer than possible root assignments. Thin the conditions until their root restrictions agree. Two remaining conditions then have compatible union, so is -cc.
For every , the union of the generic restrictions to is total by coordinate dense sets and hits every by range dense sets. It is a surjection . step 1.2 and F2 preserve the cardinal and regularity of , while all smaller infinite ordinals become countable; hence the extension identifies with .
Depends on
Used by
Dependency tree · two levels
20 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, Chapters 3–4 (standard reference, not scraped)