Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passverified 2026-08-05 (gpt-5.6-sol-codex-subscription)
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.

R≈P(N) in ZF, by the Cantor set for one injection and by the cuts {q∈Q:q<x} for the other; so ∣R∣=2ℵ0 under the Axiom of Choice

Example

Write ω2 for the set of functions ω→2={0,1}, the 2 here being the von Neumann natural number, and P(N) for the power set of N=ω (The natural numbers N (von Neumann)). Then:

(a) In ZF, with no choice principle:

R  ≈  ω2  ≈  P(N)

(Equinumerous sets, A≈B and A⪯B, The real numbers).

(b) Assuming the Axiom of Choice (The Axiom of Choice):

∣R∣  =  2ℵ0  =  ∣P(N)∣

(Cardinal sum κ⊕λ, product κ⊗λ and exponentiation κλ, and why they are written apart from the ordinal operations, The successor cardinal κ+, the alephs ℵα, the beths ℶα, successor and limit cardinals, and the identifications ℵ0=ω and ℵ1=ω1).

The two injections are the classical ones and neither uses a binary expansion. One direction is the Cantor set: The Cantor set is exactly the set of ∑k≥1ak3−k with every ak∈{0,2}, and this gives a bijection with {0,1}N already supplies a bijection from the sequences with values in {0,1} onto the Cantor set C⊆R (The Cantor middle-thirds set as the intersection of the sets Cn obtained by removing open middle thirds). The other is the cut map x↦{q∈Q:q<x}, injective because Q is dense in R (ℚ is dense in every Archimedean ordered field), and P(Q) is a copy of P(N) because Q is countable (Q is countably infinite). The Schröder-Bernstein theorem closes the loop, and it is choice free, which is what makes clause (a) a theorem of ZF.

Facts & Assumptions

Given: R with its order and the canonical embedding ι:Q→R; the Axiom of Choice is assumed only in clause (b).

[L1]

The order of Order on the reals makes R (The real numbers) a totally ordered field (The reals form a totally ordered field) with the least-upper-bound property (The Cauchy-sequence reals have the least-upper-bound property), hence a complete ordered field (Complete ordered field (least-upper-bound property)) and hence Archimedean (Every complete ordered field is Archimedean); and ι:Q→R is the unique order-preserving field embedding (The unique embedding of ℚ into an ordered field).

[L2]

For x<y in an Archimedean ordered field there is a rational q with x<ι(q)<y (ℚ is dense in every Archimedean ordered field).

[L6]

If A⪯B and B⪯A then A≈B (The Schröder-Bernstein theorem).

[L7]

For a well-orderable set X, ∣X∣ is the least ordinal equinumerous with X and equinumerous sets receive the same one (A set equinumerous with some ordinal has a least such ordinal, that ordinal is a cardinal, and equinumerous sets get the same one; no choice principle is used, Cardinal (initial ordinal) and cardinality); assuming the Axiom of Choice every set has one (The well-ordering theorem).

[L9]

A subset inclusion is an injection, a composition of injections is an injection, and a map with a two-sided inverse is a bijection (Injection, surjection, bijection).

Verification

technique · direct
1.1

The two-element sets 2={0,1} and {0R,1R} are equinumerous, since 0R≠1R in a field, so ω2≈ω{0R,1R} by [L5].

L1L5L9
1.2

The set ω{0R,1R} is exactly the set of sequences with values in {0,1} of [L3], so it is in bijection with C⊆R, and composing with the inclusion gives an injection ω{0R,1R}→R.

L3L9
1.3

The map x↦Qx:={ q∈Q:ι(q)<x } is an injection R→P(Q): for x≠y the order is total by [L1], so we may assume x<y, and [L2] supplies a rational q with x<ι(q)<y, whence q∈Qy and q∉Qx, so Qx≠Qy.

L1L2
1.4

P(Q)≈P(N) by [L4] and [L5].

L4L5
1.5

P(N)≈ω2: the map sending S⊆N to its characteristic function has the two-sided inverse h↦h−1[{1}].

L9
2.1

Chaining steps 1.1, 1.2 gives ω2⪯R, and chaining steps 1.3, 1.4, 1.5 gives R⪯ω2; so [L6] yields R≈ω2, and with step 1.5 also R≈P(N), which is clause (a) and uses no choice principle.

step 1.1step 1.2step 1.3step 1.4step 1.5L6L9
3.1

Assuming the Axiom of Choice, all three sets have cardinalities by [L7], equal by step 2.1, and ∣P(N)∣=2∣ω∣=2ℵ0 by [L8] and [L7]; so ∣R∣=2ℵ0=∣P(N)∣, which is clause (b).

step 2.1L7L8∎

Remarks

Why binary expansions are avoided. The textbook proof identifies a real in [0,1] with the set of positions where its binary expansion has a 1, and then has to deal with the reals having two expansions. Neither injection above meets that difficulty: the Cantor set map is already published as a bijection, and the cut map needs only density. The cost is that the two injections go in opposite directions and The Schröder-Bernstein theorem is required to combine them, which is free, since that theorem is choice free.

Which half needs the Axiom of Choice, and why. Clause (a) is an equinumerosity statement and is a theorem of ZF. Clause (b) writes ∣R∣ and 2ℵ0 as cardinals, that is as ordinals, and in ZF alone P(N) need not be well-orderable, so those symbols need not denote anything. The hypothesis buys the notation, not the mathematics.

What is still not decided. Nothing here says which aleph 2ℵ0 is. The one constraint proved in this development is that its cofinality is uncountable (Assuming the Axiom of Choice: κ<κcf⁡(κ) for every infinite cardinal κ, and cf⁡(2κ)>κ; in particular cf⁡(2ℵ0)>ℵ0), and the question of whether it is ℵ1 is the continuum hypothesis (What each result on this page costs in choice, and where the continuum escapes what ZFC can decide).

Depends on

Used by

Dependency tree · two levels

106 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