Alphabeta MathHow 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.
Cohen, collapse, and Lévy-collapse forcing orders
Definition
For infinite and nonzero ,
the partial functions of domain size , ordered by reverse inclusion. For infinite put
For an ordinal , the finite-condition Lévy order consists of finite functions with and whenever . In all three cases the empty function is largest and compatible conditions have union as a common extension. These are ground-model sets when used as forcing orders. The second order adds one -indexed surjection onto ; the third simultaneously addresses every nonzero .
Depends on
- Forcing preorders, compatibility and filters
- Cardinal sum $\kappa \oplus \lambda$, product $\kappa \otimes \lambda$ and exponentiation $\kappa^{\lambda}$, and why they are written apart from the ordinal operations
- The successor cardinal $\kappa^{+}$, the alephs $\aleph_\alpha$, the beths $\beth_\alpha$, successor and limit cardinals, and the identifications $\aleph_0 = \omega$ and $\aleph_1 = \omega_1$
Used by
- The basic Cohen symmetric system Definition
- A nice name for one Cohen coordinate Example
- MA produces a real outside a small listed family Example
- Cardinal effects of collapse and Lévy-collapse forcing Theorem
- Closure and chain conditions of Cohen forcing Theorem
- Cohen coordinates are distinct and mutually generic Theorem
- The omega₂ iteration forces MA and continuum aleph₂ Theorem
Dependency tree · two levels
24 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)