Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Every nondegenerate interval of R\mathbb{R} is uncountable

Statement

Let R\mathbb{R} be a complete ordered field (Complete ordered field (least-upper-bound property)) and let a,bRa, b \in \mathbb{R} with a<ba < b. Then both

  1. the closed interval [a,b]={xR:axb}[a,b] = \{\, x \in \mathbb{R} : a \le x \le b \,\}, and
  2. the open interval (a,b)={xR:a<x<b}(a,b) = \{\, x \in \mathbb{R} : a < x < b \,\}

are uncountable (Finite, countably infinite, countable, uncountable).

What this adds to R\mathbb{R} is uncountable (Cantor's nested intervals, 1874), and what it does not inherit from it. That theorem states exactly one thing: R\mathbb{R} is uncountable. Its statement says nothing about any interval, so the present result cannot be read off it. Its proof, on the other hand, is general in every part but its seed: the trisection rule of its step 2.1 is constructed there for an arbitrary (a,b)I(a,b) \in I, and its steps 4.1, 5.1 and 6.1, together with the interval reasoning of its step 7.1, use nothing about the starting interval beyond the nesting and the strictness an<bna_n < b_n that the rule delivers. Only three places are special to R\mathbb{R} and to (0,1)(0,1): the surjection of its step 1.1 is onto R\mathbb{R}, the recursion of its step 3.1 is seeded at (0,(0,1))(0,(0,1)), and the conclusion drawn in its step 7.1 is about R\mathbb{R}. So the construction is re-run below, seeded instead at the middle third of (a,b)(a,b), against a surjection onto (a,b)(a,b); the remarks record why that seed and not (a,b)(a,b) itself.

Facts & Assumptions

Given: A complete ordered field R\mathbb{R}, with 010 \ne 1 and the order of Ordered field. For uvu \le v write [u,v]={xR:uxv}[u,v] = \{\, x \in \mathbb{R} : u \le x \le v \,\} and (u,v)={xR:u<x<v}(u,v) = \{\, x \in \mathbb{R} : u < x < v \,\}, and write I={(u,v)R×R:u<v}I = \{\, (u,v) \in \mathbb{R} \times \mathbb{R} : u < v \,\} for the set of pairs coding nondegenerate closed intervals.

[L1]

Least-upper-bound property: every nonempty SRS \subseteq \mathbb{R} that is bounded above has a least upper bound supS\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 SS bounded above and an upper bound uu of SS, u=supSu = \sup S if and only if for every ε>0\varepsilon > 0 there is sSs \in S with uε<su - \varepsilon < s (Epsilon characterisation of the supremum).

[L4]

Order and arithmetic in an ordered field: 0<10 < 1 (The multiplicative identity is positive); a<ba < b implies a+c<b+ca + c < b + c, and a<ba < b with c<dc < d implies a+c<b+da + c < b + d (Order is preserved by adding a constant and by adding inequalities); a>0a > 0 implies a1>0a^{-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 XX, x0Xx_0 \in X and F:XXF : X \to X there is h:NXh : \mathbb{N} \to X with h(0)=x0h(0) = x_0 and h(σ(n))=F(h(n))h(\sigma(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\mathbb{N}); the order of N\mathbb{N} is the additive one, mnm \le n meaning m+k=nm + k = n for some kk (Order on the natural numbers, The natural numbers N\mathbb{N} (von Neumann)), and it satisfies n<σ(n)n < \sigma(n) and m<σ(n)    mnm < \sigma(n) \iff m \le n (On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n), so mσ(n)m \le \sigma(n) holds exactly when mnm \le n or m=σ(n)m = \sigma(n).

[L7]

A nonempty set is at most countable if and only if some surjection from N\mathbb{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\mathbb{N}, Finite, countably infinite, countable, uncountable).

[L8]

Every subset of an at most countable set is at most countable (Every subset of an at most countable set is at most countable).

Proof

technique · contradiction
1.1

Suppose, for contradiction, that the conclusion fails: there are a<ba < b in R\mathbb{R} for which [a,b][a,b] is at most countable or (a,b)(a,b) is at most countable. Fix such a pair. Since (a,b)[a,b](a,b) \subseteq [a,b], in the first case [L8] makes (a,b)(a,b) at most countable too, so in either case (a,b)(a,b) is at most countable.

assume-contraL7L8
1.2

Put 3:=1+1+13 := 1 + 1 + 1. Adding the inequality 0<10 < 1 to itself twice gives 3>03 > 0 by [L4], so 303 \ne 0 and 31>03^{-1} > 0; hence for d>0d > 0 the element d/3:=d31d/3 := d \cdot 3^{-1} is positive, and d/3+d/3+d/3=d313=dd/3 + d/3 + d/3 = d \cdot 3^{-1} \cdot 3 = d.

L4algebra
2.1

Fix the trisection rule. Let (u,v)I(u,v) \in I and yRy \in \mathbb{R}. Put d=vu>0d = v - u > 0, s=u+d/3s = u + d/3 and t=s+d/3t = s + d/3; then u<s<t<vu < s < t < v by step 1.2 and [L4], since su=ts=vt=d/3>0s - u = t - s = v - t = d/3 > 0. The three pairs (u,s)(u,s), (s,t)(s,t), (t,v)(t,v) all lie in II and their intervals are contained in [u,v][u,v]. Moreover [u,s][u,s] and [t,v][t,v] are disjoint, because xs<txx \le s < t \le x is impossible; so yy fails to lie in at least one of the three. Define T(u,v,y)T(u,v,y) to be the first of (u,s)(u,s), (s,t)(s,t), (t,v)(t,v), in that fixed order, whose interval does not contain yy. This is a definition by cases on the three conditions y[u,s]y \in [u,s], y[s,t]y \in [s,t], y[t,v]y \in [t,v], so T:I×RIT : I \times \mathbb{R} \to I is a function and no choice is made.

step 1.2L4construct
3.1

Trisect the fixed interval. Put d0=ba>0d_0 = b - a > 0, p=a+d0/3p = a + d_0/3 and q=p+d0/3q = p + d_0/3; then a<p<q<ba < p < q < b by step 1.2 and [L4], exactly as in step 2.1 applied to (a,b)(a,b). Hence (p,q)I(p,q) \in I, and [p,q](a,b)[p,q] \subseteq (a,b), since pxqp \le x \le q gives a<pxq<ba < p \le x \le q < b. In particular p(a,b)p \in (a,b), so (a,b)(a,b) is nonempty.

step 1.2L4
4.1

By step 1.1 the set (a,b)(a,b) is at most countable, and by step 3.1 it is nonempty, so [L7] provides a surjection g:N(a,b)g : \mathbb{N} \to (a,b). Composing with the inclusion (a,b)R(a,b) \subseteq \mathbb{R} regards gg as a function f:NRf : \mathbb{N} \to \mathbb{R} with f(n)=g(n)f(n) = g(n) for every nn.

step 1.1step 3.1L7
5.1

Apply [L5] with X=N×IX = \mathbb{N} \times I, x0=(0,(p,q))x_0 = (0, (p,q)), which lies in XX because p<qp < q by step 3.1, and F(n,(u,v))=(σ(n),T(u,v,f(n)))F(n, (u,v)) = (\sigma(n), T(u, v, f(n))): this yields h:NN×Ih : \mathbb{N} \to \mathbb{N} \times I with h(0)=x0h(0) = x_0 and h(σ(n))=F(h(n))h(\sigma(n)) = F(h(n)). An induction using [L6] shows the first coordinate of h(n)h(n) is nn, so we may write h(n)=(n,(an,bn))h(n) = (n, (a_n, b_n)) with an<bna_n < b_n, a0=pa_0 = p, b0=qb_0 = q and (aσ(n),bσ(n))=T(an,bn,f(n))(a_{\sigma(n)}, b_{\sigma(n)}) = T(a_n, b_n, f(n)) for every nn. By step 2.1 this gives anaσ(n)a_n \le a_{\sigma(n)}, bσ(n)bnb_{\sigma(n)} \le b_n and f(n)[aσ(n),bσ(n)]f(n) \notin [a_{\sigma(n)}, b_{\sigma(n)}].

step 2.1step 3.1step 4.1L4L5L6construct
6.1

For mnm \le n one has amana_m \le a_n and bnbmb_n \le b_m, by induction on nn using step 5.1 and transitivity; consequently ambna_m \le b_n for all m,nm, n: if mnm \le n then aman<bna_m \le a_n < b_n, and if nmn \le m then am<bmbna_m < b_m \le b_n, and any two naturals are comparable by [L6].

step 5.1L4L6
7.1

The set S={an:nN}S = \{\, a_n : n \in \mathbb{N} \,\} is nonempty and bounded above by b0b_0 by step 6.1, so [L1] gives its least upper bound x=supSx = \sup S, unique by [L2].

step 5.1step 6.1L1L2
8.1

For every nn: anxa_n \le x, because xx is an upper bound of SS; and xbnx \le b_n, because otherwise ε:=xbn>0\varepsilon := x - b_n > 0 and [L3] would produce amSa_m \in S with bn=xε<amb_n = x - \varepsilon < a_m, contradicting ambna_m \le b_n from step 6.1. Hence x[an,bn]x \in [a_n, b_n] for every nn.

step 6.1step 7.1L1L3L4
9.1

Taking n=0n = 0 in step 8.1 gives x[a0,b0]=[p,q]x \in [a_0, b_0] = [p, q], and [p,q](a,b)[p,q] \subseteq (a,b) by step 3.1, so x(a,b)x \in (a,b). Fix nNn \in \mathbb{N}: by step 8.1 applied to σ(n)\sigma(n), x[aσ(n),bσ(n)]x \in [a_{\sigma(n)}, b_{\sigma(n)}], whereas f(n)[aσ(n),bσ(n)]f(n) \notin [a_{\sigma(n)}, b_{\sigma(n)}] by step 5.1, so xf(n)=g(n)x \ne f(n) = g(n). As nn was arbitrary, the element xx of (a,b)(a,b) is not a value of gg, contradicting the surjectivity of gg obtained in step 4.1. So no such pair a<ba < b exists: for every a<ba < b both [a,b][a,b] and (a,b)(a,b) fail to be at most countable, that is, both are uncountable by [L7].

step 3.1step 4.1step 5.1step 8.1L7discharge-contradiction

Remarks

  • Which route this proof takes, and why. The extension is obtained by re-running the construction of R\mathbb{R} is uncountable (Cantor's nested intervals, 1874) with a new seed, not by transporting uncountability along a bijection. The reason is that there is nothing to transport: the theorem states that R\mathbb{R} is uncountable and nothing more, and no item of this library states that [0,1][0,1] is uncountable, so the affine order-isomorphism ta+t(ba)t \mapsto a + t(b-a) from [0,1][0,1] onto [a,b][a,b] has no uncountable source to carry across. Re-running is available instead precisely because the theorem's proof is already general: its step 2.1 builds the trisection rule TT for an arbitrary (a,b)I(a,b) \in I, and its steps 4.1 to 7.1 quote only the nesting anaσ(n)a_n \le a_{\sigma(n)}, bσ(n)bnb_{\sigma(n)} \le b_n, the strictness an<bna_n < b_n and the omission f(n)[aσ(n),bσ(n)]f(n) \notin [a_{\sigma(n)}, b_{\sigma(n)}]. Its step 1.1, the seed of its step 3.1 and the conclusion of its step 7.1 are the special ones, and they are the three replaced here: a surjection onto (a,b)(a,b) rather than onto R\mathbb{R}, the seed (0,(p,q))(0,(p,q)) rather than (0,(0,1))(0,(0,1)), and a conclusion about the interval rather than about R\mathbb{R}.
  • A corollary of the argument, not of the statement. That distinction is the whole content of the previous remark, and it is why the proof is written out here in full rather than replaced by a citation. A fact of the form "for every (a,b)I(a,b) \in I and every f:NRf : \mathbb{N} \to \mathbb{R} there is x[a,b]x \in [a,b] omitted by ff" is true and is what the theorem's proof establishes, but it is not what the theorem says, so quoting the theorem for it would be an attribution the theorem does not support.
  • Why the seed is the middle third and not (a,b)(a,b) itself. The point produced by the construction is a supremum of left endpoints, so it may be an endpoint of the starting interval; seeding at (a,b)(a,b) would therefore only place xx in the closed interval [a,b][a,b], which settles claim 1 but not claim 2. Seeding at (p,q)(p,q), the middle third, costs nothing and gives x[p,q](a,b)x \in [p,q] \subseteq (a,b), so the open case comes out directly and the closed case follows from it, since (a,b)[a,b](a,b) \subseteq [a,b] and a subset of an at most countable set is at most countable (Every subset of an at most countable set is at most countable). The naive order of the two claims is thus reversed: the open interval is the substantive one.
  • What the proof uses. Exactly what R\mathbb{R} is uncountable (Cantor's nested intervals, 1874) uses, and nothing else: ordered-field arithmetic, the recursion theorem (The recursion theorem), and completeness at exactly one point, step 7.1 above, where sup{an}\sup\{a_n\} is produced. In particular the construction still makes no choices, for the same reason as there, namely that the three closed thirds are tried in a fixed order and the first and third are disjoint. The result consequently fails for Q\mathbb{Q}, where the intervals with rational endpoints are countable, and it must, since the supremum taken in step 7.1 above need not exist there.
  • Degeneracy is the only exclusion. The hypothesis a<ba < b cannot be weakened: [a,a]={a}[a,a] = \{a\} is finite and (a,a)=(a,a) = \varnothing is finite, so both are at most countable. Every interval that is not a single point or empty contains a nondegenerate open interval, so this corollary gives the uncountability of the half-open and unbounded intervals as well, again by Every subset of an at most countable set is at most countable.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 55 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources