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.
FALSE, relative to an inaccessible cardinal: ZF + DC proves that a nonmeasurable subset of exists
Statement
Assume ZFC together with the existence of an inaccessible cardinal is consistent. FALSE. ZF + DC proves that a nonmeasurable subset of exists. Equivalently, relative to this consistency hypothesis, ZF + DC alone cannot guarantee a construction of such a set.
Facts & Assumptions
Given: The consistency of ZFC together with the existence of an inaccessible cardinal, and the external consistency-strength results recorded on the published choice pages.
If ZFC together with the existence of an inaccessible cardinal is consistent, then so is ZF + DC + "every set of reals is Lebesgue measurable" (Solovay's model: ZF + DC with every set of reals measurable ‡).
If ZF + DC + “every set of reals is Lebesgue measurable” is consistent, then so is ZFC + “there exists an inaccessible cardinal”; in contrast, Con(ZF) implies the consistency of ZF + DC + “every set of reals has the Baire property” (Shelah 1984: the inaccessible is needed for measurability, not for the Baire property ‡).
Refutation
By [L1], the stated consistency hypothesis supplies a model of ZF + DC in which every set of reals is Lebesgue measurable.
If ZF + DC proved that a nonmeasurable subset of exists, every model of ZF + DC would contain one. The model from step 1.1 contains none, so the asserted theorem of ZF + DC is false relative to the stated consistency hypothesis. This is precisely the consistency-strength obstruction recorded in [L2].
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
3 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
- R. M. Solovay, A model of set-theory in which every set of reals is Lebesgue measurable (standard reference, not scraped)
- S. Shelah, Can you take Solovay's inaccessible away? (standard reference, not scraped)