14  Axiomatic completeness

Our construction of the real line in ASD is finished. At any rate, we have found an object that has all of the properties that we listed in Definition 1.1, so we shall now write ℝ for it.

Are these axioms sufficient to characterise the reals? We shall show that any object R that satisfies Definition 1.1 is uniquely isomorphic to the one that we have constructed.

However, we shall state the assumption that R be Dedekind-complete explicitly when we need it, and leave it out otherwise. This is because we also intend to explore the analogy between Dedekind completeness and definition by description, which are both special cases of sobriety (Definition 4.22). All three of these ideas say how the manipulation of logical expressions has an impact back on numbers.

We claim that ASD (in particular, sobriety) generalises Dedekind’s intuition — to the extent of making Dedekind completeness redundant. This means that, if you try to encapsulate the Cauchy reals in some construction within ASD, the result will actually be Dedekind complete . We find the limit of any Cauchy sequence as a Dedekind cut in Theorem J 6.14.

We begin with the well known argument for the uniqueness of ℝ based on its algebra, order, Dedekind completeness and the Archimedean principle.

Proposition 14.1 Let R be an ordered field. Then there are unique monos ℕ→ R, ℤ→ R and j:ℚ→ R that preserve 0, 1, +, ×, < and (where appropriate) − and ÷. In particular, R has characteristic 0.         ▫

Lemma 14.2 If d< u in an Archimedean ordered field R then there is some q:ℚ with d< q< u, and we may choose it to be dyadic, i.e. of the form q≡ k· 2⁻ⁿ with k,n:ℤ.

Proof    First apply the Archimedean axiom to q≡ u−d> 0 and p≡ 2, giving m,n:ℤ with

Then use it again with q′≡ 2⁻ⁿ, giving k:ℕ with

Proposition 14.3 Let R be an Archimedean ordered field. Then there is a mono ℓ:R↣ℝ that fixes ℚ, and preserves and reflects <.

Proof    For x:R, consider δ_x,υ_x:Σ^ℚ, defined by δ_x d≡(d<_R x) and υ_x u≡(x<_R u). Since ℚ→ R preserves and reflects order, for x:ℚ, these formulae agree with Lemma 6.12.

They are clearly lower, upper and disjoint, using the basic properties of the order on R. As this order is located in the sense that (d<_R u)⇒(d<_R x)∨(x<_R u), the pair (δ_x,υ_x) is located in the sense of Definition 6.8. Boundedness follows directly from the Archimedean principle, and roundedness by Lemma 14.2.

Hence (δ_x,υ_x) is a Dedekind cut of ℚ, and we have defined a map ℓ:R→ℝ. Using Lemma 14.2 for R again, together with Definition 6.10 for <_ℝ,

so the order relations <_R and <_ℝ agree, and (as they are total) the map ℓ is mono.         ▫

Theorem 14.4 If R is a Dedekind-complete Archimedean ordered field then the map ℓ in the previous result is an isomorphism. Definition 1.1 therefore characterises ℝ uniquely up to unique isomorphism.

Proof    Members of ℝ are by definition Dedekind cuts of ℚ, which extend to cuts of R as in Proposition 9.5. These define members of R since it is Dedekind-complete. Since all of the orders agree, this process is inverse to the construction of ℓ.         ▫

Throughout this paper we have emphasised that we regard topology as primary, but it was not mentioned in the previous result. So we shall now investigate Σ^R, deducing that ℓ:R≅ℝ from the principles of ASD, without assuming Dedekind completeness. The arguments are essentially those that led up to the formulation of E in Section 2.

Proposition 14.5 For x:R and φ:Σ^R,  φ x  ⇔ ∃ d u.(d< x< u)∧ ∀ y:[d,u].φ y.

Proof    Whilst Corollary 10.8 has already shown that the Dedekind reals ℝ (as we have constructed them) satisfy this property, we claim here that it also follows from Definition 1.1. This is proved in detail in Theorem J 10.2. The key point is that, since [−1,+1]⊂ R is compact, Hausdorff and totally ordered,

and then Scott continuity (Axiom 4.21) allows us to interchange the quantifiers. This uses neither Dedekind completeness nor the Archimedean principle.         ▫

Lemma 14.6 The quantifier ∃_R is given by ∃_ℚ, as in Theorem 9.2.

Proof    By Proposition 14.5 and Lemma 14.2,

Proposition 14.7   Σ^ℓ:Σ^ℝ≅Σ^R.

Proof    As in Proposition 2.15, we define, for φ:Σ^R,

using the Heine–Borel property that we have assumed for [d,u]⊂ R. Then

in which d and u may be chosen from either ℚ or R, by Lemma 14.6, and we recognise the formula in Proposition 14.5. So Σ^ℓ· I is the identity on Σ^R.

Now, the proof of Proposition 2.17 (or its modification for Notation 8.2) is also valid for R in ASD. Hence Σ^R and Σ^ℝ split the same idempotent E on Σ^Σℚ×Σℚ, cf. Remark 5.2, so they are isomorphic.         ▫

The topology on ℝ is therefore unique, when we assume the Heine–Borel property but not necessarily Dedekind completeness. As in the title of Dedekind’s paper, the topology comes first, and we derive irrational numbers from that.

Theorem 14.8 Consider Definition 1.1, including the Heine–Borel property but omitting Dedekind completeness. If R satisfies this and is also sober, or indeed definable, then it is uniquely isomorphic to ℝ.

Proof    Propositions 4.23, 4.25, 5.18 and 14.7.         ▫

Remark 14.9 On the other hand, we could bypass the constructions of this paper by defining ℝ as a base type, together with (all of) the structure of Definition 1.1.

In Axiom 4.24 we showed how descriptions for ℕ may be formulated in a type-theoretic style by giving the introduction rule for “the”. In this, the elimination, β- and η-rules are given by singleton and substitution, and there is a normalisation theorem Section A 8. It is easy to overlook the key role of equality (=) in this — it is to descriptions as application is to λ-abstraction and membership is to set-formation. Since ℝ is Hausdorff and not discrete, we cannot base an analogous treatment of it on equality. We could use inequality (≠) (Exercise 14.14), but it is more natural to consider < and >, as these give rise to the lower and upper parts of a Dedekind cut.

Definition 14.10 Dedekind cuts and the arithmetical order may be seen as introduction and elimination rules for the type ℝ.

1. ℝ-introduction: given a cut (δ,υ):Σ^ℚ×Σ^ℚ, we introduce a real number cut (δ,υ):ℝ;
2. ℝ-elimination: given a real number a:ℝ and rationals d,u:ℚ, we eliminate a in favour of (d< a),(a< u):Σ, along with the other rules concerning the order <;
3. ℝ-beta: δ d ⇔ (d<cut (δ,υ)) and υ u ⇔ (cut (δ,υ)< u) ;
4. ℝ-eta: a=cut (λ d.d< a,λ u.a< u).

Whenever we add new features like this, we have to ask what effect they have on the terms and equations of the existing calculus.

Theorem 14.11 ℝ is a conservative extension of the ASD calculus.

Proof    As we have already constructed an object that satisfies Definitions 1.1 and 14.10 within the calculus, the earlier results of this section show that the new object is uniquely isomorphic to the old one. Similarly, any new type expressions are isomorphic to old ones. These isomorphisms translate the new terms of the old types into provably equal old terms, and the new equations are also redundant. This means that the new category is equivalent to the old one.         ▫

Remark 14.12 As this argument is not very illuminating, here is an explicit procedure for eliminating (Dedekind) cut  operations, except on the outside of a term of type ℝ.

1. If we are given a term a of type ℝ, we use the ℝ-η-law to wrap it in a cut :

   a  =   cut  (λ d.d< a,  λ u.a< u).

2. Any cut  that occurs as a proper sub-term of this is itself of type ℝ, but is enclosed in a smallest sub-term σ of type Σ. By Proposition 14.5, this is of the form

   [cut (δ,υ)/x]*σ  ⇔ (λ x.σ)cut (δ,υ)  ⇔ ∃ d< u:ℚ.δ d∧υ u∧∀ x:[d,u].σ.

This normalisation theorem means that we compute with logical expressions (involving predicates on rationals) instead of real numbers. Notice that Dedekind completeness and the Heine–Borel theorem are intimately related. In fact, instead of the quantifier ∀ x:[d,u], we may simply evaluate σ according to Moore’s rules at the interval x≡[d,u]. This is part of a translation that has the effect of replacing continuous variables by intervals, which is what programmers do anyway, but it is justified formally in [K].         ▫

As ℝ is no longer one of the types that are generated from ℕ using powers and Σ-split subspaces, we need to show that it is sober, cf. Proposition 2 for ℕ.

Lemma 14.13 If P:Σ^ΣR is prime then

is a Dedekind cut, with cut (δ,υ)=focusP, so

Proof    The last part is equivalent to the definition of δ and υ. These are rounded and bounded because

and

using inter- and extrapolation and Scott continuity. By Lemma 4.9, with σ≡(d< u),

since P preserves ⊤ and ⊥. Then (δ,υ) are disjoint because P preserves ∧ ,

and, by the dual argument, located because P preserves ∨:

Exercise 14.14 Using ≠ instead, we can develop definition by co-description for real numbers, replacing the singleton with its complement. But since ∃ also becomes ∀, we have to consider this in a compact Hausdorff space such as I, instead of ℝ. The existence and uniqueness conditions for ω to classify a co-singleton are then the duals of those in Axiom 4.24:

Consider any function f:[0,1]→ℝ. Use the Heine–Borel Theorem to show that ω x≡∃ z.f z< f x satisfies the first condition, and hence that δ d≡∀ x.(d< x)∨ω x and υ u≡∀ x.(x< u)∨ω x define an interval, i.e. they are rounded, bounded and disjoint. Classically, this interval is the convex hull of the set on which f attains its minimum value.

Now suppose that (x≠ y)=⇒∃ z.(f z< f x)∨(f z< f y), cf. [Sch03]. This is the uniqueness condition for ω. Use Lemma 4.13 for compact Hausdorff spaces to deduce that (δ,υ) is located, giving a Dedekind cut w∈[0,1]. Show that w is the minimum of f, i.e. it satisfies (x≠ w)⇒(f w< f x).

Show that definition by co-description is equivalent to sobriety and Dedekind completeness, using the translations

Expressing any co-description ω as a Dedekind cut is a special case of the characterisation of connected subspaces of ℝ in Lemma J 13.16.

From roundedness, boundedness and disjointness, we easily deduce that P preserves ⊥, ⊤ and ∧; these also entail the existence condition for the co-description ω, but this is more difficult. On the other hand, locatedness easily gives the uniqueness condition for ω, whilst it is more difficult to show that P preserves ∨.         ▫