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.

Sigma-one-three measurability makes omega-one inaccessible in L

Statement

Assume ZF+Countable Choice and boldface Σ31 measurability. Then the ambient ω1 is an inaccessible cardinal in L.

Facts & Assumptions

Given: Countable Choice and the hypothesis that every Σ31(x) set of reals is Lebesgue measurable for every real x.

[F1]

Boldface Sigma-one-three measurability: the pointclass Σ31(x), the inclusion of Σ21(x) in Σ31(x) by a dummy real quantifier, and the definition of boldface measurability.

[F2]

Failure of inaccessibility in L produces a real with correct omega-one: failure of inaccessibility of the ambient ω1 in L yields a real x with ω1L[x]=ω1.

[F3]

A measurable null-code order bounds the constructible null union: the null-code order A(x) is Σ21(x), and its measurability makes the union of the constructible null Borel sets null.

[F4]

Uniform null-code measurability makes the Raisonnier filter rapid: under Countable Choice, ω1L[x]=ω1 and measurability of A(x⊕r) for every real r, the filter F(x) is rapid.

[F5]

The Raisonnier family is a Sigma-one-three filter: F(x) is a Σ31(x) subset of the reals.

[F6]

Rapid filters are not Lebesgue measurable: rapid filters are not Lebesgue measurable.

[F7]

The Axiom of Countable Choice (ACω): the ambient choice hypothesis.

Proof

1.1assume-contraF2

Assume, for contradiction, that the ambient ω1 is not an inaccessible cardinal of L, and let x be a real with ω1L[x]=ω1, as supplied by [F2].

2.1F1F3step 1.1

For every real r, the null-code order A(x⊕r) is Σ21(x⊕r) by [F3]. By [F1] it is Σ31(x⊕r), so the boldface measurability hypothesis makes A(x⊕r) measurable. Thus the uniform hypothesis of [F4] holds, not merely its instance at r=0.

3.1F4F7step 2.1

By [F4], applied with Countable Choice [F7], ω1L[x]=ω1 and the uniform conclusion of step 2.1, the Raisonnier filter F(x) is rapid.

4.1F5F6step 3.1

By [F5] the filter F(x) is a Σ31(x) set of reals, and by [F6] it is not Lebesgue measurable. This contradicts the hypothesis that every Σ31(x) set is measurable.

5.1discharge-contradictionstep 4.1∎

The contradiction in step 4.1 refutes the assumption of step 1.1, so the ambient ω1 is inaccessible in L.

Depends on

Used by

Dependency tree · two levels

32 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