TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

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$ is uncountable (Cantor's nested intervals, 1874)

Statement

Let $R$ be a complete ordered field (Complete ordered field (least-upper-bound property)). Then $R$ is uncountable (Finite, countably infinite, countable, uncountable): there is no surjection $N \to R$ , so $R$ is neither finite nor countably infinite.

The proof is Cantor's original argument of 1874, not the decimal diagonal. Assuming a surjection $f : N \to R$ , one builds nested closed intervals $[a_{n}, b_{n}]$ with $a_{n} < b_{n}$ and $f (n) \notin [a_{n + 1}, b_{n + 1}]$ , and then $\sup {a_{n}}$ is a real number that $f$ misses. The decimal diagonal is deliberately avoided: decimal expansions are infinite series, which this library has not yet constructed, so a diagonal proof here would rest on machinery that does not exist. The diagonal argument survives in its non-circular form, on power sets, as Cantor's theorem earlier on this page; see the remarks below.

The construction uses no choice, and that is what the thirds are for. Given $[a_{n}, b_{n}]$ of length $d$ , its three closed thirds $[a_{n}, a_{n} + d / 3]$ , $[a_{n} + d / 3, a_{n} + 2 d / 3]$ , $[a_{n} + 2 d / 3, b_{n}]$ cannot all contain $f (n)$ , because the first and the third are disjoint; the rule takes the first one in that fixed order which does not contain $f (n)$ . That is a definition by cases, so the whole construction is a single application of the recursion theorem (The recursion theorem) to one explicitly given function. A version of the argument that says "pick a third avoiding $f (n)$ " would be using dependent choice, silently and unnecessarily.

Facts & Assumptions

Given: A complete ordered field $R$ , with $0 \neq 1$ and the order of Ordered field. For $a \leq b$ write $[a, b] = {x \in R : a \leq x \leq b}$ , and write $I = {(a, b) \in R \times R : a < b}$ for the set of pairs coding nondegenerate closed intervals.

[L1]

Least-upper-bound property: every nonempty $S \subseteq R$ that is bounded above has a least upper bound $\sup S$ , an upper bound below every upper bound (Complete ordered field (least-upper-bound property), Lower bound, bounded below, bounded set).

[L2]

The least upper bound is unique when it exists (Suprema and infima are unique).

[L3]

Epsilon characterisation: for a nonempty $S$ bounded above and an upper bound $u$ of $S$ , $u = \sup S$ if and only if for every $ε > 0$ there is $s \in S$ with $u - ε < s$ (Epsilon characterisation of the supremum).

[L4]

Order and arithmetic in an ordered field: $0 < 1$ (The multiplicative identity is positive); $a < b$ implies $a + c < b + c$ , and $a < b$ with $c < d$ implies $a + c < b + d$ (Order is preserved by adding a constant and by adding inequalities); $a > 0$ implies $a^{- 1} > 0$ (Inverses of positives are positive, and reciprocation reverses order); a product of positives is positive (Sign rules for products and monotonicity of multiplication); the order is transitive and satisfies trichotomy (Ordered field).

[L5]

Recursion: for any set $X$ , $x_{0} \in X$ and $F : X \to X$ there is $h : N \to X$ with $h (0) = x_{0}$ and $h (σ (n)) = F (h (n))$ (The recursion theorem).

[L6]

Induction (The principle of mathematical induction); any two naturals are comparable (Trichotomy of the order on $N$ ); the order of $N$ is the additive one, $m \leq n$ meaning $m + k = n$ for some $k$ (Order on the natural numbers, The natural numbers $N$ (von Neumann)), and it satisfies $n < σ (n)$ and $m < σ (n) ⟺ m \leq n$ (On $N$ the order is membership: $m < n ⟺ m \in n$ ), so $m \leq σ (n)$ holds exactly when $m \leq n$ or $m = σ (n)$ .

[L7]

A nonempty set is at most countable if and only if some surjection from $N$ onto it exists; uncountable means not at most countable (A nonempty set is at most countable iff it is a surjective image of $N$ , Finite, countably infinite, countable, uncountable).

Proof

technique · contradiction

1.1

Suppose, for contradiction, that $R$ is at most countable. Since $0 \in R$ , it is nonempty, so [L7] provides a surjection $f : N \to R$ .

assume-contragivenL7

1.2

Put $3 : = 1 + 1 + 1$ . Adding the inequality $0 < 1$ to itself twice gives $3 > 0$ by [L4], so $3 \neq 0$ and $3^{- 1} > 0$ ; hence for $d > 0$ the element $d / 3 : = d \cdot 3^{- 1}$ is positive, and $d / 3 + d / 3 + d / 3 = d \cdot 3^{- 1} \cdot 3 = d$ .

L4algebra

2.1

Fix the trisection rule. Let $(a, b) \in I$ and $y \in R$ . Put $d = b - a > 0$ , $p = a + d / 3$ and $q = p + d / 3$ ; then $a < p < q < b$ by step 1.2 and [L4], since $p - a = q - p = b - q = d / 3 > 0$ . The three pairs $(a, p)$ , $(p, q)$ , $(q, b)$ all lie in $I$ and their intervals are contained in $[a, b]$ . Moreover $[a, p]$ and $[q, b]$ are disjoint, because $x \leq p < q \leq x$ is impossible; so $y$ fails to lie in at least one of the three. Define $T (a, b, y)$ to be the first of $(a, p)$ , $(p, q)$ , $(q, b)$ , in that fixed order, whose interval does not contain $y$ . This is a definition by cases on the three conditions $y \in [a, p]$ , $y \in [p, q]$ , $y \in [q, b]$ , so $T : I \times R \to I$ is a function and no choice is made.

step 1.2L4construct

3.1

Apply [L5] with $X = N \times I$ , $x_{0} = (0, (0, 1))$ , which lies in $X$ because $0 < 1$ by [L4], and $F (n, (a, b)) = (σ (n), T (a, b, f (n)))$ : this yields $h : N \to N \times I$ with $h (0) = x_{0}$ and $h (σ (n)) = F (h (n))$ . An induction using [L6] shows the first coordinate of $h (n)$ is $n$ , so we may write $h (n) = (n, (a_{n}, b_{n}))$ with $a_{n} < b_{n}$ , $a_{0} = 0$ , $b_{0} = 1$ and $(a_{σ (n)}, b_{σ (n)}) = T (a_{n}, b_{n}, f (n))$ for every $n$ . By step 2.1 this gives $a_{n} \leq a_{σ (n)}$ , $b_{σ (n)} \leq b_{n}$ and $f (n) \notin [a_{σ (n)}, b_{σ (n)}]$ .

step 1.1step 2.1L4L5L6construct

4.1

For $m \leq n$ one has $a_{m} \leq a_{n}$ and $b_{n} \leq b_{m}$ , by induction on $n$ using step 3.1 and transitivity; consequently $a_{m} \leq b_{n}$ for all $m, n$ : if $m \leq n$ then $a_{m} \leq a_{n} < b_{n}$ , and if $n \leq m$ then $a_{m} < b_{m} \leq b_{n}$ , and any two naturals are comparable by [L6].

step 3.1L4L6

5.1

The set $S = {a_{n} : n \in N}$ is nonempty and bounded above by $b_{0}$ by step 4.1, so [L1] gives its least upper bound $x = \sup S$ , unique by [L2].

step 3.1step 4.1L1L2

6.1

For every $n$ : $a_{n} \leq x$ , because $x$ is an upper bound of $S$ ; and $x \leq b_{n}$ , because otherwise $ε : = x - b_{n} > 0$ and [L3] would produce $a_{m} \in S$ with $b_{n} = x - ε < a_{m}$ , contradicting $a_{m} \leq b_{n}$ from step 4.1. Hence $x \in [a_{n}, b_{n}]$ for every $n$ .

step 4.1step 5.1L1L3L4

7.1

Fix $n \in N$ . By step 6.1 applied to $σ (n)$ , $x \in [a_{σ (n)}, b_{σ (n)}]$ , whereas $f (n) \notin [a_{σ (n)}, b_{σ (n)}]$ by step 3.1, so $x \neq f (n)$ . As $n$ was arbitrary, the real number $x$ is not a value of $f$ , contradicting the surjectivity of $f$ obtained in step 1.1. Therefore no surjection $N \to R$ exists and, $R$ being nonempty, [L7] makes $R$ uncountable.

step 1.1step 3.1step 6.1L7discharge-contradiction∎

Remarks

What the proof actually uses. Completeness enters once, at step 5.1, to produce $\sup {a_{n}}$ ; everything else is ordered-field arithmetic and the recursion theorem. The argument therefore applies verbatim to any ordered field with the least-upper-bound property, and it fails for $Q$ exactly because the supremum of the left endpoints need not exist there, which is as it should be, since $Q$ is countable ( $Q$ is countably infinite).
Why thirds and not halves. Two closed halves share the midpoint, so if $f (n)$ happens to be that midpoint then both halves contain it and the rule "take the first closed half not containing $f (n)$ " has nothing to return. Three closed thirds fix this: the first and the third are disjoint, so at least one of the three always misses $f (n)$ , and listing them in a fixed order makes the selection a definition by cases rather than a choice. Open intervals would avoid the overlap too, but closed intervals are what make step 6.1 work, since the point $\sup {a_{n}}$ must be allowed to be an endpoint.
The diagonal argument is not lost, only relocated. Cantor's theorem: $A ≺ P (A)$ , proved earlier on this page, is Cantor's diagonal argument in a setting where it needs nothing but the Power Set and Separation axioms. What is unavailable here is only the decimal diagonal, and only because decimal expansions are infinite series.
The choice-freeness matters beyond tidiness. The result remains available as a local ZF theorem in later arguments, including arguments that separately state a weak-choice hypothesis for assembling countable families.
The argument gives more than the statement does. Nothing above depends on the starting interval being $(0, 1)$ , so re-seeding the recursion inside a given interval shows that every nondegenerate interval, open or closed, is uncountable. That extension is Every nondegenerate interval of $R$ is uncountable, next on this page, where it is proved rather than asserted.

Depends on

Used by

…and 2 more results.

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

J. K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)
J. Lebl, Basic Analysis I (standard reference, not scraped)
Cantor's first set theory article (Wikipedia) (standard reference, not scraped)
Nested intervals (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 (standard reference, not scraped)

RR is uncountable (Cantor's nested intervals, 1874)