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−n with k,n:ℤ.
Proof First apply the Archimedean axiom to q≡ u−d> 0 and p≡ 2, giving m,n:ℤ with
|(m−1)(u−d) < 2 < (m+1)(u−d) < 2n(u−d).|
Then use it again with q′≡ 2−n, giving k:ℕ with
|d< u−2· 2−n< k· 2−n< u<(k+2)· 2−n. ▫|
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 <ℝ,
|x<R y ⇔ ∃ q:ℚ.x<R q<R y ≡ ∃ q:ℚ.δx q∧υx q ≡ ℓ x<ℝℓ y,|
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,
|φ x =⇒ ∀ h:[−1,+1].∃δ> 0.(|h|>δ∨φ(x+h)),|
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,
|∃ x:R.φ x ⇒ ∃ d u x:R.(d< x< u)∧∀ y:[d,u].φ y ⇒ ∃ q:Q.φ(j q) ⇒ ∃ x:R.φ x. ▫|
Proposition 14.7 Σℓ:Σℝ≅ΣR.
Proof As in Proposition 2.15, we define, for φ:ΣR,
|Iφ ≡ λδυ:Σℚ.∃ d< u:ℚ. δ d∧υ u∧∀ y:[d,u].φ y:ΣΣℚ×Σℚ,|
using the Heine–Borel property that we have assumed for [d,u]⊂ R. Then
|Iφ(ℓ x) ≡ Iφ(δx,υx) ≡ ∃ d u.(d<R x<R u)∧∀ y:[d,u].φ y ⇔ φ x,|
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 ℝ.
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 ℝ.
|a = cut (λ d.d< a, λ u.a< u).|
|[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
|(δ,υ) ≡ (λ d.P(λ x.d< x), λ u.P(λ x.x< u))|
is a Dedekind cut, with cut (δ,υ)=focusP, so
|(d<focusP) ⇔ P(λ x.d< x) and (focusP< u) ⇔ P(λ x.x< u).|
Proof The last part is equivalent to the definition of δ and υ. These are rounded and bounded because
|P(λ x.d< x) ⇔ P(λ x.∃ e.d< e< x) ⇔ ∃ e.d< e∧ P(λ x.e< x)|
|⊤ ⇔ P⊤ ⇔ P(λ x.∃ e.e< x) ⇔ ∃ e.P(λ x.e< x),|
using inter- and extrapolation and Scott continuity. By Lemma 4.9, with σ≡(d< u),
|P(λ x.d< u) ⇔ P⊥ ∨ (d< u) ∧ P⊤ ⇔ (d< u),|
since P preserves ⊤ and ⊥. Then (δ,υ) are disjoint because P preserves ∧ ,
|P(λ x.d< x)∧ P(λ x.x< u) ⇔ P(λ x.d< x< u) ⇒ P(λ x.d< u) ⇔ (d< u),|
and, by the dual argument, located because P preserves ∨:
|P(λ x.d< x)∨ P(λ x.x< u) ⇔ P(λ x.d< x∨ x< u) ⇐ P(λ x.d< u) ⇔ (d< u). ▫|
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:
|⊥ ⇔ ∀ x:[0,1].ω x and x≠ y =⇒ ω x∨ω y.|
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
|ω ≡ δ∨υ and Pφ ≡ ∃ d< u.δ d∧υ u∧∀ x:[d,u].φ x.|
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 ∨. ▫