02.02.01 · analysis / real-numbers

Real-number axioms (ordered field)

shipped3 tiersLean: partialpending prereqs

Anchor (Master): Hilbert *Grundlagen der Geometrie* (1899) §13–§17; Apostol Ch. 3; Bourbaki *Topologie Générale* Ch. IV; Tarski 1948

Intuition [Beginner]

The real numbers are "all the numbers on the line" — every whole number, every fraction, every decimal that does not terminate, every length you could measure with an arbitrarily fine ruler. Picture the number line stretching out in both directions, with $0$ in the middle and the marks at $1, 2, 3, \dots$ going one way and $- 1, - 2, - 3, \dots$ going the other. The real numbers fill in everything in between.

To do calculus on this line we need a precise list of properties to reason from. Mathematicians distilled those properties into a list of $13$ rules. Nine of them say how addition and multiplication behave; three say how the ordering $<$ behaves; one says that the line has no holes. These $13$ rules are enough to recover every fact about real numbers without ever needing to construct them out of fractions or decimals.

The single rule that makes this list special is the $13$ th, the completeness rule. It says that any non-empty collection of real numbers that has some upper bound also has a smallest upper bound, sitting on the line. That rule is what guarantees the line really has no missing points — and it is the reason limits, integrals, and continuous curves all behave the way you expect.

Visual [Beginner]

The number line, with marks at $0, 1, 2, 3$ , alongside three boxes naming the three families of rules: $9$ field axioms (closure, associativity, commutativity, identities, inverses, distributivity), $3$ order axioms (trichotomy, transitivity, compatibility with $+$ and $\times$ ), and $1$ completeness axiom (every bounded-above non-empty subset has a least upper bound).

The first two boxes hold for the rationals as well; the third is what distinguishes the real line from the rational line. The rationals have holes — the point named $2$ is missing, even though arbitrarily good rational upper and lower bounds exist for it. Completeness rules out exactly that kind of hole.

Worked example [Beginner]

Take the specific subset $S = {x : x^{2} < 2}$ of real numbers — every real number whose square is less than $2$ . This set contains $0$ , $1$ , and $1.4$ but not $2$ (since $4 > 2$ ). The number $2$ is an upper bound of $S$ , and so is $1.5$ , and so is $1.42$ . The completeness rule says there is a least upper bound for $S$ in the real line.

That least upper bound is the number we call $2$ . Its square is exactly $2$ . We can pin it down to any decimal precision: the digit $1.4142 \dots$ comes from approaching the least upper bound from below. The same set $S$ inside the rationals has no smallest rational upper bound — every rational upper bound has a smaller rational upper bound, since $2$ is irrational. What this tells us: completeness in the real line is what supplies the number $2$ in the first place. Without it, the equation $x^{2} = 2$ has no solution.

Check your understanding [Beginner]

Formal definition [Intermediate+]

A complete ordered field is a set $F$ equipped with binary operations $+, \cdot$ , a relation $<$ , and distinguished elements $0, 1$ satisfying the following thirteen axioms.

Field axioms (nine axioms governing $+$ and $\cdot$ ).

(F1) Closure: $a + b \in F$ and $a \cdot b \in F$ for all $a, b \in F$ . (F2) Associativity: $(a + b) + c = a + (b + c)$ and $(a \cdot b) \cdot c = a \cdot (b \cdot c)$ . (F3) Commutativity: $a + b = b + a$ and $a \cdot b = b \cdot a$ . (F4) Identity elements: there exist $0, 1 \in F$ with $0 \neq = 1$ , $a + 0 = a$ , and $a \cdot 1 = a$ . (F5) Additive inverse: for every $a \in F$ , there exists $- a \in F$ with $a + (- a) = 0$ . (F6) Multiplicative inverse: for every $a \in F$ with $a \neq = 0$ , there exists $a^{- 1} \in F$ with $a \cdot a^{- 1} = 1$ . (F7) Distributivity: $a \cdot (b + c) = a \cdot b + a \cdot c$ .

(F1)–(F3) factor as three statements each per operation, giving the count of nine; (F4)–(F7) collectively give the rest. This packaging follows Apostol ^{[Apostol Ch. 3 §3.2]}.

Order axioms (three axioms governing $<$ ).

(O1) Trichotomy: for any $a, b \in F$ , exactly one of $a < b$ , $a = b$ , $b < a$ holds. (O2) Transitivity: if $a < b$ and $b < c$ , then $a < c$ . (O3) Compatibility: if $a < b$ , then $a + c < b + c$ for all $c$ ; and if $a < b$ and $0 < c$ , then $a \cdot c < b \cdot c$ .

A field satisfying (F1)–(F7) and (O1)–(O3) is an ordered field ^{[Apostol Ch. 3 §3.5]}.

Completeness axiom (one axiom).

(C) Least-upper-bound property: every non-empty subset $S \subseteq F$ that is bounded above admits a least upper bound $sup S \in F$ .

A least upper bound of $S$ is an element $α \in F$ satisfying (i) $s \leq α$ for every $s \in S$ and (ii) for every $α^{'} < α$ , some $s \in S$ has $s > α^{'}$ . Apostol calls this Axiom 11; equivalent formulations are Cauchy completeness plus the Archimedean property, the nested-interval property, and the monotone-convergence theorem ^{[Rudin Ch. 1]}.

A field satisfying (F1)–(F7), (O1)–(O3), and (C) is a complete ordered field. The real numbers $R$ are taken as the canonical model. The natural numbers $N \subseteq R$ are the smallest subset containing $1$ and closed under $+ 1$ ; integers, rationals, and irrationals are then defined inside $R$ .

Counterexamples to common slips.

(O3) is one axiom in two parts. Some textbooks split positivity preservation by $+$ and by $\times$ into two separate axioms; the count $13$ used here folds them together. The mathematics is the same either way.
The rationals satisfy (F1)–(F7) and (O1)–(O3). They fail only (C). The set ${x \in Q : x^{2} < 2}$ is non-empty and bounded above by $2$ , yet has no rational supremum.
A "complete" lattice is not the same as (C). Order-theoretic completeness in lattice theory requires every subset to have a sup; (C) requires only non-empty bounded-above subsets, and the empty set is excluded.
(C) is not implied by Archimedean alone. The Archimedean property holds in $Q$ , but (C) does not. The non-standard reals $^{*} R$ are the converse failure: complete in a non-Archimedean sense, but not Archimedean.

Key theorem with proof [Intermediate+]

Theorem (Archimedean property). Let $F$ be a complete ordered field with natural numbers $N \subseteq F$ . Then for every $x \in F$ there exists $n \in N$ with $n > x$ .

Proof. Suppose for contradiction that some $x \in F$ satisfies $n \leq x$ for every $n \in N$ . Then $N$ is non-empty (it contains $1$ by (F4)) and bounded above (by $x$ ). By the completeness axiom (C), $N$ has a least upper bound $α = sup N \in F$ .

The element $α - 1 \in F$ satisfies $α - 1 < α$ (using (O3) with $- 1 < 0$ ). By the defining property of the supremum, $α - 1$ is not an upper bound of $N$ , so some $n_{0} \in N$ has $n_{0} > α - 1$ . Adding $1$ to both sides via (O3) gives $n_{0} + 1 > α$ . But $n_{0} + 1 \in N$ (the naturals are closed under $+ 1$ ), contradicting the assumption that $α$ is an upper bound of $N$ .

Hence the assumption fails: for every $x \in F$ , some $n \in N$ satisfies $n > x$ . $□$

Bridge. The Archimedean property builds toward 02.02.02 pending (sup and inf), 02.03.01 pending (sequence convergence and the monotone convergence theorem), and the entire $ε$ -machinery of single-variable analysis: it is the rule that lets you make $1/ n$ arbitrarily small, and so it is the rule that lets you turn supremum-style statements into $ε$ -style statements. The same proof technique — "if $sup S$ exists, then $sup S - ε$ is not an upper bound, so some element of $S$ beats it" — appears again in the proof that continuous functions on $[a, b]$ attain their extrema, in the proof of the intermediate value theorem, and in 02.04.04 pending (FTC). The completeness axiom is the foundational reason that limits, integrals, and continuous curves all behave the way calculus assumes; the Archimedean property is the smallest visible consequence of completeness, and it is the consequence that powers every later $ε$ - $N$ argument. Putting these together, completeness identifies $R$ as the unique ordered field in which calculus, as ordinarily practised, is a theorem rather than an article of faith.

Exercises [Intermediate+]

Exercise 5 (medium, short-answer).

Prove the existence of $n$ -th roots of positive reals: for every $a > 0$ and every $n \in N$ , there exists $x > 0$ with $x^{n} = a$ .

Hint

Take the sup of ${t > 0 : t^{n} < a}$ and use the order axioms to rule out $x^{n} < a$ and $x^{n} > a$ .

Answer

Let $S = {t > 0 : t^{n} < a}$ . The set $S$ is non-empty (it contains a small positive $t$ with $t^{n} < a$ , found by Archimedean) and bounded above (by $max (1, a)$ , since $t > max (1, a)$ forces $t^{n} > a$ ). By (C), $x = sup S$ exists in $R$ . The trichotomy axiom gives three cases for $x^{n}$ versus $a$ : if $x^{n} < a$ , choose $ε > 0$ small enough using the Archimedean property to make $(x + ε)^{n} < a$ , contradicting that $x$ is an upper bound; if $x^{n} > a$ , similarly $(x - ε)^{n} > a$ for small $ε > 0$ , contradicting that $x$ is the least upper bound. Hence $x^{n} = a$ . Rubric: full credit for the sup construction and the trichotomy argument; partial credit for one direction of the contradiction.

Exercise 6 (hard, short-answer).

Show that the completeness axiom (C) is equivalent (over the ordered-field axioms (F1)–(F7) and (O1)–(O3) plus the Archimedean property) to the monotone convergence theorem: every monotonically increasing sequence of real numbers that is bounded above converges.

Hint

For one direction, use $sup_{n} a_{n}$ as the limit. For the other, given a non-empty bounded-above set $S$ , build an increasing sequence approaching $sup S$ from below.

Answer

(C) implies MCT: given an increasing bounded-above sequence $(a_{n})$ , set $α = sup_{n} {a_{n}}$ , which exists by (C). For every $ε > 0$ , $α - ε$ is not an upper bound, so some $N$ has $a_{N} > α - ε$ ; monotonicity gives $a_{n} > α - ε$ for all $n \geq N$ , while $a_{n} \leq α$ always, so $∣ a_{n} - α ∣ < ε$ . Conversely, MCT plus Archimedean implies (C): given a non-empty bounded-above $S$ , build an increasing sequence $(s_{k})$ in $S$ converging up to a candidate $β$ by repeatedly halving the gap to a fixed upper bound; the limit $β$ is then an upper bound (every $s \in S$ has $s \leq s_{k}$ for arbitrarily large $k$ , by the construction) and the least one (any smaller $β^{'} < β$ is exceeded by $s_{k}$ for large $k$ ). Rubric: full credit for both directions of the equivalence.

Exercise 7 (hard, short-answer).

Exhibit an ordered field that satisfies (F1)–(F7), (O1)–(O3), and the Archimedean property but fails the completeness axiom (C). Explain which axiom your example violates and how.

Hint

The simplest example is the rationals.

Answer

The field $Q$ of rationals is an ordered field (it satisfies (F1)–(F7) and (O1)–(O3)) and is Archimedean (for every rational $x$ , there is a rational integer $n > x$ , by setting $n$ equal to the integer part plus one). It fails (C): the set $S = {x \in Q : x^{2} < 2}$ is non-empty (contains $1$ ) and bounded above (by $2$ ), but has no rational supremum, since the only candidate is $2 \in / Q$ . So (C) is genuinely independent of the other axioms, and the rationals are the model that demonstrates this. Rubric: full credit for naming $Q$ and producing a witness set.

Lean formalization [Intermediate+]

lean_status: partial — Mathlib provides the complete-ordered-field structure on $R$ via LinearOrderedField, the conditionally complete order via ConditionallyCompleteLinearOrderedField, and the Archimedean property via the Archimedean typeclass. The categoricity statement (any two complete ordered fields are uniquely order-isomorphic) is left as a Codex-facing placeholder, since Mathlib has the pieces but not a single packaged theorem.

[object Promise]

The companion module at Codex.Analysis.RealNumbers.Axioms re-exports these instances and records the categoricity gap.

Advanced results [Master]

The thirteen-axiom presentation introduced by Hilbert in Grundlagen der Geometrie §13–§17 ^{[Hilbert 1899]} is categorical: the axiom system has a model, and any two models are uniquely isomorphic. The proof is constructive in the meta-theory, going through the order structure and the supremum operation.

Theorem (categoricity of the complete ordered field). Let $F, F^{'}$ be complete ordered fields. There exists a unique order-preserving field isomorphism $φ : F \to F^{'}$ .

Proof sketch. Define $φ$ on the natural numbers $N \subseteq F$ by sending $1_{F}$ to $1_{F^{'}}$ and extending by $φ (n + 1) = φ (n) + 1_{F^{'}}$ ; extend to $Z$ by $φ (- n) = - φ (n)$ and to $Q$ by $φ (m / n) = φ (m) \cdot φ (n)^{- 1}$ . The Archimedean property in both fields ensures that for every $a \in F$ , the set $L_{a} = {q \in Q : q < a}$ is non-empty and bounded above (by any $n \in N$ with $n > a$ ), and similarly $φ (L_{a}) \subseteq Q \subseteq F^{'}$ is non-empty and bounded above. Define $φ (a) = sup_{F^{'}} φ (L_{a})$ , which exists by completeness in $F^{'}$ . Verification that $φ$ preserves $+$ , $\cdot$ , $<$ proceeds by an $ε$ -argument using the rational lower-set characterisation; uniqueness follows because any order-preserving field map fixes $Q$ and the rational lower-sets determine each $a$ .

Theorem (independence of axioms). Each of the thirteen axioms is independent of the others: for each axiom $A_{i}$ , there is a structure satisfying every axiom except $A_{i}$ .

The witnessing models, classical:

(F6) inverse fails: $Z$ with $+, \cdot, <$ satisfies all order axioms and all field axioms except multiplicative inverse, since $2$ has no integer inverse.
(O1) trichotomy fails: $C$ with field operations and a partial order such as the lexicographic order on $(ℜ, ℑ)$ satisfies (F1)–(F7) but no order can be defined that makes $C$ an ordered field, because $i^{2} = - 1$ would force $- 1 > 0$ in any order with (O3).
(O3) compatibility fails: define the field $Q$ with the reverse order; then $1 < 0$ , but $0 < - 1$ as well, breaking (O3).
(C) completeness fails: $Q$ , as in Exercise 7. The non-standard reals $^{*} R$ of Robinson ^{[Robinson 1966]} are an ordered field satisfying (F1)–(F7), (O1)–(O3), and a non-Archimedean form of completeness, exhibiting that "Archimedean + Cauchy-complete" decomposes (C) further.

Theorem (Tarski 1948 — decidability of the elementary theory). The first-order theory of real closed fields is decidable: there is an algorithm that, given a sentence in the language ${+, \cdot, <, 0, 1}$ , decides whether it holds in $R$ ^{[Tarski 1948]}.

This theorem stands in contrast to Gödel-incompleteness for $N$ : the natural numbers' first-order theory is undecidable, while the reals' is decidable. The reason is that real closed fields admit quantifier elimination — every formula reduces to a Boolean combination of polynomial equalities and inequalities — whereas $N$ does not, due to the discrete-counting structure that supports Gödel-coding.

Theorem (constructive completeness, Bishop-Bridges). There is a development of analysis in which the real numbers $R_{c}$ are defined constructively (e.g., as Cauchy sequences of rationals with explicit modulus), the field operations are computable, and a constructive form of completeness holds — but classical least-upper-bound completeness, requiring the law of the excluded middle (LEM), does not ^{[Bishop 1967]}.

The constructive reals $R_{c}$ satisfy (F1)–(F7), (O1)–(O3), and Cauchy completeness as a constructive theorem; the classical sup-statement (C) is a non-constructive consequence available only after assuming LEM. The constructive theory recovers most of single-variable analysis — the intermediate value theorem in the form "for any $ε > 0$ there exists $c$ with $∣ f (c) ∣ < ε$ " — while certain classical theorems (least upper bound of an arbitrary inhabited bounded set, full IVT with $f (c) = 0$ ) require strictly classical reasoning.

Adjacent axiomatisations. The thirteen-axiom version is the standard for textbook calculus. Equivalent reformulations include:

Cauchy completeness plus Archimedean: replace (C) by "every Cauchy sequence converges" plus the Archimedean property. Cauchy completeness alone is strictly weaker than (C).
Nested-interval property: every nested sequence of closed bounded intervals $[a_{n}, b_{n}]$ with $b_{n} - a_{n} \to 0$ has non-empty intersection.
Monotone convergence: every monotonically increasing bounded-above sequence converges (Exercise 6).
Bolzano-Weierstrass: every bounded sequence has a convergent subsequence.

Each is equivalent to (C) over (F1)–(F7), (O1)–(O3) plus Archimedean, and each emphasises a different perspective: completeness is a statement about subsets, Cauchy completeness is about sequences, nested intervals is about intervals, monotone convergence is about ordered sequences, Bolzano-Weierstrass is about boundedness.

Synthesis. The Hilbert-Apostol thirteen-axiom presentation identifies $R$ uniquely up to isomorphism by capturing arithmetic, ordering, and the absence of holes in a single list. The Archimedean property is the smallest visible consequence of completeness and the engine of every $ε$ -argument in analysis; categoricity is what licenses the calculus textbook to speak of "the" real numbers without specifying a construction. Taking these together identifies $R$ as the unique structure on which single-variable calculus can be developed without ambiguity — Cauchy sequences, Riemann integrals, and FTC all become theorems in this structure, and the uniqueness up to isomorphism means the choice between Dedekind cuts, Cauchy completion, decimal expansions, or any other model of (F1)–(F7), (O1)–(O3), (C) is mathematically inert. The constructive variant exhibits that the classical theory factorises further: an intuitionistic core handles computable analysis, while LEM-dependent extensions handle the supremum operation in full generality. The axioms appear again in 02.02.02 pending (sup and inf), 02.03.01 pending (sequence convergence), and 02.04.04 pending (FTC); the structure builds toward the entire single-variable analysis strand and through it to functional analysis 02.11.04 and beyond.

Full proof set [Master]

Proposition (uniqueness of identity elements). In any field $F$ , the additive and multiplicative identity elements are uniquely determined by (F4).

Proof. Suppose $0$ and $0^{'}$ both satisfy (F4): $a + 0 = a$ and $a + 0^{'} = a$ for every $a$ . Take $a = 0^{'}$ in the first equation: $0^{'} + 0 = 0^{'}$ . Take $a = 0$ in the second: $0 + 0^{'} = 0$ . By (F3), $0 + 0^{'} = 0^{'} + 0$ , so $0 = 0^{'}$ . The argument for multiplicative identity is identical. $□$

Proposition (Archimedean property). Proved in §"Key theorem with proof" above.

Proposition (density of $Q$ in $R$ ). For every $a, b \in R$ with $a < b$ , there exists $q \in Q$ with $a < q < b$ .

Proof. By Archimedean, choose $n \in N$ with $n > 1/ (b - a)$ , equivalently $1/ n < b - a$ . Choose $m \in Z$ to be the smallest integer with $m > na$ . Then $m - 1 \leq na$ , so $m \leq na + 1 < na + n (b - a) = nb$ . Dividing by $n > 0$ via (O3), $a < m / n < b$ , and $q = m / n \in Q$ . $□$

Proposition (existence of $n$ -th roots of positive reals). For every $a > 0$ and every $n \in N$ , there exists a unique $x > 0$ with $x^{n} = a$ .

Proof. Existence is in Exercise 5. Uniqueness: if $x_{1}, x_{2} > 0$ both satisfy $x_{i}^{n} = a$ with, say, $x_{1} < x_{2}$ by trichotomy, then $x_{1}^{n} < x_{2}^{n}$ by repeated application of (O3), so $a < a$ , a contradiction. Hence $x_{1} = x_{2}$ . $□$

Proposition (categoricity of complete ordered fields). Stated in §"Advanced results"; full proof via the Cauchy-cut construction of $φ$ on the rationals followed by sup-extension is in Bourbaki, Topologie Générale Ch. IV §8. ^{[Bourbaki Ch. IV]}

Proposition (uncountability of $R$ ). The set $R$ is uncountable.

Proof (Cantor's diagonal, sup form). Suppose for contradiction that an enumeration $r_{1}, r_{2}, r_{3}, \dots$ of $R$ exists. Recursively construct a nested sequence of closed intervals $I_{k} = [a_{k}, b_{k}]$ with $r_{k} \in / I_{k}$ and $b_{k} - a_{k} = (b_{1} - a_{1}) / 3^{k - 1}$ : at each step, divide the current interval into three equal closed sub-intervals and pick one that excludes $r_{k}$ . The interval lengths tend to zero by Archimedean. The intersection $⋂_{k} I_{k}$ is non-empty by the nested-interval property (equivalent to (C)) — let $r$ be in it. Then $r \in I_{k}$ for every $k$ , so $r \neq = r_{k}$ for every $k$ , contradicting that the enumeration is exhaustive. Hence no enumeration exists. $□$

Connections [Master]

Sup and inf 02.02.02 pending (pending) — the supremum and infimum constructions formalised in the axiom (C) are taken further in the next unit, where the symmetry between sup and inf, the connection to limits, and the limsup / liminf operations are developed. The completeness axiom is the foundational reason both operations land inside $R$ .
Sequence convergence and the monotone convergence theorem 02.03.01 pending (pending) — the $ε$ - $N$ definition of sequence convergence is a translation of the supremum-style statement in (C) into the language of sequences. The MCT is equivalent to (C) over the ordered-field axioms plus Archimedean (Exercise 6); the entire sequence-and-series strand of analysis builds on this equivalence.
Cauchy sequences and Bolzano-Weierstrass 02.03.02 (pending) — Cauchy completeness, equivalent to (C) plus Archimedean, is the alternative formulation of completeness used in the metric-space generalisation 02.01.05. Bolzano-Weierstrass — every bounded sequence has a convergent subsequence — is a further reformulation of (C) tied to compactness.
Fundamental theorems of calculus 02.04.04 pending (pending) — the existence of $\int_{a}^{b} f$ for continuous $f$ on a compact interval relies on uniform continuity, which itself relies on the extreme value theorem, which relies on (C). The chain of dependencies makes (C) the foundational input to FTC.
Field 01.01.01 — the field axioms (F1)–(F7) are the general-field axioms restricted to the ordered case. The vector-space and module theory of 01.01.* takes (F1)–(F7) over an arbitrary field as a starting point; specialising to $R$ adds the order and completeness axioms.
Metric space 02.01.05 — every metric space has a Cauchy completion, generalising the classical construction of $R$ from $Q$ . The metric-space framework is the topological generalisation of the Cauchy-completeness reformulation of (C).
Banach space 02.11.04 — a complete normed vector space generalises the completeness axiom from a single line to an infinite-dimensional setting; the proof patterns ("sup of a bounded set", "limit of a Cauchy sequence", "intersection of nested closed balls") all originate in the calculus-textbook treatment of $R$ presented here.

Historical & philosophical context [Master]

David Hilbert gave the first complete axiomatic presentation of $R$ as a complete ordered field in Grundlagen der Geometrie (1899) ^{[Hilbert 1899]}, §13–§17, where the Vollständigkeitsaxiom (completeness axiom) was added to the ordered-field axioms to single out the real line uniquely. Hilbert framed the axiom as a maximality requirement: no proper extension of the structure can satisfy all the previous axioms. The least-upper-bound formulation, equivalent under the other axioms, became the standard textbook version after Landau's Grundlagen der Analysis (1930) and Bourbaki's Topologie Générale (1940-) ^{[Bourbaki Ch. IV]}.

The pedagogical deployment in Apostol's Calculus Vol. 1 (1967) ^{[Apostol Ch. 3]} crystallised the thirteen-axiom presentation as the canonical entry point for proof-based first-year calculus. Apostol's choice — to axiomatise $R$ rather than construct it from $Q$ via Dedekind cuts (Dedekind 1872) or Cauchy completion (Cantor 1872) — reflects an editorial decision that the construction is a meta-theorem about consistency, not a prerequisite for using the axioms.

Tarski's 1948 result ^{[Tarski 1948]} that the first-order theory of real closed fields is decidable, by quantifier elimination, sits in productive tension with Gödel-incompleteness for $N$ : arithmetic is undecidable, real-arithmetic is decidable, and the boundary is exactly the discrete-counting structure that supports Gödel-coding. Robinson's 1966 Non-standard Analysis ^{[Robinson 1966]} introduced the hyperreals $^{*} R$ , a non-Archimedean ordered-field extension in which infinitesimals are first-class; by relaxing the Archimedean consequence of (C), one recovers Leibniz-style infinitesimal calculus on rigorous foundations. Bishop's 1967 Foundations of Constructive Analysis ^{[Bishop 1967]} developed analysis without LEM, exhibiting that the LUB formulation of (C) is genuinely classical while Cauchy completeness is intuitionistically valid.

Bibliography [Master]

[object Promise]

Prerequisites

00.01.01 pending

Tier anchors

beginner: Strogatz — *Infinite Powers* (number-line intuition); 3Blue1Brown style framing
intermediate: Apostol *Calculus* Vol. 1 Ch. 3 §3.1–3.7; Rudin *Principles of Mathematical Analysis* Ch. 1
master: Hilbert *Grundlagen der Geometrie* (1899) §13–§17; Apostol Ch. 3; Bourbaki *Topologie Générale* Ch. IV; Tarski 1948

References

TODO_REF
Apostol — Calculus Vol. 1 · Ch. 3 §3.1–3.7, the field axioms, order axioms, and least-upper-bound axiom
TODO_REF
Hilbert 1899 — Grundlagen der Geometrie · §13–§17 (Vollständigkeitsaxiom), originator of the complete-ordered-field axiomatisation
TODO_REF
Rudin — Principles of Mathematical Analysis · Ch. 1, the real and complex number systems
TODO_REF
Bourbaki — Topologie Générale · Ch. IV, nombres réels
TODO_REF
Tarski 1948 — A Decision Method for Elementary Algebra and Geometry · RAND R-109, decidability of the elementary theory of $\mathbb{R}$
TODO_REF
Bishop — Foundations of Constructive Analysis (1967) · Ch. 1–2, constructive completeness without LEM
TODO_REF
Robinson — Non-standard Analysis (1966) · Ch. 3, non-Archimedean extensions of $\mathbb{R}$

Lean module

Codex.Analysis.RealNumbers.Axioms

Mathlib gap

Mathlib carries the complete-ordered-field structure on $\mathbb{R}$ via
`LinearOrderedField` together with the `ConditionallyCompleteLinearOrderedField`
instance and the `Archimedean` typeclass, so each axiom appears as a
separate piece of the inferred structure on the type `ℝ`. What is not
unified in Mathlib is (a) the categoricity theorem stating that any two
conditionally complete linearly ordered fields are uniquely
order-isomorphic, packaged as a single named result, and (b) the
side-by-side comparison between the classical complete ordered field
and the constructive (LEM-free) Bishop-Bridges development. The
Codex statement gathers the Mathlib instances under one namespace and
records the categoricity gap.

Reviewer

TBD

Estimated time

beginner: 18m
intermediate: 40m
master: 65m