The real numbers are an ordered field with the least upper bound property: every nonempty set bounded above has a supremum. This single axiom separates the reals from the rationals and makes calculus possible.
The axioms of an ordered field
The reals satisfy the field axioms (addition, multiplication, inverses) and the order axioms (trichotomy, transitivity, compatibility with arithmetic). The rationals satisfy these too. What sets the reals apart is one more axiom.
Scheme
; The field axioms in action; Commutativity, associativity, distributivity, inverses
(display "Commutativity: 3 + 5 = ")
(display (+ 35))
(display ", 5 + 3 = ")
(display (+ 53)) (newline)
(display "Associativity: (2+3)+4 = ")
(display (+ (+ 23) 4))
(display ", 2+(3+4) = ")
(display (+ 2 (+ 34))) (newline)
(display "Distributivity: 2*(3+4) = ")
(display (* 2 (+ 34)))
(display ", 2*3 + 2*4 = ")
(display (+ (* 23) (* 24))) (newline)
; Order: trichotomy
(define (trichotomy a b)
(cond ((< a b) "a < b")
((= a b) "a = b")
(else"a > b")))
(display "trichotomy(3, 5) = ")
(display (trichotomy 35))
A set S of reals is bounded above if some number M satisfies x ≤ M for all x in S. The supremum (least upper bound) is the smallest such M. The completeness axiom says: every nonempty bounded-above subset of the reals has a supremum in the reals. The rationals fail this. The set of rationals whose square is less than 2 is bounded above, but its supremum is √2, which is not rational.
Scheme
; Supremum: the least upper bound; S = rationals p such that p^2 < 2; sup S = sqrt(2), which is irrational; Approximate sup by bisection
(define (find-sup low high steps)
(if (= steps 0)
(/ (+ low high) 2.0)
(let ((mid (/ (+ low high) 2.0)))
(if (< (* mid mid) 2)
(find-sup mid high (- steps 1))
(find-sup low mid (- steps 1))))))
(define approx-sqrt2 (find-sup 1.02.050))
(display "Approximate sup{p in Q : p^2 < 2} = ")
(display approx-sqrt2) (newline)
(display "approx^2 = ")
(display (* approx-sqrt2 approx-sqrt2)) (newline)
; sqrt(2) is irrational: no fraction p/q in lowest; terms satisfies p^2 = 2*q^2 (parity argument)
(display "The completeness axiom guarantees sqrt(2) exists in R")
The Archimedean property says: for any real x, there exists a natural number n with n > x. No real number is infinite. A consequence: between any two distinct reals lies a rational number (density of Q in R). The rationals are dense, yet they have "holes" that the completeness axiom fills.
Scheme
; Archimedean property: for any x, there exists n > x
(define (archimedean x)
(let loop ((n 1))
(if (> n x) n (loop (+ n 1)))))
(display "Archimedean: n > 3.7 => n = ")
(display (archimedean 3.7)) (newline)
(display "Archimedean: n > 100.1 => n = ")
(display (archimedean 100.1)) (newline)
; Density of Q: between any two reals, find a rational p/q; Given a < b, pick n with 1/n < b-a, then find m with m/n in (a,b)
(define (rational-between a b)
(let* ((n (archimedean (/ 1.0 (- b a))))
(m (+ 1 (floor (* a n)))))
(/ m n)))
(define r (rational-between 1.411.42))
(display "Rational between 1.41 and 1.42: ")
(display (exact->inexact r))
Python
# Python equivalentimportmathdef archimedean(x):
n = 1while n <= x:
n += 1return n
print("Archimedean: n > 3.7 => n =", archimedean(3.7))
print("Archimedean: n > 100.1 => n =", archimedean(100.1))
def rational_between(a, b):
n = archimedean(1.0 / (b - a))
m = 1 + math.floor(a * n)
return m / n
r = rational_between(1.41, 1.42)
print("Rational between 1.41 and 1.42:", r)
Infimum and the completeness of lower bounds
The infimum (greatest lower bound) is the dual of supremum. Every nonempty set bounded below has an infimum. You don't need a separate axiom: if S is bounded below, then the set of negations -S is bounded above, and inf S = -sup(-S).
Scheme
; Infimum from supremum via negation; inf S = -sup(-S); S = {1/n : n = 1,2,3,...}; S is bounded below by 0; inf S = 0 (but 0 is not in S)
(define (partial-inf-search n terms)
(if (= terms 0) n
(let ((val (/ 1.0 terms)))
(if (< val n)
(partial-inf-search val (- terms 1))
(partial-inf-search n (- terms 1))))))
(display "min of first 100 terms of {1/n}: ")
(display (partial-inf-search 999.0100)) (newline)
(display "min of first 10000 terms: ")
(display (partial-inf-search 999.010000)) (newline)
(display "inf{1/n : n >= 1} = 0 (limit, not attained)")
Python
# Python equivalent# inf of {1/n : n >= 1}for count in [100, 10000]:
terms = [1/n for n inrange(1, count + 1)]
print("min of first " + str(count) + " terms of 1/n:", min(terms))
print("inf{1/n : n >= 1} = 0 (limit, not attained)")
Notation reference
Symbol
Scheme
Meaning
sup S
(find-sup ...)
Least upper bound of S
inf S
-sup(-S)
Greatest lower bound of S
N, Z, Q, R
number types
Naturals, integers, rationals, reals
x ≤ M for all x in S
(bounded-above? S M)
M is an upper bound of S
√2 ∉ Q
parity argument
sqrt(2) is irrational
Neighbors
Discrete Math — proof techniques (induction, contradiction) used throughout
📐 Calculus Ch.3 — limits in calculus depend on the completeness of the reals
📝 Proofs Ch.3 — proof by contradiction: used to prove the irrationality of √2
Translation notes
Floating-point arithmetic is not the reals. Our bisection for √2 converges to a float, not an exact real. The completeness axiom is about the mathematical structure, not any computer representation. The irrationality proof of √2 is a proof by contradiction that can't be "run" in the REPL.