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.
Absorption, factorization, and homogeneous truth in the Solovay collapse
Statement
For every in , there are a real and an ordinal such that and is definable there from . There is also an -generic over such that . A sentence with parameters in and no occurrence of has homogeneous Boolean value or . The same factorization is available after adjoining one random or Cohen real.
Facts & Assumptions
Given: The Solovay collapse setup and a supplied generic extension.
The Lévy collapse localizes countable ordinal data: every countable ordinal sequence belongs to a small initial-collapse extension.
Forcing theorem: deciding conditions and the truth lemma compute forcing truth.
The Axiom of Choice: ambient AC enumerates the dense sets and maximal antichains used in the absorption recursion.
Proof
By F1, choose with . Solovay's small-collapse factorization replaces this initial extension by , where is a -generic collapsing map for some ordinal and . Define
Then is a real. In , quotienting by equality in the coded preorder and taking its well-order type reconstructs and ; hence . Finally choose the canonically least constructible-ground name for and let be its ordinal code. Valuation by the generic recovered from defines from . This is the cited real-capture argument; constructibility is used only to replace the ground name parameter by . [F1, F2, F3]
The initial forcing has size below . Solovay's absorption construction recursively embeds its Boolean completion and the tail collapse into a fresh copy of over : at stage , put the next maximal antichain and the next dense set into coordinates above all earlier supports. Regularity of bounds each stage, and the union is a dense complete embedding. The image of is therefore a generic with both inclusions . F3 is used exactly to enumerate those dense sets and maximal antichains.
The collapse is weakly homogeneous. Given , first move the finitely many coordinates of away from those of by coordinate permutations; the moved is compatible with . If some condition forced a sentence and another forced its negation, apply such an automorphism. It fixes every and yields compatible conditions forcing opposites, contrary to forcing consistency. Density of decision then makes the Boolean value or . The omission of is essential.
Random and Cohen forcing have cardinal below in each localized model. Insert their Boolean completion as the first small factor in the same absorption recursion. Thus, after adjoining its generic real , the remaining extension is again a homogeneous Lévy collapse over .
Depends on
Used by
- Factoring the Solovay collapse around a real parameter Example
- Homogeneous truth about a generic real has Borel representatives Lemma
- All sets of reals in Solovay L(R) have LM, BP, and PSP Theorem
- Every uncountable Solovay-model set of reals has a perfect subset Theorem
- The Solovay inner model satisfies ZF and every real set has a real–ordinal definition Theorem
Dependency tree · two levels
14 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
- Solovay 1970, Part I §1.12, Lemma 3.5, and Lemmas 4.1–4.3 (standard reference, not scraped)