Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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.

V equals L implies diamond

Statement

ZF proves that V=L implies ♢ on ω1. Thus for every A⊆ω1, the set of correct guesses is stationary, not merely unbounded.

Facts & Assumptions

Given: Ambient ZF together with V=L. Clubs and stationarity are the notions on ω1 in the cited definitions.

[F1]

Finite-stage L histories and weak limit-level absoluteness supplies a formula χ defining the actual canonical order <L and agreeing with its restriction in every nonzero limit L-level; the stage-by-stage order makes each Lγ an initial segment.

[F2]

The canonical definable global well-order of L says that <L well-orders all of L by least definition codes.

[F3]

Canonical L-hulls are elementary and small supplies a canonical countably infinite elementary hull of a finite seed in a nonzero limit L-level, without ambient Choice.

[F4]

Condensation for constructible levels identifies the transitive collapse of such a hull with an actual Lγ.

[F5]

What the collapse fixes gives π(ω1)=X∩ω1 when that intersection is transitive, and fixes transitive parts pointwise.

[F6]

Transfinite recursion realizes the deterministic recursive guessing rule.

[F7]

Diamond on ω1, Closed unbounded subsets of ordinals, and The club filter and nonstationary ideal give the required subset, club, and stationary clauses.

Proof

1.1F1F2F6F7given

Define (Sα)α<ω1 by F6. Having defined the earlier guesses, call (B,D) bad at α when B⊆α, D⊆α is club in α, and Sξ≠B∩ξ for every ξ∈D. If a bad pair exists, take the χ-least ordered pair and set Sα=B; otherwise set Sα=∅. F2 makes the choice unique and F1 makes this one fixed first-order recursion; S0=∅, and always Sα⊆α.

2.1F2F7assume-contrastep 1.1

Assume for contradiction that this sequence is not diamond. By F7 there are A⊆ω1 and a club C⊆ω1 such that Sα≠A∩α for every α∈C. Among all such global failure pairs choose the χ-least (A,C), possible because V=L and F2 well-orders L.

3.1F1F3F7step 2.1

Choose a nonzero limit θ such that Lθ contains S,A,C,ω1. Because Lθ is a <L-initial segment and the badness predicate has only bounded quantifiers once these parameters are fixed, it sees that (A,C) is the least failure pair. Let X be the canonical hull of this finite seed. F3 gives X≺Lθ and makes X countably infinite. Put δ=X∩ω1. Elementarity makes X∩ω1 an ordinal, hence transitive, and countability gives δ<ω1. For every ξ<δ, elementarity applied to the unbounded set C produces c∈C∩X above ξ; hence C∩δ is unbounded in δ. It follows that δ is a nonzero countable limit, and closure of C gives δ∈C.

4.1F4F5step 3.1

Collapse X by π to M=Lγ using F4. By F5, π(ω1)=δ. Since every ξ<δ lies in X, evaluation of the function S∈X puts Sξ∈X; as Sξ⊆ξ, F5 fixes it. The collapse equations therefore give π(S)=S↾δ, π(A)=A∩δ, and π(C)=C∩δ.

5.1F1F4F7step 1.1step 2.1step 4.1

By elementarity and isomorphism, M regards (A∩δ,C∩δ) as its χ-least failure pair for the sequence S↾δ on its first uncountable ordinal δ. The predicates “subset of δ,” “club in δ,” and “fails at every member” are bounded here and are absolute between the transitive M and the universe for these fixed parameters. F1 says that M and the universe use the same χ-order on M, and that M=Lγ is an initial segment of that order. Therefore no ambient bad pair at δ can precede (A∩δ,C∩δ): any preceding pair would belong to M and contradict internal leastness. Thus step 1.1 sets Sδ=A∩δ.

6.1F7discharge-contradictionstep 2.1step 3.1step 5.1∎

But step 3.1 gives δ∈C, while step 2.1 says Sδ≠A∩δ at every member of C. This contradicts step 5.1. Hence the sequence is diamond, and its correct-guess set meets every club for every target subset of ω1.

Depends on

Used by

Dependency tree · two levels

35 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