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.

Shelah's model separates universal Baire property from universal measurability

Statement

Relative to Con⁡(ZFC), it is consistent that ZF+DC holds, every set of reals has the Baire property, and not every set of reals is Lebesgue measurable. Thus universal Baire property does not entail universal Lebesgue measurability over ZF+DC.

Facts & Assumptions

Given: The model-theoretic assumption Con⁡(ZFC) and Shelah's published relative-consistency construction.

[F1]

Absoluteness, idempotence and minimality of L is a theorem of ZF. Its external comparison clause assumes transitivity, but the theorem itself may be evaluated inside any first-order model of ZF. In particular, internally, a definable transitive inner class with all ordinals computes the same L as its ambient model. No external transitivity of the model used below is inferred.

[F2]

Inaccessible and Mahlo cardinals defines inaccessibility, while An inaccessible rank segment models ZFC proves in ZFC that Vκ models ZFC when κ is inaccessible and that inaccessibility below κ is absolute to that rank segment. This theorem too can be interpreted internally in an arbitrary first-order model.

[F3]

Shelah's CH-length homogeneous sweet construction constructs the required forcing over every ZFC+CH ground. When the ground also satisfies V=L, Every real set in the Shelah inner model has the Baire property proves at the exact homogeneity and Borel-to-open interfaces that the resulting N=HOD(S) has universal Baire property. The exact equiconsistency of ZFC and the all-Baire-property model is used only for the published metatheoretic comparison, not as the construction interface.

[F4]

The Shelah inner model satisfies ZF and Dependent Choice: N has the same ordinals and reals as the extension and satisfies ZF+DC.

[F5]

Failure of inaccessibility in L produces a real with correct omega-one: in ZF+Countable Choice, if the ambient ω1 is not inaccessible in its constructible universe, there is a real x with ω1L[x]=ω1.

[F6]

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

[F8]

Completeness for explicitly countable set languages supplies a countable model of the consistent countable theory ZFC. The fixed-formula definability induction in Forcing theorem is a ZF proof scheme. Although that item's external semantic formulation assumes a transitive ground, an arbitrary model of ZFC satisfies the corresponding internal Boolean-valued truth theorem. Since the model below is externally countable, a generic ultrafilter exists by recursively meeting its externally countable list of internal dense sets; the extension is formed as the quotient of internal names by that ultrafilter, using internal Boolean values, rather than by an external well-founded recursion on names.

Proof

1.1F1F2F8

By [F8], take a countable first-order model M⊨ZFC; it may be externally ill-founded. Perform the following construction internally to M. Its constructible universe LM satisfies ZFC+GCH. If M thinks that LM has no inaccessible, set N0=LM. Otherwise let κ be what LM regards as its least inaccessible and set N0=(Vκ)LM. The internal instance of [F2] says that this rank segment satisfies ZFC and that every internally inaccessible ordinal below κ would already be inaccessible in LM, contrary to the internal minimality of κ. Since LM⊨V=L and internally every member of this inaccessible rank segment has transitive closure of size below κ, its constructible rank is below κ; the internal constructibility recursion [F1] therefore gives N0⊨V=L. Thus in both cases N0 is an externally countable first-order model of ZFC+V=L+"there is no inaccessible cardinal", and hence of ZFC+CH. This is an internal model construction; no external well-foundedness or transitivity of M or N0 is asserted.

2.1F3F4F8step 1.1

Inside N0, apply the direct ZFC+CH construction theorem in [F3] and let P be the forcing it produces. Externally enumerate all dense subsets of the Boolean completion of P that belong to the countable structure N0, recursively meet them, and let G be the generated N0-generic ultrafilter. Form N0[G] as the Boolean-valued quotient of the internal N0-names: equality and membership of two quotient classes are determined by whether their internal Boolean values lie in G. The internal fixed-formula truth theorem from [F8] validates every standard formula and axiom used here; no external recursion through the possibly ill-founded name relation is required. In N0[G] form the definable inner class N=HOD(S). Because step 1.1 arranged N0⊨V=L, the inner-model conclusions in [F3] and [F4] apply and make N a first-order model of ZF+DC in which every set of reals has the Baire property.

3.1F4step 2.1

In addition, [F4] says internally in N0[G] that N is transitive and has all of the extension's ordinals and reals. This is the hypothesis needed for the internal constructibility comparison below.

3.2F1F8step 1.1step 2.1

We first compute L across the forcing extension without invoking the external transitivity clause of [F1]. The standard ZFC proof formalised by the forcing theorem says that set forcing adds no ordinals. It then proves, by internal induction on the common ordinals, that LαN0[G]=LαN0 for every internal ordinal α: the zero and limit steps are immediate, and at a successor both sides take the definable subsets of the same preceding set structure, whose first-order satisfaction relation is unchanged. Since N0⊨V=L, the union of the ground levels is all of N0. Therefore N0[G] internally satisfies LN0[G]=N0. This is a theorem proved and evaluated inside the arbitrary model, not an external absoluteness comparison between transitive universes.

4.1F1step 1.1step 3.1step 3.2

Now reason inside N0[G]. The class N is there a definable transitive ZF inner model containing every ordinal by step 3.1. The internal instance of the ZF theorem [F1] therefore gives LN=LN0[G]=N0. Consequently N satisfies that its constructible universe has no inaccessible cardinal, because that is exactly the first-order property arranged internally in N0 at step 1.1. This establishes the same-L invariant without ever treating the externally ill-founded structures as transitive.

5.1F5F6F7step 4.1

Suppose toward a contradiction that every set of reals in N is Lebesgue measurable. DC gives Countable Choice by [F7]. Since step 4.1 makes ω1N noninaccessible in LN, [F5] supplies a real x∈N with ω1L[x]=ω1N. For every real r∈N, the set A(x⊕r) is a set of reals in N and is therefore measurable by the supposition. This is the full uniform premise of [F6], not just its instance at r=0, so F(x) is rapid. But F(x) is itself a set of reals by [F7] and a rapid filter is not Lebesgue measurable, contradicting the supposition. Hence N contains a nonmeasurable set of reals.

6.1F3F8step 1.1step 2.1step 5.1

Starting from the countable arbitrary model supplied by consistency, steps 1.1--5.1 construct a first-order model N of ZF+DC+all BP+¬all LM. Hence Con⁡(ZFC)→Con⁡(ZF+DC+all BP+¬all LM). No transitive-model consequence of bare consistency is used.

7.1step 3.1step 5.1step 6.1∎

The steps above establish the relative consistency and the failure of the implication from universal BP to universal LM over ZF+DC; this is the Statement.

Depends on

Used by

Dependency tree · two levels

86 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