The title of Richard Dedekind’s paper [Ded72] leads with the word “Stetigkeit”, officially translated as “continuity”. Irrational numbers get second billing — his construction gives us access to them only via continuity, and he stresses the importance of geometrical intuition. In other words, the real line is not a naked set of Dedekind cuts, dressed by later mathematicians in an outfit of so-called “open” subsets, but has a topology right from its conception. Dedekind cited square roots as an example of the way in which we use continuity to enrich the rational numbers, but even the rationals — being defined by division — presuppose an inequality relation that we shall come to regard as topology.
Although a great deal of mathematics has since been built over Dedekind’s construction, we still have no definition of the real numbers that is widely accepted across different foundational settings. This is in contrast to the Dedekind–Peano–Lawvere definition of the natural numbers, which has been applied within logical systems that are much weaker than the classical one, or differ substantially from it in other ways. This is a very unfortunate state of affairs at a time when a debate has at last begun amongst a number of separate disciplines that all call themselves “constructive”, ours being one of them. We need a definition so that we can agree on what we’re talking about.
So, at the risk of seeming presumptuous in the face of such a venerable object, let us first write down our own opinion of what it is that we are trying to construct. In this paper we shall use R for the object under construction, and ℝ for the real line in classical or other forms of analysis.
Definition 1.1
An object R is a Dedekind real line if
| y> 0 ⇒ ∃ n:ℤ. y(n−1) < x< y(n+1). |
Our axioms are all true of the classical real line. Indeed, with the exception of the new concept of overtness, they are all headline properties in traditional analysis — just as induction had been formulated two centuries before Dedekind and Peano encapsulated it in their axioms, and used two millennia before that. These are not just peculiar order-theoretic facts that happen to lend themselves to some interesting construction.
However, some of our constructive colleagues have not adopted certain of these axioms. In particular, many formalist accounts and machine implementations use Cauchy sequences instead of Dedekind cuts. You already know our opinion on this question from the title of this paper: familiar examples such as Riemann integration give Dedekind cuts naturally, but sequences artificially. Any Cauchy sequence with a specified modulus of convergence has a limit that is defined by a Dedekind cut, but it is more difficult to translate in the other direction. We suspect that the preference for Cauchy sequences is merely a symptom of the traditional prejudice against logic. This paper shows that Dedekind cuts can be defined without using set theory, and we hope to demonstrate in future work that they also provide a natural way in which to compute with real numbers [Bau08][K].
The Heine–Borel theorem (compactness of the closed interval) is one of the most important properties that real analysts use. However, as we shall see in Section 15, this is not just a result that we prove in passing, but a hotly debated issue in the foundations of constructive analysis. For example, Errett Bishop [Bis67] reformulated a large part of the subject without it, deftly avoiding the many pathologies that arise from so doing.
In particular, he defined a function to be “continuous” if it is uniformly so when restricted to any compact domain, “compact” itself being defined as closed and totally bounded. Hence any continuous f:K→ℝ+ is bounded (away from ∞, if you wish), but there is no similar result to bound it away from 0. Indeed, if K is Cantor space, such a result would entail (Brouwer’s fan theorem and so) the Heine–Borel theorem. It follows that, if there is a category of partial functions on ℝ that agrees with the uniformly continuous ones on compact domains and includes λ x.1/x, then the Heine–Borel theorem holds [Pal05, Sch05, Waa05, JR84, BB08a, BB08b]
The reason why Bishop’s followers and others omit this property is that they are interested in computation, at least in principle. However, if one tries to develop analysis based on points, that is, in the way in which it has been done since Cantor, but using only those real numbers that are representable by programs, then the results are exceedingly unpleasant. In particular, the Heine–Borel theorem fails.
In fact, Dedekind completeness and the Heine–Borel property are both consequences of the view that open sets and not points are primary. That they hold at all in the traditional setting is the result of the heavy-handed methods of classical mathematics, which are far stronger than what is justified by computation. Brouwer’s fan theorem is, arguably, a way of legitimising part of the classical approach in a constructive setting.
The best developed formulation of topology entirely in terms of open sets (“pointless topology”, according to a now rather tired joke) is provided by locale theory. Although it does not consider computation, it does provide a way of developing general topology in foundational settings (at least, in toposes) other than the classical one. The most famous example of this is that it proves the Tychonov theorem (that the product of any family of compact objects is compact) without using the axiom of choice [Joh82, Theorem III 1.7]. Less well known, but more importantly for us, the localic interval [0,1] is always Dedekind-complete and compact. On the other hand, when we interpret the traditional (point-based) definitions in the internal language of a sheaf topos, the object of Cauchy reals is typically smaller than the Dedekind one, and the Heine–Borel theorem fails [FH79].
Formal Topology also works with open subspaces, but is based on Martin-Löf type theory; there too [0,1] is compact [CN96].
Abstract Stone Duality exploits the algebra of open sets as well, and so the “real line” R that we construct in this paper is Dedekind-complete and satisfies the Heine–Borel property. But ASD generalises Dedekind’s topological conception of the real line: in it, the topology is an inherent and unalienable part of a space, which is not a set of points to which open subsets have been added as an afterthought.
In locale theory, the algebra and lattice theory are all too obvious, whilst they are represented in formal topology by generators and relations. Both of these theories expect a high degree of mathematical sophistication and perseverance from the student, and only in an exceptionally well written account do the public theorems about topology stand out from the private algebraic calculations. In [Joh82] the former are marked with an asterisk, although the official meaning of that symbol is a dependence on the axiom of choice.
The lattice of open subspaces in locale theory is a set (or an object of a topos), but in ASD it is another space, with its own topology. This is formulated in the style of a type theory that makes ASD look like topology with points. The λ-notation speaks out loud and clear about continuous maps in a way that frame homomorphisms in locale theory do not. When we do some basic analysis in [J], we shall see that the language of terms, functions and open predicates actually works more smoothly than does the traditional one using set theory.
In both traditional topology and locale theory there is an asymmetry between infinite unions and finite intersections that makes it difficult to see the duality between open and closed phenomena. Intuitionistic foundations also obscure this symmetry by stating many results that naturally pertain to closed sets in a form that uses double negations. When we treat the lattice of opens of one space as another space, by contrast, the purely infinitary (directed) joins slip into the background, and the open–closed duality stands out very clearly. Indeed, it is a fruitful technique to “turn the symbols upside down” (⊤/⊥, ∧/∨, =/≠, ∀/∃), often giving a new theorem.
In this context, we shall see what the foundational roles of Dedekind completeness and the Heine–Borel theorem actually are. The former is the way in which the logical manipulation of topology has an impact on numerical computation. Again there is an analogy with the axioms for the natural numbers: for them the same role is played by definition by description, which Giuseppe Peano was also the first to formulate correctly [Pea97, §22], albeit in a different paper from the one on induction. In the ASD λ-calculus, these ideas are captured as rules that introduce numbers on the basis of logical premises.
The Heine–Borel property, meanwhile, is the result of ensuring that all algebras are included in the category. Our λ-calculus formulates this idea in an apparently point-based way by introducing higher-order terms which ensure that subspaces carry the subspace topology. We shall show that these terms are inter-definable with the “universal quantifiers” ∀ that define compactness.
The new concept of overtness is related to open subspaces in the way that compactness is to closed ones, and to logic in the shape of the existential quantifier, ∃. However, in contrast to compactness of the closed interval, no discipline would contest that the real line is overt. Indeed, the reason why you haven’t heard of overt (sub)spaces before is that classical topology makes all spaces overt — by force majeure, without providing the computational evidence.
This idea has, in fact, been identified in locale theory, but only the experts in that subject have been able to exploit it [JT84, Joh84]. In the case of overtness, formal topology shows up the idea better than locale theory does. Its role in constructive analysis is played by locatedness, though that is a metrical property, so the correspondence is not exact [Spi10]. We shall show in ASD’s account of analysis [J] that overtness explains the situations in which equations f x=0 for f:ℝ→ℝ can or cannot be solved.
However, it is really in computation that the importance of this concept becomes clear. For example, it provides a generic way of solving equations, when this is possible.
Since ASD is formulated in a type-theoretical fashion, with absolutely no recourse to set theory, it is intrinsically a computable theory.
The familiar arithmetical operations +, − are × are, of course, computable algebraic structure on R, as are division and the (strict) relations <, > and ≠ when we introduce suitable types for their arguments and results. The topological properties of overtness and compactness are related to the logical quantifiers ∃ and ∀, which we shall come to see as additional computable structure.
Any term of the ASD calculus is in principle a program, although the details of how this might be executed have yet to be worked out [Bau08][K]. In particular, our proofs of compactness and overtness of closed intervals provide programs for computing quantifiers of the form ∀ x:[d,u] and ∃ x:[d,u] respectively. These are general and powerful higher-order functions from which many useful computations in real analysis can be derived.
This paper is rather long because we have to introduce the ASD calculus before we can use it for the construction. Although real arithmetic is familiar and not really related to the main issue of the Heine–Borel theorem, you would think it odd if we left it out, and of course we shall need it in order to prove completeness of the axioms, but it is a sizable task in itself. If you are impatient to see our construction of R, you may find it helpful to start with Section 6, and then bring in the introductory material as you need it.
We shall use a lot of ideas from interval analysis. However, instead of defining an interval [d,u] as the set {x∈ℝ ∣ d≤ x≤ u} or as a pair <d,u> of real numbers, as is usually done, we see it as a weaker form of Dedekind cut, defined in terms of the rationals. Real numbers (genuine cuts) are special intervals. Section 2 explains the classical idea behind our construction of the Dedekind reals, presenting it from the point of view of interval analysis.
As this is the first paper in which Abstract Stone Duality has reached maturity, we give a survey of it in Sections 3–5 that will also be useful for reference in connection with other applications besides analysis. This provides a guide to the earlier papers, by no means making them redundant; for other independent introductions, see [J][O].
Sections 6–9 perform the main construction, developing cuts, the interval domain and the real line in ASD, and prove Dedekind completeness. Section 10 proves that the closed interval is compact and overt.
Sections 11–13 consider arithmetic in an entirely order-theoretic style, i.e. with Dedekind cuts rather than Cauchy sequences. We formulate an important “roundedness” property of the interval operations that is crucial to their correctness, extend the arithmetic operations to Kaucher’s back-to-front intervals, and identify the precise role of the Archimedean principle.
After we have shown how to construct an object that satisfies Definition 1.1, Section 14 shows that it is unique (up to unique isomorphism), i.e. that the axioms above are complete. This means, on the one hand, that they are sufficient to develop analysis [J], and on the other that we may focus on them in order to do computation. We also show that Dedekind completeness is equivalent to abstract sobriety via some simple λ-conversions.
Finally, Section 15 compares ours with other schools of thought. In particular, we contrast compactness of the closed interval here with its pathological properties in Recursive Analysis, and comment on the status of ASD from the point of view of a constructivist in the tradition of Errett Bishop.