Chapter 211Core route

Completions and the Real Numbers

The real numbers

Constructively, a sequence of equivalence classes need not have a sequence of representatives. Thus the ordinary quotient of Cauchy sequences may require countable choice, while Dedekind cuts do not. We construct the two real types and identify the hypothesis under which they agree; the Cauchy construction generates limits and equality simultaneously rather than first quotienting representatives.

Convention 74.60 — The ambient propositions ¶

Fix a set $SProp$ of mere propositions containing $0$ and $1$ and closed under $\land$ , $\lor$ , and existential quantification over $N$ (hence over countable sets). Cuts below are $SProp$ -valued predicates. One may obtain such a $SProp$ by tracking universes, by propositional resizing, or, classically, from $2$ under LEM.

Referenced from 2 locations

Completions and the Real Numbers

Remark 74.61 — The rationals ¶

$Z$ is constructed from $N$ and $Q$ from $Z$ by the set quotients of definition 68.38 (pairs modulo cross-multiplication), or quotient-free via canonical representatives. Equality on $Q$ is decidable, so $Q$ is a set already by Hedberg’s theorem (theorem 66.29); it is a discrete, archimedean ordered field with decidable order. We write $Q^{+} : = \sum_{q : Q} (q > 0)$ .

Referenced from 2 locations

Completions and the Real Numbers

Definition 74.62 — Dedekind reals ¶

A Dedekind cut is a pair $(L, U)$ of predicates $L, U : Q \to SProp$ satisfying four conditions:

it is inhabited: $\exists q . L (q)$ and $\exists r . U (r)$ ;
it has roundedness: membership persists through a strictly closer rational bound, expressed by $L (q) \leftrightarrow \exists r . (q < r) \land L (r)$ , and $U (r) \leftrightarrow \exists q . (q < r) \land U (q)$ ;
it is disjoint: $\neg (L (q) \land U (q))$ for all $q$ ;
it is located: $(q < r) \to L (q) \lor U (r)$ for all $q, r$ ,

where quantifiers range over $Q$ and $\exists$ , $\lor$ denote the truncated connectives of chapter 66. Writing $isCut (L, U)$ for the conjunction, the type of Dedekind reals is $R_{d} : = \sum_{(L, U) : (Q \to SProp) \times (Q \to SProp)} isCut (L, U) .$ Each $q : Q$ determines the cut $L_{q} (r) : = (r < q)$ , $U_{q} (r) : = (q < r)$ , giving an embedding $Q \to R_{d}$ .

Referenced from 3 locations

Completions and the Real Numbers

Lemma 74.63 ¶

$R_{d}$ is a set.

Referenced from 2 locations

Completions and the Real Numbers

Proof of Lemma 74.63

Proof. $isCut$ is a mere proposition and $Q \to SProp$ is a set (a product of sets, by theorem 65.18); a subtype of a set is a set. ◻

Definition 74.64 ¶

For $x = (L_{x}, U_{x})$ and $y : R_{d}$ define $\begin{aligned} (x < y) & : = \exists q : Q . U_{x} (q) \land L_{y} (q), \\ (x \leq y) & : = \forall q : Q . L_{x} (q) \to L_{y} (q), \\ L_{x + y} (q) & : = \exists r, s . L_{x} (r) \land L_{y} (s) \land (q = r + s), \\ U_{x + y} (q) & : = \exists r, s . U_{x} (r) \land U_{y} (s) \land (q = r + s), \end{aligned}$ Negation and the lattice operations are defined by $\begin{aligned} L_{- x} (q) & : = U_{x} (- q), & U_{- x} (q) & : = L_{x} (- q), \\ L_{x \lor y} (q) & : = L_{x} (q) \lor L_{y} (q), & U_{x \lor y} (q) & : = U_{x} (q) \land U_{y} (q), \\ L_{x \land y} (q) & : = L_{x} (q) \land L_{y} (q), & U_{x \land y} (q) & : = U_{x} (q) \lor U_{y} (q) . \end{aligned}$ Put $| x | : = x \lor (- x)$ . For example, roundedness of $L_{- x}$ follows from upper roundedness of $U_{x}$ : from $U_{x} (- q)$ choose $t < - q$ with $U_{x} (t)$ , set $r : = - t > q$ , and obtain $L_{- x} (r)$ .

Referenced from 3 locations

Completions and the Real Numbers

Theorem 211.6 — Dedekind-real additive structure ¶

The operations of definition 74.64 have the following properties.

Addition and negation make $R_{d}$ a lattice-ordered abelian group, and the rational-cut map is an order-reflecting group embedding. The order is archimedean in the exact sense that, if $0 < x$ , then for every $y$ there merely is $n : N$ with $y < n \cdot x$ .
If $x < y$ , then there merely is a rational $q$ with $x < q < y$ .

Referenced from 2 locations

Completions and the Real Numbers

Proof of Theorem 211.6 — Dedekind-real additive structure

Proof. The cut axioms for $x + y$ follow directly from rational witnesses. For example, if $L_{x + y} (q)$ has witnesses $r, s$ , lower roundedness of $x$ gives $r^{'} > r$ in $L_{x}$ ; then $q^{'} = r^{'} + s > q$ witnesses roundedness of the sum. If both $L_{x + y} (q)$ and $U_{x + y} (q)$ held, their witnesses would give $r < r^{'}$ and $s < s^{'}$ but $r + s = r^{'} + s^{'} = q$ , a contradiction. Given $q < q^{'}$ , choose rational $a < b$ and $c < d$ around $x$ and $y$ with $(b - a) + (d - c) < q^{'} - q$ . Either $q < a + c$ , which gives $L_{x + y} (q)$ by lower closure, or $a + c \leq q$ . In the second case the width inequality gives $b + d < q^{'}$ , hence $U_{x + y} (q^{'})$ by upper closure.

We first prove cut extensionality. Equality of lower predicates implies equality of cuts: upper roundedness and disjointness give $U_{x} (q) \to \exists r < q . \neg L_{x} (r),$ while locatedness at $r < q$ proves the converse. Propositional and function extensionality therefore recover the upper predicate from the lower one. Cut extensionality now reduces associativity, commutativity, and the zero laws to reassociation and commutation of rational witnesses. For the inverse law, the implication $L_{x + (- x)} (q) \to q < 0$ follows from $r < x < - s$ and $q = r + s$ . Conversely, for $q < 0$ choose a rational bracket $r < x < t$ with $t - r < - q$ ; then $r < x < r - q$ and $q = r + (q - r)$ , so $r$ and $q - r$ witness $L_{x + (- x)} (q)$ . The upper cuts are dual, hence $x + (- x) = 0$ .

The four displayed predicates for $x \lor y$ and $x \land y$ satisfy the cut axioms. For example, locatedness of $x \lor y$ follows by applying locatedness first to $x$ and then to $y$ : either a lower predicate holds, or both upper predicates hold. Roundedness of the conjunctions uses a common rational refinement, and disjointness follows from disjointness of the selected component. Pointwise inclusion of lower predicates proves $x \leq x \lor y, y \leq x \lor y, (x \leq z \land y \leq z) \to x \lor y \leq z,$ and the dual three laws for $x \land y$ . Thus the displayed cuts are the join and meet. Translation by $z$ preserves $\leq$ , and translation by $- z$ reflects it; hence translation is an order isomorphism and preserves joins and meets. This proves the lattice-ordered group laws. The formulas for rational cuts preserve and reflect order, addition, and negation.

For the second clause, a witness to $x < y$ is precisely a rational $q$ satisfying $U_{x} (q) \land L_{y} (q)$ , which says $x < q < y$ .

To prove the Archimedean clause, let $0 < x$ . The rational-density result gives $q : Q$ with $0 < q < x$ . Choose a rational upper bound $r$ for $y$ from inhabitedness of $U_{y}$ , and then choose $n : N$ with $0 < n$ and $r < n q$ by the Archimedean property of $Q$ . Order preservation under finite sums gives $y < r < n q < n \cdot x .$ These arguments are the constructive additive part of [Uni13]; no multiplicative inverse or field structure for $R_{d}$ is asserted here. ◻

Definition 74.66 — Cauchy approximation ¶

For an archimedean lattice-ordered abelian group $F$ , a Cauchy approximation is a map $x : Q^{+} \to F$ with $| x_{δ} - x_{ϵ} | < δ + ϵ$ for all $δ, ϵ$ ; a limit of $x$ is $ℓ : F$ with $| x_{ϵ} - ℓ | < ϵ + θ$ for all $ϵ, θ$ . $F$ is Cauchy complete if every Cauchy approximation has a limit. We take a sequence modulus to be antitone in the requested precision. Any modulus can be put in this form by passing to dyadic precisions and taking finite running maxima; a Cauchy sequence with such an explicit modulus determines a Cauchy approximation, and conversely approximations retain their moduli.

Referenced from 2 locations

Completions and the Real Numbers

Theorem 74.67 ¶

The Dedekind reals are Cauchy complete. A Cauchy approximation $x$ has the limit cut $\begin{aligned} L_{y} (q) & : = \exists ϵ, θ : Q^{+} . L_{x_{ϵ}} (q + ϵ + θ), \\ U_{y} (q) & : = \exists ϵ, θ : Q^{+} . U_{x_{ϵ}} (q - ϵ - θ) . \end{aligned}$

Referenced from 5 locations

Proof of Theorem 74.67

Proof. For the first clause, choose a rational interval around one $x_{ϵ}$ to see that $L_{y}$ and $U_{y}$ are inhabited; moving an endpoint by a smaller positive rational proves roundedness. If both $L_{y} (q)$ and $U_{y} (q)$ held, their witnesses would put $x_{δ}$ strictly more than $δ + ϵ$ below $x_{ϵ}$ , contradicting the Cauchy inequality. For locatedness, given $q < r$ , choose $ϵ > 0$ with $4 ϵ < r - q$ . Locatedness of $x_{ϵ}$ at $q + 2 ϵ < r - 2 ϵ$ gives $L_{x_{ϵ}} (q + 2 ϵ) or U_{x_{ϵ}} (r - 2 ϵ),$ hence $L_{y} (q)$ or $U_{y} (r)$ . Finally, by rational density, for each $ϵ, θ > 0$ there are endpoints $x_{ϵ} - ϵ - θ < q < x_{ϵ} - ϵ - θ / 2 < x_{ϵ} < x_{ϵ} + ϵ + θ / 2 < r < x_{ϵ} + ϵ + θ .$ The definitions of $L_{y}$ and $U_{y}$ give $q < y < r$ , and therefore $| x_{ϵ} - y | < ϵ + θ$ . This proves exactly Cauchy completeness; no finality or Dedekind-completion idempotence theorem is used below. ◻

Exercise 74.17 ¶

★★★ Verify that $(L_{q}, U_{q})$ of definition 74.62 is a cut, and that $q \mapsto (L_{q}, U_{q})$ is injective, order-preserving, and order-reflecting.

Referenced from 3 locations

Exercise 74.18 ¶

★★★ Define $- x$ for $x : R_{d}$ , verify the cut conditions, and prove $x + (- x) = 0$ . Where is locatedness of $x$ used?

Referenced from 3 locations

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 211.3, then complete exercise 211.4.

Exercise 211.3 ¶

★★★ For the cut $(L_{y}, U_{y})$ in theorem 74.67, prove inhabitedness and roundedness of both halves. Then give the complete contradiction that rules out $L_{y} (q) \land U_{y} (q)$ , naming the two approximation indices and the strict rational inequality that contradicts the Cauchy bound.

Referenced from 4 locations

Exercise 211.4 ¶

★★★ Practical project.dedekind-bracket-refiner Implement in Agda or Kappa dyadic bisection for $\sqrt{2}$ , representing a bracket by natural numbers $(l, u, d)$ with $l^{2} < 2 d^{2} < u^{2}$ . One step compares $(l + u)^{2}$ with $2 (2 d)^{2}$ and returns a bracket of half the width. Starting from $(1, 2, 1)$ , print three refinements and check the invariant after each one. Mutation test: omit the factor $2$ on the right side of the midpoint comparison; an invariant check must fail. The executable establishes only these finite arithmetic checks, not the existence of a Dedekind real or the chapter’s completeness theorem.

Referenced from 5 locations

Bibliographic notes

The Dedekind definitions follow Chapter 11 of the HoTT Book [Uni13]. The exact free-completion, extension, field, and Cauchy-to-Dedekind embedding theorems used on the optional route are imported from Gilbert’s paper and accompanying formalization [Gil17]. The inductive–inductive Cauchy construction is motivated by the failure of the ordinary sequential quotient to have the desired choice-free universal property; the Dedekind side follows constructive analysis. General categorical semantics for the quotient and truncation constructions are treated in [Jac99]. The optional construction uses the QIIT/QWI elimination principle from chapter 68; no theorem in the core Dedekind development depends on that route.