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

- it is an overt space (Theorem 9.2);
- it is Hausdorff, with an inequality or apartness relation, ≠ (Theorem 9.3);
- the closed interval [0,1] is compact (Theorem 10.7);
*R*has a total order, that is, (*x*≠*y*)⇔ (*x*<*y*)∨(*y*<*x*) (Theorem 9.3);- it is Dedekind-complete, in a sense in which the two halves of a cut are open (Theorem 9.6);
- it is a field, where
*x*^{−1}is defined iff*x*≠ 0, in the sense of (d) (Theorem 13.4); - and Archimedean (Theorem 13.6), that is,
for
*x*,*y*:*R*,*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.