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.
The Solovay inner model satisfies Dependent Choice
Statement
satisfies the serial-relation Dependent Choice principle, although it need not satisfy full Choice.
Facts & Assumptions
Given: In , a nonempty set , a serial relation , and .
The Solovay inner model is closed under ambient omega-sequences: every ambient omega-sequence of elements of lies in .
The serial-relation Dependent Choice principle over ZF: gives the required serial-chain formulation.
The Axiom of Choice: ambient AC supplies recursive choices.
Proof
In , recursively set as given and, using ambient AC, choose with . Seriality supplies a nonempty successor fibre at every finite stage.
The resulting function maps into , so F1 puts it in . Transitivity makes compute each assertion correctly. This is precisely DC by F2. If is a singleton the constant chain works; nonemptiness is essential and supplied.
Depends on
Used by
- The Solovay model has no Banach–Tarski decomposition Corollary
- The Solovay model has no Vitali or Bernstein set Corollary
- The volume contradiction for an alleged Banach–Tarski decomposition Example
- Borel-code, measure, category, and perfect-set absoluteness Lemma
- Fixed finite-fragment verification for the Solovay construction Lemma
- Universal real measurability transfers to finite-dimensional Euclidean spaces Lemma
- The Solovay model has no Hamel basis and no discontinuous additive real function Theorem
Dependency tree · two levels
8 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 III, Lemma 2.7 (standard reference, not scraped)