Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedaudited 2026-09-22
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.

Exact equiconsistency of universal measurability and an inaccessible

Statement

ZFC plus an inaccessible cardinal and ZF+DC plus every set of reals Lebesgue measurable are equiconsistent. The same lower bound already follows from universal boldface Σ31 measurability under Countable Choice.

Facts & Assumptions

Given: Fixed arithmetizations of the two theories and their finite fragments.

[F1]

Solovay-model regularity is consistent relative to an inaccessible cardinal: by the externally indexed finite-fragment transfer for the Lévy-collapse construction, Con(ZFC+an inaccessible)Con(ZF+DC+universal LM). No uniform arithmetic proof-code transformer is used in that theorem.

[F2]

All-real-set measurability yields an inaccessible inner model: from ZF+DC plus universal measurability, the constructible universe satisfies ZFC and contains an inaccessible cardinal. Relativization to that definable inner model is an interpretation, so it sends every actual finite target refutation to a source refutation (Interpretation transports derivations and inconsistency).

[F3]

Under ZF+Countable Choice plus universal boldface Σ31 measurability, the ambient ω1 is inaccessible in L (Sigma-one-three measurability makes omega-one inaccessible in L, The Axiom of Countable Choice (ACω), Boldface Sigma-one-three measurability), and L satisfies ZFC (Semantic and formal inner-model theorem for L). Relativization to L therefore gives the same refutation translation as in [F2] (Interpretation transports derivations and inconsistency).

Proof

1.1

Upper bound: assume Con(ZFC+inaccessible). The exact external finite-fragment consistency implication in [F1] yields Con(ZF+DC+every set of reals is Lebesgue measurable).

F1
1.2

Lower bound: assume Con(ZF+DC+universal LM). If ZFC plus an inaccessible had an actual refutation, [F2] would translate it to a refutation of the assumed source theory. Hence Con(ZFC+inaccessible) follows.

F2
1.3

The refinement: if ZF+Countable Choice plus boldface Σ31 measurability is consistent, an actual refutation of ZFC plus an inaccessible would translate by [F3] to a refutation of that source theory. Thus its consistency already implies the consistency of ZFC plus an inaccessible cardinal. This is the stronger form of the lower bound stated.

F3
1.4

The inaccessible hypothesis is needed only on the Solovay branch: steps 1.1 uses it, and steps 1.2 and 1.3 use none; the separation of the two branches is the point of this pair.

F1F2F3
2.1

Steps 1.1 through 1.3 give the two consistency implications in both directions, and step 1.4 records the exact role of the inaccessible; this is the Statement.

step 1.1step 1.2step 1.3

Depends on

Used by

Dependency tree · two levels

44 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