The Dedekind Reals in Abstract Stone Duality
Andrej Bauer and Paul Taylor
3 June 2009
Abstract
Abstract Stone Duality (ASD) is a direct axiomatisation of general topology, in contrast to the
traditional and all other contemporary approaches, which rely on a prior notion of discreteset, type or object of a topos.
ASD reconciles mathematical and computational viewpoints, providing an inherently computable calculus that does not sacrifice key properties of real analysis such as compactness ofthe closed interval. Previous theories of recursive analysis failed to do this because they werebased on points; ASD succeeds because, like locale theory and formal topology, it is foundedon the algebra of open subspaces.
ASD is presented as a lambda-calculus, of which we provide a self-contained summary,as the foundational background has been investigated in earlier work.
The core of the paper constructs the real line using two-sided Dedekind cuts. We show thatthe closed interval is compact and overt, where these concepts are defined using quantifiers.
Further topics, such as the Intermediate Value Theorem, are presented in a separate paperthat builds on this one.
The interval domain plays an important foundational role. However, we see intervals as
generalised Dedekind cuts, which underly the construction of the real line, not as sets or pairsof real numbers.
We make a thorough study of arithmetic, in which our operations are more complicatedthan Moore’s, because we work constructively, and we also consider back-to-front (Kaucher)intervals.
Finally, we compare ASD with other systems of constructive and computable topology
and analysis.
AMS classification: 03F60 06E15 18C20 26E40 54D45 65G40.
Keywords: Dedekind real numbers, abstract Stone duality, Heine–Borel theorem, compact
topological space, constructive analysis, interval analysis, domain theory, lambda calculus,
exact real arithmetic, Kaucher arithmetic.
Contents
1. Introduction
2. Cuts and intervals
3. Topology as λ-calculus
4. The ASD λ-calculus
5. The monadic principle
6. Dedekind cuts
7. The interval domain in ASD
8. The real line as a space in ASD

2
5
12
15
22
28
33
37

9.
10.
11.
12.
13.
14.
15.
16.

Dedekind completenessOpen, compact and overt intervals
Arithmetic
Multiplication
Reciprocals and roots
Axiomatic completeness
Recursive analysis
Conclusion

To appear in Mathematical Structures in Computer Science, 19 (2009).

1

42
45
49
54
58
60
64
67

1

Introduction

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, thereal line is not a naked set of Dedekind cuts, dressed by later mathematicians in an outfit of socalled “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 therationals — being defined by division — presuppose an inequality relation that we shall come toregard 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 foundationalsettings. 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, ordiffer 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’retalking 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 R for the real line in classical or other forms of analysis.
Definition 1.1 An object R is a Dedekind real line if(a) it is an overt space (Theorem 9.2);(b) it is Hausdorff, with an inequality or apartness relation, 6= (Theorem 9.3);(c) the closed interval [0, 1] is compact (Theorem 10.7);(d) R has a total order, that is, (x 6= y) ⇔ (x < y) ∨ (y < x) (Theorem 9.3);(e) it is Dedekind-complete, in a sense in which the two halves of a cut are open (Theorem 9.6);(f) it is a field, where x−1 is defined iff x 6= 0, in the sense of (d) (Theorem 13.4);(g) and Archimedean (Theorem 13.6), that is, for x, y : R,
y > 0 ⇒ ∃n:Z. y(n − 1) < x < y(n + 1).
Our axioms are all true of the classical real line. Indeed, with the exception of the new conceptof overtness, they are all headline properties in traditional analysis — just as induction had beenformulated 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 lendthemselves 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 showsthat 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 result2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 → R+ 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 R 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, BB08b, BB08a]
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 numbersthat 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 theview that open sets and not points are primary. That they hold at all in the traditional settingis the result of the heavy-handed methods of classical mathematics, which are far stronger thanwhat is justified by computation. Brouwer’s fan theorem is, arguably, a way of legitimising partof 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 (atleast, 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 forus, 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, theobject 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-Lö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 ofmathematical sophistication and perseverance from the student, and only in an exceptionallywell 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 ofthat 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 isanother 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 actuallyworks more smoothly than does the traditional one using set theory.
3

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” (>/⊥, ∧/∨, =/6=, ∀/∃), often giving a new theorem.
In this context, we shall see what the foundational roles of Dedekind completeness and theHeine–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 thatthese 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 toclosed ones, and to logic in the shape of the existential quantifier, ∃. However, in contrast tocompactness 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 [Spi07]. We shall show in
ASD’s account of analysis [J] that overtness explains the situations in which equations f x = 0 for
f : R → R 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 6= when we introduce suitable types fortheir 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 andovertness 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 issueof the Heine–Borel theorem, you would think it odd if we left it out, and of course we shall need itin 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.
4

We shall use a lot of ideas from interval analysis. However, instead of defining an interval [d, u]
as the set {x ∈ R | d ≤ x ≤ u} or as a pair hd, ui of real numbers, as is usually done, we see it asa 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 surveyof 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 thereal line in ASD, and prove Dedekind completeness. Section 10 proves that the closed interval iscompact 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 backto-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 showsthat 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, andcomment on the status of ASD from the point of view of a constructivist in the tradition of Errett
Bishop.

2

Cuts and intervals

We begin by recalling Richard Dedekind’s construction, and relating it to some ideas in interval
analysis. These provide the classical background to our abstract construction of R in ASD, which
will start with our formulation of Dedekind cuts in Section 6. In this section we shall use theHeine–Borel theorem to prove an abstract property of R, from which we deduce the fundamental
theorem of interval analysis. The same abstract property, taken as an axiom, will be the basis of
our construction of R and proof of the Heine–Borel theorem in ASD.
Remark 2.1 Dedekind [Ded72] represented each real number a ∈ R as a pair of sets of rationals,{d | d ≤ a} and {u | a < u}. This asymmetry is messy, even in a classical treatment, so it is better
to use the strict inequality in both cases, omitting a itself if it’s rational. So we write
Da ≡ {d ∈ Q | d < a}and Ua ≡ {u ∈ Q | a < u}.

These are disjoint inhabited open subsets that “almost touch” in the sense thatd < u =⇒ d ∈ D ∨ u ∈ U.
This property is usually known as locatedness.
The idea that a set of rationals is open in the usual topology on R and extends towards ±∞can be expressed order-theoretically, using a condition that we shall call roundedness:d ∈ D ⇐⇒ ∃e. d < e ∧ e ∈ D

and5u ∈ U ⇐⇒ ∃t. t < u ∧ t ∈ U.

A real number represented as a cut is therefore a pair of subsets, i.e. an element of P(Q) × P(Q),that is rounded, bounded (i.e. inhabited), disjoint and located.
Exercise 2.2 If ∆ ⊂ R is an open set of reals that extends downwards, show that D ≡ ∆ ∩ Q isa rounded set of rationals with the same property, and that this defines a bijection between such
subsets, where ∆ ≡ {r ∈ R | ∃q ∈ D. r < q}. In future we shall write D for either representation,and pass between them without comment; in particular, in “R \ (D ∪ U )” below, real as well as
rational numbers are removed.
Definition 2.3 It is very useful to generalise the notion of Dedekind cut by dropping the locatedness condition. Instead of almost touching, and so representing a single real number a ∈ R, sucha pseudo-cut corresponds classically to a closed interval [d, u] ≡ R \ (D ∪ U ). We sometimes
weaken the other conditions too, allowing D ≡ ∅ and d ≡ −∞, or U ≡ ∅ and u ≡ +∞.
The extension of the arithmetic operations to such intervals was defined by Ramon Moore[Moo66]:[d, u] ⊕ [e, t] ≡ [d + e, u + t]
[d, u]≡ [−u, −d][d, u] ⊗ [e, t] ≡ [min(de, dt, ue, ut), max(de, dt, ue, ut)][d, u]−1≡ [u−1 , d−1 ]if 0 ∈/ [d, u], so 0 ∈ D ∪ U≡ [−∞, +∞]if 0 ∈ [d, u].

The formula for multiplication is complicated by the need to consider all possible combinations ofsigns.
Remark 2.4 Moore’s interval analysis has been used to develop a variety of numerical algorithms; see [Kea96] for a brief survey with an extensive bibliography. Amongst these, we focus
on what it achieves for the problem of optimisation. By this, we understand finding the maximum value of a continuous function defined on a non-empty compact domain, but not necessarily
any location where the function attains that value. Plainly, any value of the function provides alower bound for the maximum, but finding upper bounds is problematic using standard numericalmethods, especially when the function has “spikes”.
For the sake of illustration, consider an arithmetical function f : [0, 1]n → R. If this is justaddition or multiplication, Moore’s interval operations provide the minimum and maximum valuesof the function on the domain directly. For a more complicated arithmetical function, we interpretthe operations according to Moore’s formulae, and may (if we’re lucky) still obtain the minimum
and maximum.
In general, however, the result of Moore’s interpretation will be an interval that contains
the required image. In other words, it provides an upper bound of the maximum — exactly
what standard numerical methods find difficult. Unfortunately, this may be a vast over-estimate,especially when the definition of the function is complicated and involves subtraction of similarlarge numbers, so this does not really help very much with spiky functions.
In fact, Moore and his followers have provided various techniques for reducing the sizes of theresulting intervals. One of these simply massages the arithmetic expression to reduce multiple
occurrences of variables and sub-expressions, since computing x − x introduces a large error thatcan easily be avoided. However, these techniques are not the purpose of the present discussion.
Remark 2.5 We regard Moore’s definitions as merely one way of extending certain continuousfunctions to take intervals instead of real numbers as arguments. In fact, that’s exactly the point:(a) ideally, we extend f to the operation F0 that takes intervals to intervals by
F0 [d, u] ≡ {f x | x ∈ [d, u]},6

(b) but in practice, Moore’s operations extend a general arithmetic expression f to some continuous operation F on intervals such that
F [a, a] = [f a, f a]

and F0 [d, u] ⊂ F [d, u].

Whilst Moore’s interpretation may give a huge over-estimate of the image if we don’t rewrite theexpression, it has an important technical property, namely that it preserves (syntactic) compositionof arithmetic expressions, so it is easily performed by a compiler.
The first question that this raises is whether the ideal operation F0 , which (a) defines set-theoretically, is continuous. Then we can ask whether there is a way of computing it, using (b).
Continuity is crucial to our whole development: not only that of the single operation F0 , butalso for the process that extends f to F or F0 . However, as P(Q) is a complete lattice, rather thana space that has a familiar Hausdorff topology motivated by geometry, we first have to describe
what its topology is. (In this paper, we do not even attempt to put a topology on RR .)Definition 2.6 Let L be a complete lattice such as P(Q). Then a family U ⊂ L is called Scott
open [Sco72a, GHK+ 80] if it is(a) an upper set, so if U ∈ U and U 6 V then V ∈ U; andWW(b) “inaccessible by directed unions”, i.e. if ( i∈I Ui ) ∈ U then already ( i∈F Ui ) ∈ U for somefinite subset F ⊂ I.
This Scott topology is never Hausdorff (except, that is, on the trivial lattice).
A function f : L1 → L2 between complete lattices is continuous with respect to the Scott
topology iff it preserves directed unions. In particular, it is monotone, i.e. if x 6 y in L1 thenf x 6 f y in L2 . See [J] for a brief account of this topology that is enough for its use here.
Exercise 2.7 Let L be the topology (lattice of open subsets) of any topological space X, andK ⊂ X any subset. Show that the family U ≡ {U | K ⊂ U } of open neighbourhoods of K is
Scott open iff K is compact in the usual “finite open sub-cover” sense. If this is new to you, you
would be well advised to stop at this point to see for yourself why this is the case, since this idea
is fundamental to our whole programme.

Example 2.8 Let L ≡ R ≡ R + {−∞, +∞}, considered as a complete lattice in the arithmeticalorder, so +∞ is the top element. Equipped with the Scott topology, this space arises in real
analysis because lower semicontinuous functions X → R are just functions X → R that arecontinuous in the sense of general topology. We shall see, however, that it is a mistake to think of
R as derived from R in this clumsy way: it is really simpler and more fundamental than R itself.
Its elements, which we call ascending reals, are given by Exercise 2.2, i.e. in a similar way to
the Dedekind reals, except that only the lower cut D ⊂ Q is used. The descending reals, R, aredefined in the same way, but with the opposite order, and are related to upper semicontinuousfunctions. The words “ascending” and “descending” relate the usual temporal language about thereal line to the vertical intuition of lattice theory.
Remark 2.9 It is useful theoretically to consider more general intervals than Moore did, i.e. notnecessarily having rational endpoints. For example, a computation that is allowed to continue
forever may generate a converging pair of sequences of rationals,
d 0 < d 1 < d 2 < · · · < u2 < u 1 < u 0 ,whose limits sup dn and inf un we would like to see as the ‘ultimate result’ of the computation.
7

T If these limits exist in R, say d ≡ sup dn and u ≡ inf un , then [d, u] is the (directed) intersection[dn , un ]. However, d and u are best seen as ascending and descending reals,D ≡ {d | ∃n. d < dn } ∈ R

andU ≡ {u | ∃n. u > un } ∈ R,

since, constructively, they need not exist as members of the usual “Euclidean” structure (Remark 15.1). Nevertheless, the intersection of the closed intervals does exist: it is R \ (D ∪ U ), andis always a closed subspace.
Notice that the open subsets D and U represent positive information, namely the lower andupper bounds that we have verified so far for the real number that we’re trying to calculate. The
closed interval [d, u], on the other hand, consists of the candidate real numbers that we have notyet excluded, which is negative information.
Definition 2.10 We can consider these generalised intervals as members of the interval domain, IR [Sco72b, ES98]. The order relation is traditionally defined as reverse inclusion of closed
intervals, and so directed joins are given by intersection.
According to our preferred view, an interval is defined as a generalised Dedekind cut (D, U ),and the order relation is the forward inclusion of these sets. As we acquire more information about
the number, in the form of tighter bounds, the correspondingly narrowing interval goes up in theorder on the domain.
We shall now start using some of the notation of the calculus that we intend to introduce.
Notation 2.11 Classically, any subset D ⊂ Q may be represented as a function Q → {>, ⊥} thatsays whether or not each d ∈ Q belongs to D. Since we believe that topology is fundamental, we
give this target set the Scott topology. It then becomes the Sierpiński space,  in which just one
singleton {>} is open, making the other {⊥} closed. It therefore looks like

• , and we shall callit Σ.
Since Q is discrete, it doesn’t change much to require our functions Q → Σ to be continuous.
However, for a general topological space X (such as R), continuous functions φ : X → Σ correspondbijectively to open subspaces U ⊂ X, by U ≡ φ−1 (>). We shall say that φ classifies U .
Notation 2.12 Having passed from the (open) subset D ⊂ Q to a (continuous) function δ : Q → Σ,
we also replace set-theoretic notation with the λ-calculus. A function x 7→ φ(x) is written as a
λ-abstraction λx. φ(x); we use nested λ-abstractions for several variables, but write λxy. σ insteadof λx. λy. σ. Application φ(a) is written without parentheses, φa. Expressions built from λabstractions and applications are called λ-terms.
So in ASD we represent D and U by λ-terms δ, υ : ΣQ , adopting the convention of using Greek
letters for terms of this type. Many authors in computer science would write Q → Σ instead of ΣQ ,which is the notation in pure mathematics. Membership d ∈ D is written δd, and set-formation
becomes λ-abstraction. In particular, Da and Ua becomeδa ≡ λd. (d < a)andυa ≡ λu. (a < u),so δa d means d < a. Then any real number can be represented as a pair (δ, υ) of λ-terms, and thereal line as a whole is a subset R ⊂ ΣQ × ΣQ .
Remark 2.13 We want to use this representation to compute with real numbers, and in the first
instance to do arithmetic with them. Dedekind indicated how this can be done, defining operations
on cuts. But there is a difference between his objective of providing a rigorous foundation fordifferential and integral calculus, and ours of getting a machine to compute with real numbers. He
8only had to define and justify the operations on legitimate cuts (those that are rounded, bounded,disjoint and located), whereas our machine will do something with any pair of λ-terms that wegive it, even if that’s only to print an error message.
It’s reasonable to ask that any program F that is intended to compute a function f : R → R
using Dedekind cuts will actually take any pair of λ-terms and return another such pair. We
say that the program is correct for this task if, when it is given the pair (δa , υa ) that represents
a number a, it returns the pair (δf a , υf a ) that represents the value f (a) of the function at that
input. In other words, the square on the left commutes:
i
Rf
?
R-

i

i

- ΣQ × ΣQ
..
..
..
..
.. F
..
..
..?
Q
- Σ × ΣQ

- ΣQ × ΣQ
.....
.....
.
.
.
.
.....
φ
....Φ
.
.
.
.
.
.....
?......
ΣR-

Remark 2.14 We shall not attack the problem of extending functions directly. It is simpler andmore in keeping with the ideas of computation, Dedekind cuts and topology to consider first how
an open subset of R may be extended to one of ΣQ × ΣQ .
Recall from Notation 2.11 that such an open subset is classified by a continuous function taking
values in Σ. We expect the function φ from R (classifying an open subset of it) to be the restrictionof a function Φ from ΣQ × ΣQ (classifying an open subset of that), making the triangle on theright above commute. In other words, R should carry the subspace topology inherited from theambient space, ΣQ × ΣQ , which itself carries the Scott topology.
This extension of open subspaces is actually the fundamental task, since we can use it to extend
functions by definingF (δ, υ) ≡ λd. Φd (δ, υ), λu. Ψu (δ, υ) ,where Φd and Ψu are the extensions of φd ≡ λx. (d < f x) and ψu ≡ λx. (f x < u) respectively.
The extension process must therefore respect parameters. We implement this idea by introducing a new operation I that extends φ to Φ in a continuous, uniform way, instead of a merely
existential property of the extension of functions or open subspaces one at a time. This depends
on an understanding of Scott-continuous functions of higher type.
Q

Q

Proposition 2.15 Classically, there is a map I : ΣR  ΣΣ ×Σ , defined by(V ⊂ R) open 7→ {(D, U ) | ∃d ∈ D. ∃u ∈ U . (d < u) ∧ [d, u] ⊂ V }in traditional notation, or
φ : ΣR 7→ λδυ. ∃du. δd ∧ υu ∧ (d < u) ∧ ∀x:[d, u]. φxQQin our λ-calculus, that is Scott-continuous. It makes ΣR a retract of ΣΣ ×Σ , as it satisfies theequationΣi · I = idΣRorx : R, φ : ΣR ` Iφ(ix) ⇔ φx,where ix ≡ (δx , υx ) : ΣQ × ΣQ . This expresses local compactness of R.
Proof The Heine–Borel theorem, i.e. the “finite open sub-cover” definition of compactness forthe closed interval [d, u], says exactly that the expression “[d, u] ⊂ V ” is a Scott-continuous

9

predicate in the variable V : ΣR (Exercise 2.7). Thus the whole expression for I is a Scottcontinuous function of V . This satisfies the equation because, if φ classifies V ⊂ X,
φa ≡ (a ∈ V ) 7→ Iφ(ia) ≡ ∃du. a ∈ (d, u) ⊂ [d, u] ⊂ V ⇐⇒ (a ∈ V ).
The argument so far has relied on the prior existence of R. The next step is to eliminate real
numbers in favour of rational ones.
Lemma 2.16 Since Φ : ΣQ × ΣQ → Σ is a Scott-continuous function,
Φ(δf , υs )⇐⇒∃et. (e < f ) ∧ (s < t) ∧ Φ(δe , υt )(a)

Φ(δx , υx )⇐⇒∃mk. (pk−1 < x < pk+1 ) ∧ Φ(δpk−1 , υpk+1 )(b)where pk ≡ d + 2−m k(u − d), for any chosen d < u. Although pk also depends on m, d and u, weomit them to simplify the notation: they should be understood to come from the expression inwhich pk is embedded.
Proof

In traditional notation, the unions
[
6
De
Df =

and Us =

[
6
Ut
s<t

e<f

are directed, cf. Remark 2.9, so Φ preserves them. The equations above say the same thing in our
λ-calculus (Notation 2.12). Notice that (⇐) is monotonicity. Having enclosed the point x in someopen interval (e, t), we may find m and k so that e < pk−1 < x < pk+1 < t.
QQ

Proposition 2.17 The idempotent E ≡ I · Σi on ΣΣ ×Σ is given byEΦ(δ, υ) ≡ ∃n ≥ 1. ∃q0 < · · · < qn . δq0 ∧ υqn ∧n−1^

Φ(δqk , υqk+1 ).

k=0

Proof

Substituting ix ≡ (δx , υx ) into the definition of I in Proposition 2.15,
(I · Σi )Φ(δ, υ) ≡ I λx. Φ(ix) (δ, υ) ≡ ∃du. δd ∧ υu ∧ (d < u) ∧ ∀x:[d, u]. Φ(δx , υx ).

[E 6 I · Σi ]: Although the formula for E essentially involves abutting closed intervals,[d, u] = [q0 , q1 ] ∪ [q1 , q2 ] ∪ · · · ∪ [qn−1 , qn ],part (a,⇒) of Lemma 2.16 expands each of them slightly, from [qk , qk+1 ] to [e, t]. Then eachx ∈ [d, u] lies inside one of the overlapping open intervals (e, t):EΦ(δ, υ) ⇒∃q0 . . . qn . δq0 ∧ υqn ∧n−1^∃et. (e < qk < qk+1 < t) ∧ Φ(δe , υt )k=0⇒∃du. d < u ∧ δd ∧ υu ∧ ∀x:[d, u]. ∃et. (e < x < t) ∧ Φ(δe , υt )⇒∃du. d < u ∧ δd ∧ υu ∧ ∀x:[d, u]. Φ(δx , υx ),where the last step uses Lemma 2.16(a,⇐) with f ≡ s ≡ x.
[E > I · Σi ]: For the converse, Lemma 2.16(b,⇒) also encloses each point x ∈ [d, u] in an open
interval (pk−1 , pk+1 ) 3 x with dyadic endpoints, such that Φ(pk−1 , pk+1 ) holds. Although some10

points x may â priori need narrower intervals than others, with larger values of m, the Heine–
Borel theorem says that finitely many of them suffice, so there is a single number m that serves
for all x ∈ [d, u]. Another way of saying this is that the universal quantifier ∀x : [d, u] is Scottcontinuous, preserving the directed join ∃m.
∀x:[d, u]. Φ(δx , υx )⇒∀x:[d, u]. ∃m:N. ∃k. (pk−1 < x < pk+1 ) ∧ Φ(δpk−1 , υpk+1 )⇒∃m. ∀x:[d, u]. ∃k. (pk−1 < x < pk+1 ) ∧ Φ(δpk−1 , υpk+1 )

⇒

∃m.

m

2
^

⇒

Φ(δpk−1 , υpk+1 )

∃m.

k=0

−1
2m
^

Φ(δpk , υpk+1 ),k=0where we trim the intervals using Lemma 2.16(a,⇒) and omit the last one. Then n ≡ 2m ,q0 ≡ p0 ≡ d, q1 ≡ p1 , . . . , qn ≡ p2m ≡ u provide a sequence to justify EΦ(δ, υ).

Remark 2.18 Notice that this formula for E involves only rational numbers (and predicates onthem) but not reals. We can write this formula with very little assumption about the underlying
logic. The role of the classical Heine–Borel theorem was to define a different map, I, to prove that
it is Scott-continuous and that it satisfies the equations
Σi · I = idΣR

and I · Σi = E.

It is the formula E — not the classically defined map I or the accompanying proof — that we shalluse to construct the real line in ASD. In Section 15 we shall discuss some systems of analysis inwhich the Heine–Borel theorem fails, and the operation I does not exist either.
Besides the construction of R in ASD, the formula is important for many other reasons. In
particular, it shows how Moore’s interval arithmetic solves the optimisation problem, and justifies
the interval-subdivision algorithms that have been developed using interval analysis. It would beappropriate to call it the fundamental theorem of interval analysis. Moore himself proved
it [Moo66, Chapter 4] using convergence with respect to the metric∂ [d, u], [e, t] ≡ max |d − e|, |u − t| .
Corollary 2.19 Let f : R → R be a continuous function and F be any continuous extension off to intervals (Remark 2.13). For example, if f is an arithmetic expression then F may be its
interpretation using Moore’s operations. Suppose that e and t are strict bounds for the image of[d, u] under f , so
∀x:[d, u]. e < f x < t,or, equivalently, F0 [d, u] ⊂ (e, t),where F0 gives the set-theoretic image. Then there is some finite sub-division (which could bechosen to be dyadic), d ≡ q0 < q1 < · · · < qn−1 < qn ≡ u, such that(e, t) ⊃n−1[

F [qk , qk+1 ].

m=0Moreover, we obtain F0 from F in Remark 2.5 using E and Remark 2.14.

11This sub-division could be found by a recursive program that either applies the function Moorewise to the whole interval, or splits it and calls itself on each half.
Remark 2.20 Finally, some curious things happen in both interval analysis and ASD when weplay around with the formulae. Of course, if a < b then the subsets
D ≡ Db ≡ {d | d < b}and U ≡ Ua ≡ {u | a < u}overlap. But we may still apply Proposition 2.15 to them, obtaining the existential quantifier,(Db , Ua ) ∈ IV ⇐⇒ ∃x:[a, b]. x ∈ V.
We shall see in Section 10 that both quantifiers are derived from E like this.
Given that ∀ is related to over estimation of the range of a function in interval analysis, could
this back-to-front version for ∃ yield an under estimate? It is obviously very dangerous in this caseto rely on any intuition of an interval as a single closed set, as is common in the literature on
interval analysis. On the other hand, there is no problem in dealing with a back-to-front intervalin our formulation of it as a pair (D, U ) of (now overlapping) open sets.
In order to exploit this idea, we would have to begin with a careful study of the arithmetic,
which was introduced by Edgar Kaucher [Kau80]. Addition and subtraction are as in Remark 2.3,
but multiplication is more complicated (Lemma 12.1). Various authors have used Kaucher’sarithmetic to investigate questions of linear algebra, logic and underestimation, e.g. [KNZ96,
Lak95].

3

Topology as lambda-calculus

Now we shall introduce Abstract Stone Duality. It is a direct axiomatisation of general topology
whose aim is to integrate it with computability theory and denotational semantics, without sacrificing important properties such as the Heine–Borel theorem. The basic building blocks — spaces
and maps — are taken as fundamental, rather than being manufactured from sets by imposing
extra structure.
The ASD calculus formalises the notation that we have already used for the set-theoretic
constructions in the previous section (Notation 2.11ff):(a) the Sierpiński space Σ and its lattice structure;(b) λ-terms of type ΣX to encode open subspaces of X;(c) ∃ for combinatorial structure;(d) ∀ to say when the direct image of a closed bounded interval is contained in an open interval;(e) real numbers represented as Dedekind cuts, considered as pairs (δ, υ) of λ-terms; and(f) the Σ-splitting I that is related to compactness of the interval [d, u].
As a type theory, ASD has types, terms and equations between terms. The types are also called
spaces, and the terms maps or functions. The three basic spaces 1, N and Σ are axiomatised bytheir universal properties. From them, we may construct products, X × Y , and exponentials of
the form ΣX , but not arbitrary Y X . The theory also provides certain “Σ-split” subspaces, and it
is our main objective to construct R in this way, using the idea of Proposition 2.15.
As Notation 2.11 suggests, terms of type ΣX behave very much like predicates on X, and, morebasically, those of type Σ like propositions. We can form conjunctions and disjunctions of suchterms, but not implications or negations — these become equations between terms. In some cases
there are also operators ∃X : ΣX → Σ and ∀X : ΣX → Σ that satisfy the same formal properties12

as the quantifiers (cf. Remark 4.16). A space X is called compact when it has a ∀X operator, andovert when it has ∃X .
Statements in the theory are expressed as equations between terms, but we use 6 or ⇒ assyntactic sugar in the lattices ΣX and Σ. Since not every formula of (for example) the predicate
calculus is of this form, the theory imposes limitations on what can be said within it.
You may think that we are making a rod for our own backs by restricting ourselves to sucha weak calculus. This criticism puts us in good company with constructive mathematicians, who
often face the same lack of understanding. Indeed, one of the reasons why the papers on ASD are
so long is that proofs in weak calculi — where they exist at all — necessarily have far more steps
than those in stronger systems: it’s like digging a trench with a teaspoon.
But the ASD calculus is the calculus of spaces and maps. If some feature is missing from it, thisis not because of our asceticism, but because spaces and maps do not possess it. The justificationof this claim is that, starting from the axioms of ASD, we may reconstruct the categories ofcomputably based locally compact locales [G] and of general locales over an elementary topos [H].
In such a weak calculus, it will not surprise you to hear that, as a rule, it is very difficult toknow how to say anything at all. But experience has shown something very remarkable, namely
that, once we have some way of expressing an idea, it usually turns out to be the right way.
In contrast, stronger calculi, i.e. those that take advantage of the logic of sets, type theory or a
topos, offer numerous candidates for formulating an idea, but these then often lead to distracting
counterexamples.
It will be useful to state the formal relationship between ASD and traditional topology.
Definition 3.1 In the classical interpretation of ASD, each type X denotes a locally compact
topological space. This space need not be Hausdorff, so by “local compactness” we mean thateach x ∈ U ⊂ X has some x ∈ V ⊂ K ⊂ U ⊂ X, where U and V are open and K is compact[GHK+ 80]. Similarly, each term x : X ` f x : Y denotes a continuous function f : X → Y . Allmaps between spaces are continuous, simply because the calculus never introduces discontinuousfunctions.
The exponential ΣX is the topology (lattice of open subspaces) of X, regarded not as a set
but as another topological space, equipped with the Scott topology (Definition 2.6); since X is
locally compact, ΣX is a continuous lattice. Maps ΣX → ΣY are Scott-continuous functions. The
connectives >, ⊥, ∧ and ∨ are interpreted in the obvious way in the lattice, and ∃N by N -indexed
unions or joins. When K is a compact space, ∀K : ΣK → Σ denotes the Scott-continuous function
in Exercise 2.7.
Remark 3.2 We usually think of a map φ : X → Σ as representing an open subspace of X,
namely the inverse image of the open point > ∈ Σ. But, by considering the inverse image of theclosed point ⊥ ∈ Σ instead, the same term also corresponds to a closed subspace.
Hence there is a bijection between open and closed subspaces, but it arises from their common
classifiers, not by complementation. Indeed, there is no such thing as complementation, as there
is no underlying theory of sets (or negation).
This extensional correspondence between terms and both open and closed subspaces gives rise
to Axiom 4.7 and Lemma 4.9, which are known as the Phoa principle. This makes the difference
between a λ-notation for topology that must still refer to set theory to prove its theorems, and acalculus that can prove theorems for itself, indeed in a computational setting. It was the subjectof the first published paper on ASD [C].
Constructive or intuitionistic logicians may, however, feel uncomfortable using this axiom,
because it looks like classical logic. Nevertheless, the “classical” interpretation above is also valid
for intuitionistic locally compact locales (LKLoc) over any elementary topos.
13

The reason for this is that ASD is a higher-order logic of closed subspaces, just as much as it
is of open ones. When it is functioning in its “closed” role, we are essentially using the symbols
the wrong way round: for example, ∨ denotes intersection.
The discomfort will be particularly acute in this paper, as it deals with a Hausdorff space,
where the diagonal R ⊂ R × R is closed (Definition 4.12). This means that we can discuss equalityof two real numbers, a, b : R, using a predicate of type Σ. But since the logic of closed predicatesis upside down, the (open) predicate is a 6=R b, and for equality we have to write the equation(a 6= b) ⇔ ⊥ between terms of type Σ. For the integers, on the other hand, we can state equality
as (n = m) ⇔ >.
That equality of real numbers is “doubly negated” like this was recognised by Brouwer,
cf. [Hey56], and arguably even by Archimedes. However, we stress that this is not what weare doing in ASD: 6= is primitive, not derived from equality, and there is no negation of predicates.
The equational statements (−) ⇔ > and (−) ⇔ ⊥ merely say that the parameters of the expression (−) belong respectively to certain open or closed subspaces. These are of the same status in
the logic.
Remark 3.3 As we shall see, it is the part of the calculus that concerns (sub)types that is crucial
to the compactness of the closed interval.
There are many approaches to topology that are based on sets of points, although the word“set” may be replaced by (Martin–Löf) type or object (of a topos), and “functions” may be
accompanied by programs. In all of these systems, a new object X is constructed by specifying a
predicate on a suitable ambient object Y , and then carving out the desired subobject i : X  Yusing the subset-forming tools provided by the foundations of the system. For example, the realline may be constructed as the set (type, object) of those pairs (D, U ) or (δ, υ) that satisfy theproperties required of a Dedekind cut.
What is the topology on such a subset? We fall on the mercy of the underlying logic of sets ofpoints to determine this, and so to prove important theorems of mathematics such as compactnessof the real closed interval. As we shall see in Section 15, in many interesting logical systems,
especially those that are designed to capture recursion, the logic may not oblige us with a proof,
but may yield a counterexample instead.
We consider that this topological problem is not about the underlying logic but about theexistence of certain continuous functions of higher type. We saw in Proposition 2.15 that, in theclassical situation, we may use the Heine–Borel theorem to define a Scott-continuous map I that
extends any open subset of X ≡ R to one of Y ≡ ΣQ × ΣQ . The other foundational systems inwhich Heine–Borel is provable can also define this map, whilst others do neither.
The key feature of Abstract Stone Duality is that it provides the map I : ΣX  ΣY (calleda Σ-splitting) axiomatically whenever we define a subspace i : X  Y , thereby taking accountof the intended topology. It is important to understand that the types that are generated by thelanguage that we describe are therefore abstract ones, not sets of points.
The essence of our construction in the rest of the paper is then that the quantifier ∀[0,1] thatmakes [0, 1] compact may conversely be derived from this map I.
Beware, however, that there are some subspaces (equalisers, Definition 5.3) that have no Σsplitting in ASD or any other system of topology. For example, i : NN  ΣN×N can be expressed as
an equaliser of topological spaces or locales, but it does not have a Scott-continuous Σ-splitting I.
The direct image map, called i∗ , does satisfy the relevant equation, i∗ · i∗ = id, where i∗ is localic
notation for our Σi , but i∗ is only monotone, not Scott-continuous. Consequently, NN is notdefinable in ASD as the calculus is described here. On the other hand, a particular inclusion may
have many different Σ-splittings, as we shall find in Section 7.
We formalise the subspace calculus in Section 5. However, as we shall see in Sections 7 and 8,
it is not as easy to use as set-theoretic comprehension — the rule has been to introduce only one
14subspace per paper. So far, it only gives a robust account of locally compact spaces, but there iswork in progress to extend it.
Remark 3.4 Since ASD is presented as a λ-calculus, it is reasonable to ask whether(a) it is powerful enough for us to write programs in it;(b) it has some computational interpretation, at least in principle; and(c) we can actually print out digits of real numbers using it.
Each of these questions deserves a paper in itself. You will find several remarks here that are motivated by practical computation, and we are actively thinking about a prototype implementation[Bau08], but we do not say very much about it in this paper.
The language was indeed partly inspired by ideas from theoretical computer science. Computation is a natural part of the calculus, and there is no need to bolt a clumsy, old-fashioned theoryof recursion on to the front of it. Domain theory can be developed within ASD [F], and thenprogramming languages such as Plotkin’s PCF can be translated into this, using the denotationalsemantics in [Plo77].
Computationally, we understand the elements > and ⊥ of Σ as termination (“yes”) and nontermination (“wait”) respectively; Σ is not a “Boolean” type, as there is no definite “no”. Thenaı̈ve interpretation of the Phoa principle is then that any function F : Σ → Σ is specified by its
effect on these two possible inputs. It cannot interchange them, as that would solve the Halting
Problem, so F ⊥ ⇒ F >, leaving essentially only three possible behaviours. More generally, all maps
ΣY → ΣX are monotone with respect to the lattice order in both topology and computation.
In fact, ASD is topologically more expressive than domain theory: its types denote exactly
the “computably based” locally compact locales, and the maps are the computable continuousfunctions [G].
Conversely, the topological features of the calculus can be “normalised out” of its terms [A, §11].
Given that the most important type, Σ, captures propositions rather than functions, the resultof this normalisation is a kind of logic program. However, to put this into practice would require
a combination of three different generalisations of Prolog, namely the addition of λ-calculus,
parallelism (for ∨) and the manipulation of intervals or constraints.
In logic programming, a predicate is interpreted as a program whose objective is to find a proof
and report instantiations for the free and existentially bound variables. If the predicate is false,
the program never halts (in a “successful” way: it might abort). The basic process for doing thisis unification, in which variables are assigned values according to the constraints imposed by therest of the program, i.e. the values that they must have if the program is ever to terminate with aproof of the original predicate. The usual notion of unification only makes sense for combinatorial
structures, but [Cle87] suggests an analogue for the reals.
Remark 3.5 Applying this to the issues of constructivity in the Introduction, logic programming
gives an effective meaning to the existential quantifier. However, in ASD this is weaker than thatfound in other constructive foundational systems: in our version the free variables of the predicate
must also be of overt discrete Hausdorff type. That is, they must be either natural numbers orsomething very similar, such as rationals. They cannot be real numbers, functions or predicates.
Our choice principle is therefore only N–N for Σ01 -predicates. This is topologically significant,because it constrains the sense in which the closed interval has the Heine–Borel “finite sub-cover”
property in Section 10.
As you would expect, “de Morgan” duality between ∧ and ∨ extends to the quantifiers, i.e. from∃ to ∀. Once again, however, this is different in ASD from proof theory: whilst ∃ is true more
often in ASD, ∀ is true less often, as we shall explain in Section 15.

15

4

The ASD lambda calculus

This section and the next summarise the symbolic language for ASD in a “user manual” style.
Beware, however, that the manual for some device does not make its engineering redundant,
and indeed the development of the more powerful devices of the future depends on advances in
the underlying principles. Nevertheless, the constructions in the rest of this paper will be madeentirely within this calculus. We repeat that there is no underlying set theory, and that themonadic and Phoa principles are unalienable parts of the system. On the other hand, there areother formulations of Scott continuity of various strengths besides the one that we give here.
Axiom 4.1 The types of ASD are generated from(a) base types 1, Σ and N, by(b) products, X × Y ,(c) exponentials, ΣX , or X → Σ if you prefer, and(d) Σ-split subspaces.
We do not introduce general exponentials Y X , infinitary products, type variables or dependent
types — at least, not in this version of the calculus. We will explain Σ-split subspaces, which
abstract Proposition 2.15, in the next section; they will be used to define open, closed and retract
subspaces, and, of course, R itself.
Axiom 4.2 The logical terms of type Σ or ΣU (also known as propositions and predicates
respectively) are generated from(a) constants > and ⊥;(b) the lattice connectives ∧ and ∨ (but not ⇒ or ¬);(c) λ-abstraction λx. φ, where φ must itself be logical (i.e. of some type of the form ΣV , and inparticular not N or R), but x may be of any type;(d) λ-application φa, where a : A, and φ : ΣA is logical;(e) equality (n =N m), where N is any discrete type;(f) inequality or apartness (h 6=H k), where H is any Hausdorff type;(g) existential quantification ∃x:X . φx, where φx is logical, and the type X is overt;(h) universal quantification ∀k:K . φk, where φk is logical, and the type K is compact.
These terms are generated within a larger calculus that also includes(i) variables of all types, for which we use increasingly exotic alphabets as the types get more
complex; and(j) pairing h , i and projections π0 , π1 for product types.
Discrete, Hausdorff, overt and compact spaces will be defined shortly. Existential quantification
over N or R is allowed, but universal quantification is not. Universal quantification over the closed
interval I ≡ [0, 1] is justified in Section 10.
So examples of invalid logical formulae include√
λn. n + 3, λx. 3 x, π =R 3.14159, ∀n. ∃pq. 2n = p + q and ∀x. x2 6= −1,
but (∃npqr:N. pn +q n = rn ) and (∀x:|x| ≤ 2. x2 < 0) are fine. Programs to which an Ml compiler
would assign the types nat → nat or real → real are treated in ASD as terms of type N → N⊥
or R → R⊥ [D, F].

16

Binding, renaming, duplication, omission and substitution for variables are the same as inthe λ- and predicate calculi. A quantified formula has the same type as its body (φ), whilst λabstraction and application modify types in the usual way. Alternating quantifiers are allowed toany depth — so long as their ranges are overt or compact spaces.
Axiom 4.3 The numerical terms of type N are generated from(a) the constant 0;(b) variables;(c) successor; and(d) definition by description: the n. φn (Axiom 4.24).
(e) We also allow primitive recursion over N at any type X.
Definition 4.4 Judgements in the calculus are of the four forms` X type,Γ ` a : X,Γ ` a=b:Xand Γ ` α 6 β : ΣX ,asserting well-formedness of types and typed terms, and equality or implication of terms. We shallrefer to a = b and α 6 β on the right of the ` as statements. On the left is the context Γ,
consisting of assignments of types to variables, and maybe also equational hypotheses [E, §2].
The form Γ ` α 6 β : ΣX is syntactic sugar:
Axiom 4.5 The predicates and terms satisfy certain equational axioms, including(a) those for a distributive lattice; in particular, for Γ ` φ, ψ : ΣX we write
φ 6 ψ

to mean φ ∧ ψ = φ,or equivalently

φ ∨ ψ = ψ,although for σ, τ : Σ we use σ ⇒ τ and σ ⇔ τ instead of σ 6 τ and σ = τ , since we shall alsoneed the symbols ≤ and = for their more usual “numerical” meanings;(b) the β- and η-rules for λ-abstraction/application and pairing/projection;(c) the β- and η-rules for primitive recursion over N; and(d) others that we describe in a little more detail in the rest of this section.
Remark 4.6 Predicates and terms on their own denote open subspaces and continuous functions
respectively, but their expressive power is very weak. We introduce implications into the logic,
but make their hierarchy explicit, in the form of statements and judgements.
(a) Observe, first, that 6, =, ⇒ and ⇔ link predicates to form statements, not new predicates.
In other words, Σ is a lattice and not a Heyting algebra.
(b) There are equality statements a = b : X for any type, but equality predicates (n =N m) : Σ
only for discrete types. In particular, for a, b : R, there are predicates a 6= b and a < b, but
a = b and a ≤ b are statements, since R is Hausdorff but not discrete.
(c) For any proposition σ, we sometimes write σ or ¬σ for the statements σ ⇔ > or σ ⇔ ⊥.
(d) Nested equality and implication are not allowed in statements: we use a judgement of theform α2 ⇒ β1 ` γ1 ⇒ δ0 instead. If we need another level of nesting, we use a proof rule:
α3 ⇒ β2`γ2 ⇒ δ12 ⇒ ζ1`η1 ⇒ θ017See Exercise 6.17 for some examples. This is as far as we can go. This rather artificial limit
will be rectified in a future extended calculus [M].
(e) Equality and implication statements for function-types ΣX provide a way of stating quantification over any type X — as a statement — it’s a predicate only when X is compact.
However, for the sake of clarity, we usually write Γ, x : X ` φx ⇔ ψx instead of Γ ` φ = ψ.
Our convention is that λ-application binds most tightly, followed by the propositional relations,then ∧, then ∨, then λ, ∃ and ∀, then ⇒, ⇔, 6, = and finally `. This reflects the hierarchyof propositions, predicates, statements, judgements and rules. We often bracket propositional
equality for emphasis and clarity.
Axiom 4.7 In addition to the equations for a distributive lattice, Σ satisfies the rules1
Γ, σ ⇔ > ` α ⇒ β=================Γ ` σ∧α ⇒ βΓ, σ ⇔ ⊥ ` β ⇒ α=================
Γ ` β ⇒ σ∨α

Axiom 4.8 Every F : ΣΣ is monotone, i.e. F ⊥ ⇒ F >.
Lemma 4.9 Σ satisfies the Phoa principle, F σ ⇐⇒ F ⊥ ∨ σ ∧ F >, for F : Σ → Σ and σ : Σ,possibly involving parameters.
Plainly Phoa entails monotonicity, and we shall explain shortly why the Gentzen-style rules in
Axiom 4.7 are also derivable from it.
Definition 4.10 We say that φ : ΣX classifies an open subspace of X, and co-classifies aclosed one. In symbols, for a : X,a ∈ U (open) if φa ⇔ > and a ∈ C (closed) if φa ⇔ ⊥,so U ⊂ U 0 iff C 0 ⊂ C iff φ 6 φ0 . This means that
open subspaces of X,

closed subspaces of X

and continuous functions X → Σ

are in bijection. A clopen, complemented or decidable subspace is one that is both open andclosed. Then it and its complement are the inverse images of 0, 1 ∈ 2 under some (unique) map
X → 2 [B, Theorem 11.8] [C, Proposition 9.6].
Remark 4.11 Such inverse image types cannot of course be generated from N and Σ by × andΣ(−) . Our comments here will be justified by the introduction of open and closed subspaces asΣ-split subspaces in the next section. Briefly, being Σ-split means that all open subsubspaces ofa subspace are restrictions of open subspaces of the ambient space, indeed in a canonical way.
Consider the left-hand Gentzen rule in terms of the open subspaces that α, β and σ classify.
The top line expresses the containment α ⇒ β of open subsubspaces of the open subspace classified
by σ. In the ambient space, this means that α ∧ σ ⇒ β ∧ σ, or, more briefly, α ∧ σ ⇒ β, as in thebottom line.
The rule on the right says exactly the same thing, but for the intersection of closed subspaces.
Translating this into a result about relatively open subsubspaces of the closed subspace, the relative
containment β ⇒ α in the closed subspace means β ∨ σ ⇒ α ∨ σ, or just β ⇒ α ∨ σ, in the whole
space.
1 Peter Aczel pointed out the resemblance to Gerhard Gentzen’s rules for negation in classical sequent calculus [Gen35].

18

Another “extensional” aspect of topology that the rules state is that, if the inverse images of> under φ, ψ : X ⇒ Σ coincide as (open) subspaces of X, then x : X ` φx ⇔ ψx (or φ = ψ) as
logical terms. The inverse images of ⊥ behave in a similar way [C, §5].
Subspaces of X 2 or X 3 are often called binary or ternary relations. In particular, open binary
relations are the same thing as predicates with two variables.
Definition 4.12 If the diagonal subspace, X ⊂ X × X, is open or closed then we call X discreteor Hausdorff respectively. Type-theoretically, such spaces are those in which we may internalise
equality-statements as predicates:Γ ` n = m:N=================Γ ` (n =N m) ⇔ >Γ ` h = k:H=================Γ ` (h 6=H k) ⇔ ⊥Lemma 4.13 Equality has the usual properties of substitution, reflexivity, symmetry and transitivity, whilst inequality or apartness obeys their lattice duals:
φm ∧ (n = m)(n = n)(n = m)(n = m) ∧ (m = k)

⇒ φn
⇔ >
⇔ (m = n)⇒ (n = k)φh ∨ (h 6= k)(h 6= h)(h 6= k)(h 6= k) ∨ (k 6= `)

⇐ φk
⇔ ⊥
⇔ (k =6 h)⇐ (h =
6 `)(The proof of this uses Axiom 4.7.) In an overt discrete space, or a compact Hausdorff one, wehave the converse of the first of the four rules:∃m. φm ∧ (n = m) ⇔ φn∀h. φh ∨ (h 6= k) ⇔ φk.

When both =X and 6=X are defined, as they are for N, they are complementary:(n =X m) ∨ (n 6=X m) ⇔ >and(n =X m) ∧ (n 6=X m) ⇔ ⊥.

In this case X is said to have decidable equality .

Definition 4.14 A space X that admits existential or universal quantification is called overt orcompact respectively. By these quantifiers we mean the type-theoretic rules
Γ, x : X ` φx ⇒ σ=================Γ ` ∃x. φx ⇒ σΓ, x : X ` σ ⇒ φx=================Γ ` σ ⇒ ∀x. φx

Axiom 4.15 The space N is overt. This and Scott continuity break the de Morgan-style lattice
duality that the other rules enjoy.
Remark 4.16 So long as the types of the variables really are overt or compact, we may reason
with the quantifiers in the usual ways:(a) If we find a particular a : X that satisfies φa, then we may of course assert ∃x. φx. This simple
step tends to pass unnoticed in the middle of an argument, in the form φa ⇒ ∃x. φx.
(b) Similarly, if the judgement ∀x. φx has been proved, and we have a particular value a : X, thenwe may deduce φa. Again, we often just write (∀x. φx) ⇒ φa.
(c) The familiar mathematical idiom “there exists”, in which ∃x. φx is asserted and then x is
temporarily used in the subsequent argument, is valid, as [Tay99, §1.6] explains.
(d) The λ-calculus formulation automatically allows substitution under the quantifiers [C, §8],
whereas in categorical logic this property must be stated separately, and is known as theBeck–Chevalley condition [Tay99, Chapter IX].
19

However, we must observe the caveats in Remarks 3.5 and 15.4:(e) Given ∃x. φx, there need only be a term a : X satisfying φa in the case where X and the types
all of the parameters in φ are overt discrete and Hausdorff.
(f) We cannot deduce ∀x. φx from proofs of φa for every closed term a : X.
Exercise 4.17 Use the Phoa principle to prove the Frobenius and modal laws
∃x. σ ∧ φx ⇔∀x. σ ∨ φx ⇔σ ∧ ∃x. φxσ ∨ ∀x. φx(∀x. φx) ∧ (∃x. ψx) ⇒(∀x. φx) ∨ (∃x. ψx) ⇐∃x. (φx ∧ ψx)∀x. (φx ∨ ψx)

where the type of x is both overt and compact. The Frobenius law for ∀ is another feature that
ASD has in common with classical but not intuitionistic logic; it was nevertheless identified in
intuitionistic locale theory by Japie Vermeulen [Ver94].
Lemma 4.18 Any topology ΣX has joins indexed by overt objects and meets indexed by compact
ones:
^
_
≡ ∀X : (ΣX )K ∼≡ ∃X : (ΣX )N ∼= (ΣK )X −→ ΣX .
= (ΣN )X −→ ΣX and
K

N

K

N

Binary meets distribute over joins by the Frobenius law, and “substitution under the quantifier”
means that all inverse image maps Σf : ΣY → ΣX , whereΣf ψ ≡ ψ · f ≡ λx. ψ(f x)orΣf V ≡ f ∗ V ≡ f −1 V ≡ {x | ψx},preserve all joins indexed by overt objects, and meets indexed by compact ones [C, §7].
Since N is overt but not compact, each Σ
N-indexed meets.

X



f

has and each Σ preserves N-indexed joins, but not

Remark 4.19 We often want the quantifiers or meets and joins to range over dependent types,
even though we have not provided these in the calculus.
The most pressing case of this is the join or existential quantifier indexed by an open subspace
M ⊂ N of an overt space. This subspace is classified by a predicate α : ΣN , which we shall writeas Γ, n : N ` αn : Σ. The M -indexed family φm : ΣX of which we want to form the join may
always be considered to be the restriction to M of an N -indexed family, so we have_φm ≡ ∃n:N . αn ∧ φn : ΣX .
m:M

This sub- and super-script notation, which is used extensively in [G], indicates co- and contravariance with respect to an imposed order relation, such as the arithmetical order in Q or inclusionof lists.
We shall also want to define both quantifiers over the closed interval [d, u], where d and u neednot be constants, but we shall cross this bridge when we come to it, in Section 10.
Definition 4.20 Such a pair of families (αn , φn ) is called a directed diagram, and the corresponding_
 φn ≡ ∃n. αn ∧ φnn:αn

is called a directed join, if (a) (∃n. αn ) ⇔ >, and (b) αn@m ⇔ αn ∧ αm and φn@m > φn ∨ φmfor some binary operation @ : N × N → N .
In this, αn ∧ αm means that both φn and φm contribute to the join, so for directedness in theinformal sense, we require some φn@m to be above them both (contravariance), and also to counttowards the join, for which αn@m must be true (covariance). Hence the imposed order relation on
N is that for which (N, @) is essentially a meet semilattice.
20

This allows us to formalise Scott continuity (Definitions 2.6 and 3.1).
Axiom 4.21 Any F : ΣΣX(possibly with parameters) preserves directed joins in the sense thatF (∃n. αn ∧ φn ) ⇐⇒ ∃n. αn ∧ F φn .

Notice that F is attached to φn and not to αn , since the join being considered is really that over thesubset M ≡ {n | αn } ⊂ N . The principal use of this axiom in this paper is Proposition 7.12, where
the ambient overt object N is Q, and its imposed order is either the arithmetic one or its reverse,so @ is either max or min. Scott continuity is also what connects our definition of compactness
with the traditional “finite open sub-cover” one (Remark 10.10), whilst in denotational semantics
it gives a meaning to recursive programs.
In locale theory [Joh82], the homomorphisms are those of finite meets and arbitrary joins.
Since we have just taken care of (some of) the directed joins, in ASD we need only consider thefinitary connectives >, ⊥, ∧ and ∨.
X

Definition 4.22 A term P of type ΣΣ is called prime if it preserves all four lattice connectives:
P> ⇔ >P⊥ ⇔ ⊥P (φ ∧ ψ) ⇔ P φ ∧ P ψ

P (φ ∨ ψ) ⇔ P φ ∨ P ψ.

The type X is said to be sober if every prime P corresponds to a unique term a : X (which wecall focus P ) such thatφ(focus P ) ⇔ P φ
or
P = λφ. φa.
Proposition 4.23 Let i : X → Y between sober objects. If the map Σi : ΣY → ΣX has aninverse I, then so does i itself [Tay91].
Y

Proof The map η : Y  ΣΣ given by y 7→ λψ. ψy is mono, because focusY (λψ. ψy) = y.
Since I is an isomorphism, both it and P ≡ λφ. Iφy preserve all four lattice operations, i.e. P
is prime. Then, as X is sober, we may define j : Y → X by jy ≡ focusX (λφ. Iφy). It satisfies
j(ix) = focusX λφ. Iφ(ix) = focusX λφ. I(Σi φ)x = focusX (λφ. φx) = xand λψ. ψ i(jy) = λψ. (Σi ψ) focusX (λφ. Iφy) = λψ. I(Σi ψ)y = λψ. ψy ≡ ηY y,Y

so i(jy) = y since η : Y  ΣΣ is mono.



For N, sobriety is equivalent to a more familiar idiom of reasoning that characterises singleton
predicates, φ = {n} ≡ (λm. n = m). This is only meaningful for (overt) discrete objects, but weshall see in Section 14 that Dedekind completeness expresses sobriety of R.
Axiom 4.24 A predicate φn for n : N (possibly involving other parameters) is called a description
if it is “uniquely satisfiable” in the sense that(∃n. φn) ⇐⇒ > and (φn ∧ φm) =⇒ (n =N m)
are provable. Then we may introduce the n. φn : N, with the same parameters, satisfying
φm ⇐⇒ (m =N the n. φn).
Descriptions may be used to define general recursion (minimalisation) [A, D, O].

21

Proposition 4.25 All types that are definable from 1, Σ and N using × and Σ(−) are sober.
Proof1(a) The only prime of type ΣΣ is P ≡ λφ. φ?, and focus1 P = ?.
N(b) If P : ΣΣ is prime then φn ≡ P (λm. n =N m) is a description, and focusN P = the n. φn[A, Proposition 10.4].
(c) If X and Y are sober then so is X × Y , withfocusX×Y P = focusX λφ. P (λp. φ(π0 p)) , focusY λψ. P (λp. ψ(π1 p)) .
(d) Any ΣX is sober, with focusΣX P ≡ λx. P(λφ. φx) [A, Lemma 8.8].



Examples 4.26 We conclude with some examples of the four main topological properties.
overt
discretecompact Hausdorff
N×Σ
X
×
×
×
R, Rn
X
×
×
X
Σ
X
×
X
×
I, 2N
X
×
X
X
free combinatory algebra
X
X
×
×
X
X
×
X
N, Q
Kuratowski finite
X
X
X
×finite (n)XXXX
the set of codes of
non-terminating programs
×
X
×
X
The axioms only provide the quantifiers ∀∅ ≡ >, ∃∅ ≡ ⊥, ∀2 ≡ ∧, ∃2 ≡ ∨ and ∃N directly —it is the business of this paper to construct ∃R , ∃I and ∀I , in Sections 9 and 10. To put this theother way round, assuming that a future extension of the calculus will allow arbitrary nesting of⇒ and ∀ in statements (cf. Remark 4.6), these constructions will justify quantifier eliminationin the corresponding cases.
The calculus as we have described it so far will be used to define individual Dedekind cuts in
Section 6.

5

The monadic principle

We have seen how some of the ideas of topology can be expressed using the types and terms ofa λ-calculus. In particular, compactness of a space K is expressed as a “universal quantifier”∀K : ΣK → Σ. The main application of this idea will be to the closed interval K ≡ [d, u] ⊂ R ⊂ΣQ × ΣQ ≡ Y , where we shall construct R as the subspace of those pairs of predicates on Q thatare Dedekind cuts (Remark 2.1).
How could we obtain a map ΣK → Σ from one i : K  Y ? We have ΣY → Σ by evaluation
at some y : Y (Lemma 5.12), but nothing ΣK → ΣY , since the maps go the wrong way. However,given that we have already introduced higher types, it hardly seems to be a revolutionary step tointroduce extra terms of those types. Indeed, in our brief account of interval analysis in Section 2,
we have already discussed such a map, I : ΣK → ΣY . It extends open sets and functions fromthe real line to the interval domain, and it is intimately related to the quantifiers ∀ and ∃, indeed
these are special cases of it.
In this section we shall give the type-theoretic rules that formally introduce i and I for (certain)
subspaces, at least the ones that we need. This will complete our manual of the axioms of ASD.

22

The basis of our proof of the Heine–Borel theorem is that the rules force these subspaces to carry
the subspace topology. Naturally, we shall use terms of higher type (such as I) to do this, justas we have already introduced terms of lower type and equations between them in the previous
section.
Definition 5.1 An inclusion i : X  Y is called a Σ-split subspace if there is another map
I : ΣX  ΣY such that
Σi · I = idΣXorx : X, φ : ΣX ` Iφ(ix) ⇔ φx,

thereby making ΣX a retract of ΣY with inclusion I and projection Σi . The convention in the
λ-calculus is that Iφ(ix) means (Iφ)(ix).
Remark 5.2 Whenever two maps compose to the identity one way round like this, they may berecovered (uniquely up to unique isomorphism) from their composite the other way, which is an
idempotent (E = E · E). In this case, E ≡ I · Σi : ΣY → ΣY determines ΣX . (We wrote E for E
in Proposition 2.15 in accordance with our convention of using fancier typefaces for fancier types.)
The object X itself is the equaliserX-

i Y

y 7→ λψ. ψy ΣY- Σ .
y 7→ λψ. Eψy

The idea is that the operator E “normalises” open subspaces of Y by restricting them to X using
Σi , and then re-expanding them using I. Therefore a : Y belongs to {Y | E} iff its membershipof any open subspace ψ of Y is unaffected by this process.
Definition 5.3 Recall that being the equaliser means that(a) the inclusion i has equal composites with the parallel pair: it sends each x : X to y ≡ ix : Y
satisfying the equation (ψy ⇔ Eψy for all ψ : ΣY );(b) whenever we have another map b : Γ → Y (which is the same as a term b : Y with parametersfrom Γ) that has equal composites with the parallel pair (i.e. which satisfies the equationψb ⇔ Eψb for all ψ), then we may introduce a map a : Γ → X (term Γ ` a : X) that makes
the triangles commute, so b = ia, and this is unique.
Not every idempotent E on ΣY can arise in this way from a Σ-split subspace, because thesurjective part Σi of its splitting must be a homomorphism for the topological structure. In particular, it must preserve the four lattice connectives, but any order-preserving surjective function
between lattices preserves > and ⊥ anyway. So the crucial condition is this:Lemma 5.4 E ≡ I · Σi : ΣY → ΣY satisfies the equations, for φ, ψ : ΣY ,E(φ ∧ ψ) = E(Eφ ∧ Eψ)andE(φ ∨ ψ) = E(Eφ ∨ Eψ).



Definition 5.5 A term E that satisfies the equations in the Lemma is called a nucleus. In order
to avoid developing a theory of dependent types, we do not allow E to have parameters.
The word “nucleus” was appropriated from locale theory, since both kinds of nuclei play thesame role, namely to define subspaces, but the definitions are different. A localic nucleus, usuallycalled j, must satisfy id 6 j = j · j but need not be Scott-continuous [Joh82, §II 2]. Nuclei in ASD,
on the other hand, are continuous but need not be order-related to id. So the common ground is23

when E > id and j is continuous: ASD and locale theory therefore agree on how to form closed
subspaces, but not open ones or retracts.
In Section 8 we shall use E to define R as a subspace of the interval domain IR, and in thiscase E is a nucleus in both senses. If we view R instead as a subspace of ΣQ × ΣQ , but still definedby E, this is a nucleus only in the sense of ASD, not that of locale theory.
Notation 5.6 We write {Y | E} for the subspace X ⊂ Y that is defined by any nucleus E on Y .
Beware, however, that this has very few of the properties of subset-formation in set theory.
Definition 5.7 A term a : Y (which may now involve parameters from a context Γ) of the larger
space Y is called admissible with respect to the nucleus E ifΓ, ψ : ΣY ` ψa ⇔ Eψa.
This is the same as saying that the map a : Γ → Y has equal composites with the parallel pair inthe diagram in Remark 5.2, so it factors through the equaliser.
Since this equaliser is the subtype X ⊂ Y , we may then regard a as a term of type X or
{Y | E}. However, when we need to discuss the calculus in a formal way, we shall write admitY,E a
for it, in order to disambiguate its type.
Remark 5.8 The simplest (and first, [C, §3]) application of this calculus is to the construction ofopen and closed subspaces. This will formalise Remark 4.11.
Let θ : ΣY be a closed term (i.e. without parameters), which we think of as a continuousfunction θ : Y → Σ. The open and closed subspaces that θ (co)classifies are the inverse images
U ≡ θ−1 (>) and C ≡ θ−1 (⊥) of the two points of the Sierpiński space (Remark 3.2).
Classically, any open subspace of U is already one of Y , whilst an open subspace of C becomes
open in Y when we add U to it. This means thatΣU ∼= ΣY ↓ θ ≡ {ψ | ψ 6 θ}and ΣC ∼= θ ↓ ΣY ≡ {ψ | ψ > θ},i.e. the parts of the lattice ΣY that lie respectively below and above θ. (The ↓ notation is used in
category theory for “slice” or “comma” categories.)
From this we see what the Σ-splittings and nuclei for U and C must be. The construction of
the interval domain IR ⊂ ΣQ × ΣQ in Section 7 will involve an open subspace, a closed one and aretract.
Lemma 5.9 Let e : Y → Y be an idempotent and θ : Y → Σ any map. ThenΣe ,

θ ∧ (−)θ ∨ (−)

andare nuclei on Y , with respect to which a : Y is admissible iff respectively
ea = a,θa ⇔ >andθa ⇔ ⊥.



Notation 5.10 As we shall need to name the Σ-splittings of j : U, C  Y , we write∃j : ΣU  ΣY

and∀j : ΣC  ΣY ,where ∃j (Σj ψ) = ψ ∧ θ and ∀j (Σj ψ) = ψ ∨ θ. See [C] for the reasons for these names.
In Sections 7 and 8 we shall need to combine several nuclei. However, the intersection of two
Σ-split subspaces need not exist, in general, and even if it does, it need not be Σ-split. Everything24

works if the nuclei commute, but this does not often happen. In fact, there are many situations
in which E1 · E2 · E1 = E1 · E2 , and that is sufficient to justify forming the intersection.
Lemma 5.11 Let E1 and E2 be nuclei on a type Y such that either E1 · E2 = E2 · E1 or
E1 · E2 · E1 = E1 · E2 . Then E1 · E2 is also a nucleus, and defines the intersection (pullback){Y | E1 · E2 }- - {Y | E1 }?
?

?
{Y | E2 }-?
- Y

in which all five inclusions (including the composite) are Σ-split. Regarding {Y | E1 } ⊂ Y as thesubset of admissible elements, and Σ{Y |E1 } as the subset {ψ : ΣY | E1 ψ = ψ}, we see E1 · E2 as anucleus on {Y | E1 } but not necessarily on {Y | E2 }.

We have already said that nuclei and Σ-splittings are intimately related to the quantifiers thatdefine compactness and overtness. The following two lemmas will provide the key to defining ∃and ∀ from I in Section 10. There we shall use the slices ΣQ ×ΣQ ↓ (δu , υd ) and (δd , υu ) ↓ ΣQ ×ΣQ ,which we shall call lattices in this very specific context.
Lemma 5.12 Any lattice L is overt and compact, with ∃Φ ≡ Φ(>) and ∀Φ ≡ Φ(⊥).
Proof By monotonicity, Φ(⊥) ⇒ Φ(x) ⇒ Φ(>) for any x : L.



Lemma 5.13 Let i : X  L and I : ΣX  ΣL with Σi · I = id. Then2(a) if I preserves ⊥ and L is overt then so is X, with ∃x:X . φx ≡ ∃y:L. Iφy, whilst(b) if I preserves > and L is compact then so is X, with ∀x:X . φx ≡ ∀y:L. Iφy.
Proof In each column we deduce in both directions,Γ, x : X`Γ, σ ⇔ ⊥ `Γ, σ ⇔ ⊥ `Γ, σ ⇔ ⊥ `Γ
`φx ⇒ σΣi (Iφ) ≡ φ = ⊥ : ΣX
Iφ = ⊥ : ΣL
∃L (Iφ) ⇒ ⊥∃L (Iφ) ⇒ σ

Γ, x : X` σ ⇒ φxΓ, σ ⇔ > ` > = φ ≡ Σi (Iφ) : ΣXΓ, σ ⇔ > ` > = Iφ : ΣLΓ, σ ⇔ > ` > ⇒ ∀L (Iφ)Γ` σ ⇒ ∀L (Iφ)

using Axiom 4.7 and Definition 4.14.



It is high time we gave the actual rules that define subtypes and their admissible terms. These
formally adjoin Σ-split subspaces to the calculus just as number theorists formally adjoin rootsof particular polynomials to a field, or set theorists construct “equiconsistent” models that havealtered properties. Theorem 15.8 describes the corresponding categorical construction.
As in type theory, we name the rules after the connective that they introduce or eliminate.
Our connectives are called {} and Σ{} .
Axiom 5.14 The {}-rules of the monadic λ-calculus define the subspace itself:
Y typey : Y, ψ : ΣY ` Eψy : Σ{Y | E} type2 This result was suggested by Alex Simpson.

25

E is a nucleus{}FΓ, ψ : ΣY ` ψa ⇔ Eψa

Γ ` a:YΓ ` admitY,E a : {Y | E}{}I

x : {Y | E} ` iY,E x : Y{}E0

x : {Y | E}, ψ : ΣY ` ψ(iY,E x) ⇔ Eψ(iY,E x){}E1Γ, ψ : ΣY ` ψa ⇔ Eψa

Γ ` a:YΓ ` a = iY,E (admitY,E a) : Y
x : X ≡ {Y | E} ` x = admitY,E (iY,E x) : {Y | E}.

{}β
{}η

These rules say that {Y | E} is the equaliser in Remark 5.2.
Axiom 5.15 The following Σ{} -rules say that {Y | E} has the subspace topology, where IY,E
expands open subsets of the subspace to the whole space.
φ : Σ{Y |E} ` IY,E φ : ΣY .

Σ{} E

The Σ{} I rule is derived from {}E0 :ψ : ΣY ` Σi ψ ≡ λx:{Y | E}. ψ(iY,E x) : Σ{Y |E} .
Σi- Σ{Y |E}- I- ΣY is E:
` IY,E λx:{Y | E}. ψ(iY,E x) y ⇔ Eψy.

The β-rule says that the composite ΣYy : Y, ψ : ΣY

Σ{} IThe η-rule says that the other composite Σ{Y |E}- - ΣY

Σ{} β- Σ{Y |E} is the identity:

φ : Σ{Y |E} , x : {Y | E} ` φx ⇔ IY,E φ(iY,E x).

Σ{} ηThis equation is the one in Definition 5.1 for a Σ-split subspace.
Remark 5.16 Notice that the Σ{} β-rule is the only one that introduces E into terms. This issomething that we want to avoid if at all possible, given that the expressions for nuclei, such as E,
which we intend to use to construct R, are usually very complicated. The normalisation theorem
that eliminates unnecessary Es is proved in [B, §§9-10].
When E does find its way into a program, it will give rise to a substantial computation. But thisis what we would expect, considering the relationship to the quantifiers, and their computational
meaning as optimisation and search (Section 2).
Warning 5.17 It is important to understand that, for another structure to admit a valid interpretation of this calculus, not only must the equaliser in Remark 5.2 exist, but there must also be
a map I in the structure that satisfies the equations Σi · I = idΣX and I · Σi = E, cf. Remark 2.18.
Proposition 5.18
(a) If Y is sober then so is {Y | E}, with focus{Y |E} Q = admitY,E focusY (Σ2 iY,E Q) .
(b) If X is also sober and has maps f : X → Y and F : ΣX → ΣY with Σf · F = idΣX andF · Σf = E then X ∼= {Y | E}, wherex:X`

x0 ≡ admitY,E (f x) : {Y | E}

x0 : {Y | E}`x ≡ focusX λφ:ΣX . F φ(ix0 ) : X.
26

In particular, f is the equaliser in Remark 5.2.



Remark 5.19 If this paper is the first one about ASD that you have seen, you may reasonably
imagine that we have cooked up the rules from the observations in Section 2, based on little
more than the properties of the real line that first year undergraduates learn. Can this theory of
topology even be generalised to Rn ? Is it of any use in proving theorems in mathematics otherthan those that we have mentioned?
Actually, we have told the story so far in reverse historical order. The calculus above wasderived from a categorical intuition, and when it was formulated [B], it was a solution in searchof a problem. There were no clear ideas of how the real line might be constructed, and certainly
no inkling that it might behave in ASD in a radically different way from the established theory of
Recursive Analysis (Section 15). That it turned out to do so is a tribute to category theory as asource of, or rather as a way of communicating, mathematical intuitions.
For reference we give a summary of some of the constructions that have been performed using
nuclei in the infrastructure of ASD.
Theorem 5.20 Σ-split subspaces interact with the underlying structure of products and exponentials as follows, and also provide stable disjoint unions [B, §11].
X{X | E0 } × {Y | E1 }
Σ{X|E}{{X | E1 } | E2 }{X | E0 } + {Y | E1 }
where

EHH


X
∼
= {ΣΣ | λFF . F λx. F(λφ. φx) }∼= {X × Y | E1X · E0Y }∼= {ΣX | ΣE }∼= {X | E2 }X
Y∼
= {ΣΣ ×Σ | E}
≡ H λx. H(λφψ. E0 φx), λy. H(λφψ. E1 ψy) .

In Section 8, we shall need to perform some combinatorial arguments using lists of rational
numbers. However, since ASD is a direct axiomatisation of topology, without using set theory, we
have to recover some kind of “naı̈ve set theory” within our category of spaces. Our “sets” are theovert discrete objects.
Theorem 5.21 The full subcategory consisting of the overt discrete objects has(a) finite products (1 and ×);(b) equalisers;(c) stable disjoint coproducts (0 and +);(d) stable effective quotients of open equivalence relations [C]; and(e) free monoids or “sets of lists”, List(X) [E].
This categorical structure is called an arithmetic universe.



Remark 5.22 We shall rely on this result to provide the “discrete mathematics” that we need,
namely(a) the usual arithmetic operations on N, Z and Q;(b) the operations of naı̈ve set theory over these types, including, for example, the use of lists and(Kuratowski-) finite sets; and(c) both quantifiers over finite sets, i.e. finite conjunctions and disjunctions, which have wellknown definitions using primitive recursion.

27

The infinite objects that are generated in this way are countable in the strict sense of being
bijective with a decidable subset of N in the calculus; since our isomorphisms are homeomorphisms,
such objects inherit =, ∃, and in some cases 6=, from N.
These “sets” do not admit a full powerset on the basis of the axioms that we have given here,
and therefore they do not form an elementary topos or model of set theory. However, it is possible
to add another (much more powerful, and certainly non-computational) axiom to ASD that does
make the full subcategory of overt discrete objects into a topos. This axiom asserts that thissubcategory is co-reflective, i.e. that the inclusion has a right adjoint, which formally assigns anovert discrete object to any space, and we call this object the “underlying set” of the space [H].
We do not use this axiom in this paper.
Remark 5.23 In order to formulate the definition of Σ-split subspace we only need powers Σ(−) ,not the lattice structure on Σ or the quantifiers. The category-theoretic summary of this sectionis that we require the adjunction Σ(−) a Σ(−) to be monadic.
The notions of sobriety and Σ-split subspaces in ASD come from the two conditions in thetheorem of Jon Beck (1966) that characterise monadic adjunctions [Tay99, Theorem 7.5.9]. Sobriety says that Σ(−) reflects invertibility (Proposition 4.23). Nuclei are essentially the same asΣ(−) -contractible equalisers; Axiom 5.14 says that such equalisers exist, and Axiom 5.15 that Σ(−)
takes them to coequalisers. These conditions are given as equations between higher-order λ-termsin [A, B].
In the presence of the other topological structure in the previous section, in particular Scottcontinuity, the equations that define a nucleus are equivalent to the much simpler ones involving
finitary ∧ and ∨ that we gave in Lemma 5.4 and Definition 4.22 [G, §10]. In this setting, any
definable object X of ASD can be expressed as a Σ-split subspace, i : X  ΣN , where i and I
correspond directly to a basis of open subspaces and related compact subspaces. Locally compact
spaces and computably continuous functions between them can then be understood directly in
ASD [G]. This calculus is how we implement the foundations of recursive analysis and topology
based on open sets instead of points.
However, the introduction of nuclei with this definition after the lattice theory in the previous
section is the reason why our discussion of open and closed subspaces and the Phoa principle
in Remark 4.11 was deductively unsatisfactory. From a foundational point of view, the monadic
structure should really come first. Then the Euclidean principle (σ ∧ F σ ⇔ σ ∧ F >), which isthe part of the Phoa principle that applies to intuitionistic set theory or the subobject classifierin an elementary topos, is exactly what is required to make Eφ ≡ φ ∧ θ a nucleus in the abstract
sense, or equivalently to justify the first of the two Gentzen-style rules. This is essentially how
this principle was discovered [C, §3].
The results that we have sketched here are treated in greater detail in the earlier papers thatdeveloped ASD. The foundations of the theory, together with the methodology and motivations
behind it, are surveyed in [O].

6

Dedekind cuts

We now return to Richard Dedekind’s construction of the real line, which we introduced in Section 2. Whilst this is very familiar, we need to be sure that it can be carried out in our very weak
logic. We begin with what we require of the rationals for the purposes of topology, postponing
arithmetic to Sections 11–13. Both the ingredients (Q) and the result (R) of the construction
satisfy the first definition, but we shall use combinatorial operations on the rationals which will
rely on decidable equality (Remark 6.15).

28

Definition 6.1 A dense linear order without endpoints is an overt Hausdorff object Q(Definitions 4.12 and 4.14) with an open binary relation < that is, for p, q, r : Q,(a) transitive and interpolative (dense):(p < r)(b) extrapolative (without endpoints): (∃p. p < q)(c) linear (total or trichotomous):(p 6= q)⇐⇒⇐⇒⇐⇒(∃q. p < q < r)> ⇐⇒ (∃r. q < r)
(p < q) ∨ (q < p).

The ∃q in the interpolation axiom does not necessarily mean the midpoint 21 (p + r). It mightinstead mean the “simplest” interpolant, in some sense, as in John Conway’s number system[Con76]. In practical computation, the best choice of q may be determined by considerations
elsewhere in the problem, cf. unification in Prolog (Remark 3.4).
Lemma 6.2
(p < q) ∧ (s < t)=⇒(p < t) ∨ (s < q)

(p < q) ∧ (q < r)=⇒

(p < r) =⇒ (p < q) ∨ (q < r)Lemma 6.3 If Q is discrete then = and < are decidable, with (p ≮ q) ≡ (p = q) ∨ (q < p). Thisis the case when Q is countable (by which we mean strictly that Q ∼= N, Remark 5.22), in whichcase the usual order on N induces another (well founded) order ≺ on Q that we call simplicity . 
Examples 6.4 Such countable Q may consist of(a) all fractions n/m with m 6= 0, where “simpler” fractions have smaller denominators;(b) dyadic or decimal fractions k/2n and k/10n ;(c) finite continued fraction expansions; or(d) roots of polynomials with integer coefficients, where the notion of simplicity is given by the
degree and coefficients of the polynomials;
where in all cases < is the arithmetical order. For the sake of motivation and of having a name forthem, we shall refer to the elements of any such countable Q as rationals, but for a particulartarget computation any of the above structures may be chosen. We keep the dyadic rationals inmind for practical reasons, but they have no preferred role in the definition.
Proposition 6.5 Any two countable dense linear orders without endpoints are order-isomorphic.
Proof The isomorphism Q1 ∼= Q2 is built up from finite lists of pairs (Theorem 5.21) by courseof-values recursion and definition by description (Axiom 4.24). Given such a list, we may add
another pair that consists of the simplest absentee from Q1 , together with its simplest ordermatch from Q2 . At the next stage, we start with an absentee from Q2 .

Remark 6.6 Of course, this well known model-theoretic result misses the point of real analysis.
When we apply it to different notions of “rationals”, it destroys the arithmetic operations and theArchimedean property (Axiom 11.2). In Definition 13.1 we shall show how order automorphisms(strictly monotone functions) of R arise from relations rather than functions on Q.
Remark 6.7 There are many formulations of Dedekind cuts. We choose a two-sided version thatappears as Exercise 5.3.3 in [TvD88], but we don’t know who originally formulated it. That book,like many other accounts, uses a one-sided version in its main development.
As in the case of open and closed subspaces (Remark 3.2f), the relationship between the twosides of the cut is contravariant. One-sided accounts obtain one from the other by means of(Heyting) negation — with some awkwardness, since arithmetic negation ought to be involutive,
whereas logical negation is not, in intuitionistic logic.
29

The ASD calculus does not allow negation of predicates. Nor, indeed, is there any kind ofcontravariant operation, as it would be neither continuous nor computable. So we have to use
both halves of the cut. But this is not just to overcome a technical handicap of our weak logic:
like open and closed subspaces, the two parts play complementary roles that are plainly of equal
importance. We also saw in Section 2 that it is natural to generalise Dedekind cuts by not forcing
the halves to be complementary, the resulting space being the interval domain.
Definition 6.8 Formalising Remark 2.1, a (Dedekind ) cut (δ, υ) in a (not necessarily discrete)dense linear order without endpoints (Q, <) is a pair of predicatesfor d, u : Q,δd, υu : Σ,possibly involving parameters, such thatυuδd⇔ ∃t:Q. υt ∧ (t < u)⇔ ∃e:Q. (d < e) ∧ δe

>
>

⇔
⇔

⊥
⇔
(d < u) ⇒∃u:Q. υu∃d:Q. δdδd ∧ (u < d) ∧ υu(δd ∨ υu)

υ rounded upperδ rounded lower
bounded above
bounded below
disjoint
order-locatedWe call δ or υ rounded if they satisfy the first or second of the above properties, these being
the most important. Their types are the ascending and descending reals (R, R, Example 2.8 andDefinition 7.3). Lemma 7.5 explains why we have defined disjointness in this way, in preference toseveral others, and we shall discuss a stronger notion of locatedness that is needed for arithmeticin Proposition 11.15. When (δ, υ) are rounded, bounded and disjoint, they represent an interval(Definitions 2.3 and 7.8). We construct the space IR of intervals in the next section, on the way
to the construction of R itself.
We do not introduce the “set” of cuts. However, we reformulate this definition using alittle category theory to provide the context in which to understand both our construction in ASD
and the alternatives in other foundational settings in Section 15.
Remark 6.9 The six axioms above are (essentially) equations (cf. Axiom 4.5). The boundedness
axioms are already equations between terms of type Σ, whilst the roundedness and disjointness
conditions become equations of type ΣQ and ΣQ×Q when we λ-abstract the variables. Finally,
locatedness may be rewritten as
λdu. δd ∨ υu ∨ (d < u) = λdu. δd ∨ υu of type ΣQ×Q .
We therefore expect R to be the subspace of ΣQ × ΣQ of those pairs (δ, υ) that satisfy these six
equations. In the language of category theory, this is the equaliser (Definition 5.3) of the parallel
pair of arrows that collects them together:
Q

j -

i
R- - ΣQ × ΣQ
..
..6
a ...
..
(δ, υ)
Γ

LHS Q
Q
Q×Q
× ΣQ×Q- Σ ×Σ ×Σ×Σ×Σ
RHS

We shall explain how to construct this equaliser in ASD, i.e. to define the new type R of
Dedekind cuts, in the next two sections. For the remainder of this one, Definition 6.8 is merely alist of properties that a pair of predicates on Q may or may not have.
30Real numbers admit two order relations, which we shall now define in terms of cuts. Recall
from Remark 4.6(b) that we expect a < b to be a predicate (a term of type Σ) but a ≤ b to be astatement (an equation between such terms).
Definition 6.10 The irreflexive (strict) order relation on cuts is the predicate(δ, υ) < (, τ ) ≡ ∃q. υq ∧ q.
The idea is that the right part of the smaller cut overlaps the left part of the larger.
Lemma 6.11 The relation < is transitive.
Proof
δ

υ
q



τ
r

α

σ



Lemma 6.12 As in Remark 2.1, each q : Q gives rise to a cut jq ≡ (δq , υq ) withδq ≡ λd. (d < q)andυq ≡ λu. (q < u).

Beware that q is a sub-script! This is an order embedding, in the sense that(q < s) ⇔ (∃r. q < r < s) ⇔ (∃r. υq r ∧ δs r) ≡(δq , υq ) < (δs , υs ) .

The map j makes Q an example of the test object Γ in the equaliser diagram above. Then the
map Q → ΣQ × ΣQ by q 7→ (δq , υq ) is mono (1–1), as is j : Q → R.
When we compare a real number (i.e. a cut) with a rational, we recover the lower or upper
part of the cut:
Lemma 6.13

(δd , υd ) < (δ, υ) ⇐⇒ δdand (δ, υ) < (δu , υu ) ⇐⇒ υu.



We would like to show next that < is interpolative and extrapolative, but even to say that weneed ∃R , for which we have to define R itself as a type in ASD, so we leave this until Section 9.
Now we consider the reflexive (non-strict) order ≤. This is given by implication or inclusion
between the cuts considered as predicates or subsets.
Proposition 6.14 Let (δ, υ) and (, τ ) be cuts, possibly involving parameters. Then the threestatementsδ >  : ΣQ ,
υ 6 τ : ΣQ
and(δ, υ) < (, τ ) ⇔ ⊥are equivalent. We write (, τ ) ≤ (δ, υ) for any of them. Notice that the arithmetical order ≤agrees with the logical one 6 for the ascending reals δ and , but is the reverse for the descending
reals τ and υ, cf. Example 2.8.
Proof Since (δ, υ) < (, τ ) is ∃q. υq ∧ q, it is ⊥ if either  6 δ or υ 6 τ , since cuts are rounded
and disjoint.
Conversely, by the definition of ∃, another way of writing the statement with < isfor any
Then, for p : Q,p(υq ∧ q) ⇒ ⊥q : Q,⇔ ∃q. (p < q) ∧ q
⇒ ∃q. (δp ∨ υq) ∧ q

 is rounded(δ, υ) located⇔∃q. (δp ∧ q) ∨ (υq ∧ q)

distributivity⇒∃q. (δp ∨ ⊥) ≡ δpand similarly υp ⇒ τ p.

hypothesis,31

There is one more order-theoretic property that we shall need: it develops the notion of orderlocatedness a little towards arithmetic, for which the stronger definition will be needed. The factthat this Lemma does not require disjointness, and so also applies to the back-to-front intervals
in Remark 2.20, will become relevant when we study the existential quantifier.
Remark 6.15 We present this proof in the usual informal style, in which “· · ·” indicates thevariable length of the list, but the formal proof, of course, uses list induction. In particular, theordering of the list is an open predicate that, like the n-fold conjunction, is easily definable byrecursion on lists. This means that we rely on the methods of “discrete mathematics” that were
outlined in and following Theorem 5.21, but these only work for overt discrete spaces. On theother hand, for Definition 6.1 it had to be Hausdorff, so equality on Q must be decidable,
cf. Lemmas 4.13 and 6.3.
Lemma 6.16 Let q0 < q1 < · · · < qn be a strictly ascending finite sequence of rationals, and let(δ, υ) be rounded, located and bounded, with δq0 and υqn . Then this (pseudo-)cut belongs to atleast one of the overlapping open intervals(q0 , q2 ),in the sense that

(q1 , q3 ),
n−2
_

...,

(qn−2 , qn ),(δqj ∧ υqj+2 ).

j=0

Proof
give

The hypotheses δq0 and υqn and order-locatedness of (δ, υ) applied to each pair qj < qj+1
δq0 ∧ (δq0 ∨ υq1 ) ∧ (δq1 ∨ υq2 ) ∧ · · · ∧ (δqn−1 ∨ υqn ) ∧ υqn ,which we expand using distributivity. Of the 2n disjuncts, n + 1 yield those in the claim, including
two repetitions:δq0 ∧ υq1 ∧ υq2 ∧ · · · ∧ υqn⇒

δq0 ∧ υq2

δq0 ∧ · · · ∧ δqj ∧ υqj+2 ∧ · · · ∧ υqn⇒

δqj ∧ υqj+2

δq0 ∧ · · · ∧ δqn−2 ∧ δqn−1 ∧ υqn⇒

δqn−2 ∧ υqn .

Each of the remaining 2n − n − 1 disjuncts consists of a conjunction of δs up to some δqj and of
υs starting from υqi , with 1 ≤ i ≤ j + 1 ≤ n. Such a conjunction vanishes if δ and υ are disjoint.
But even if they are not, since υ is upper we have
δqj ∧ υqi =⇒ δqj ∧ υqj+2 ,which is one of the disjuncts in the claim.



Exercise 6.17 Formulate the following in accordance with Remark 4.6, and prove them:(a) if a ≤ b < c ≤ d then a < d;(b) if a < b or a = b then a ≤ b;(c) if a ≤ b and a 6= b then a < b;(d) if δd then (d < u) ∨ δu;(e) if (d < u) ∨ δu for all u then δd [NB: ∀u : Q is not allowed];(f) not all d : Q satisfy δd.
Finally, verify that the results about < and ≤ make no use of the boundedness axiom for cuts,and therefore also apply to +∞ ≡ (>, ⊥) and −∞ ≡ (⊥, >).

32

7

The interval domain in ASD

You might reasonably expect that our next task would be to construct R as an object of ASD.
This would involve showing that the formula E in Section 2 satisfies the definition of a nucleus in
Section 5, and that its admissible terms are exactly the Dedekind cuts of Section 6.
However, hard experience with nuclei has shown that one cannot go at them like a bull in achina shop: whilst the calculations are elementary, they are very tricky. In fact, it is precisely
because we want to give an elementary proof (in the technical sense of the word, i.e. in a very
weak logic) that it is difficult. If we were willing to assume all of the structure of set theory,
Proposition 2.17 for R would already have justified the equations in Lemma 5.4. The elementary
proof requires messy manipulation of sequences of rationals.
Sorting out the mess teaches us two things conceptually.
One is that we need to construct the ascending and descending reals and the interval domain
first. The other is that the Euclidean nucleus E turns out to be a composite of four parts that are
examples of the easy ways of defining nuclei in ASD, namely idempotents, open subspaces, closed
subspaces and Scott-continuous localic nuclei (Definition 5.5 and Lemma 5.9). As we shall also
see with arithmetic, the interval domain collects the “easy” properties of real numbers, clearing
the ground for work on the difficult property of locatedness.
The technical difficulties that we resolve in this section may seem to be of our own making, as
we have allowed δ, υ : ΣQ to be arbitrary λ-terms of this type. These terms may, for example, pickout individual rationals for “special” treatment, in the way that we find in the pathological counterexamples of real analysis but not its fundamental intuitions. As we explained in Remark 2.13,
we start from ΣQ because that is as close to computation as is reasonable, whereas the other structures are partial compromises with mathematics. (The order and arithmetic on Q are complicatedwhen encoded via the bijection Q ∼= N, but are well known to lie within a weak fragment of logic
like ASD.) Also, the types in ASD must be defined progressively from 1 and N using ×, Σ(−) andΣ-split subspaces, so we have to use ΣQ (∼= ΣN ) on the way to constructing the interval domain
and finally R.
We dispose of most of the arbitrariness by constructing the spaces of ascending and descending
reals (Example 2.8) as retracts of ΣQ .
Q

Q

Notation 7.1 For arbitrary δ, υ : ΣQ and Φ : ΣΣ ×Σ , defineδ̂d ≡ ∃e. (d < e) ∧ δe,
B(δ, υ) ≡ ∃du. δd ∧ υu,andυ̌u ≡ ∃t. υt ∧ (t < u),∇(δ, υ) ≡ ∃du. δd ∧ (u < d) ∧ υu

E1 Φ(δ, υ) ≡ ∃d < u. δ̂d ∧ υ̌u ∧ Φ(δd , υu ).

As the name “roundedness” suggests, δ̂ and υ̌ trim off the endpoints of cuts of the kind that
Dedekind originally introduced, cf. Remark 2.1, as well as closing the subsets down- or upwards.
The predicates B and ∇ capture boundedness and (non-)disjointness respectively (note the u < din ∇!). We shall find three nuclei that define the interval domain, but E1 will turn out to be themost useful one.
Lemma 7.2 These operations δ 7→ δ̂ and υ 7→ υ̌ are idempotent. They fix δ and υ iff these arerounded (Definition 6.8). In particular, δd , > and ⊥ are fixed by the first operation (rounding
downwards), whilst υu , > and ⊥ are fixed by the second (upwards).
Definition 7.3 Using Lemma 5.9, these idempotents on ΣQ define types
b : R / ΣQ−and −̌ : R / ΣQ ,33

called the ascending and descending reals respectively. The product R × R is similarly aretract of ΣQ × ΣQ , so it is given by the nucleus
Er Φ(δ, υ) ≡ Φ(δ̂, υ̌) ≡ Φ(λd. ∃e. d < e ∧ δe, λu. ∃t. υt ∧ t < u).
We may think of the lattice R × R as the space of “intervals” that may be infinite and evenback-to-front (Remark 2.20).
Lemma 6.12 defines “inclusion” maps δ(−) : Q → R / ΣQ and υ(−) : Q → R / ΣQ . These canbe extended to R → R and R → R, of course simply as the projections that extract δ and υ fromthe cut (δ, υ) : R. However, by monotonicity (Axiom 4.8), there is no map
R → R,

R → R,

R→R

or

R→R

that commutes with these inclusions. This is why both δ and υ are needed in the definition of
Dedekind cuts.
Exercise 7.4 Construct the ascending natural numbers, with ∞ as top, in a similar way.
Next we consider disjointness. Of the three possible definitions, in Definition 6.8 we chose theone that is invariant under rounding, so that the nuclei commute, cf. Lemma 5.11.
Lemma 7.5 Let δ, υ : ΣQ . Then ∇(δ, υ) ⇔ ∇(δ̂, υ̌) and E1 ∇(δ, υ) ⇔ ⊥.
Also, the statements (a,d,e,f) below are equivalent:∇(δ, υ) ⇔ ⊥δd ∧ υu ⇒ d < uδq ∧ υq ⇔ ⊥

(a)
(b)
(c)

(d)
(e)
(f)

∇(δ̂, υ̌) ⇔ ⊥δ̂d ∧ υ̌u ⇒ d < uδ̂q ∧ υ̌q ⇔ ⊥However, if Q is discrete then δ ≡ λd. (d ≤ r) and υ ≡ λu. (r ≤ u) satisfy (a,d,e,f) but not (b,c);
in fact (b) is equivalent to (a&c).
Proof∇(δ̂, υ̌)≡ ∃detu. δe ∧ (t < u < d < e) ∧ υt
E1 ∇(δ, υ)⇔∃et. δe ∧ (t < e) ∧ υt ≡ ∇(δ, υ)≡∃d < u. δ̂d ∧ υ̌u ∧ ∇(δd , υu )≡∃d < u. δ̂d ∧ υ̌u ∧ ∃et. δd e ∧ (t < e) ∧ υu t⇒

∃detu. d < u < t < e < d ⇒ ⊥.



Definition 7.6 The unbounded interval domain is the closed subspace IR∞ ⊂ R × R that is
co-classified by ∇, so it consists of those (δ, υ) for which ∇(δ, υ) is false (Remark 4.11), i.e. which
are rounded and disjoint. Using Lemma 5.9, IR∞ ⊂ ΣQ × ΣQ is defined by the nucleus
Erd Φ(δ, υ) ≡ ∇(δ̂, υ̌) ∨ Φ(δ̂, υ̌).
∞The inclusion map IR → R × R provides the endpoints of any interval, but as ascending anddescending reals: there is no such map IR∞ → R × R (cf. Remark 2.9). On the other hand,
there is of course a function from {(d, u) | d ≤ u} / R × R to IR∞ that provides the interval withspecified endpoints.
That version of the interval domain included (⊥, υu ) ≡ [−∞, u], (δd , ⊥) ≡ [d, +∞] and (⊥, ⊥) ≡[−∞, +∞]. The following construction, on the other hand, eliminates them; since it therefore has
no least element, it is called a predomain. It is again invariant under rounding.
Lemma 7.7∇(δ, υ) =⇒ B(δ, υ) ⇐⇒ B(δ̂, υ̌) ⇐⇒ E1 >(δ, υ).
34

ProofB(δ̂, υ̌)≡∃du. δ̂d ∧ υ̌u ⇔ ∃d < u0 . δ̂d ∧ υ̌u0 ≡ E1 >(δ, υ)≡⇔∃detu. (d < e) ∧ δe ∧ υt ∧ (t < u)∃et. δe ∧ υt ≡ B(δ, υ).

u0 > d, uDefinition 7.8 The bounded interval predomain is the open subspace IR ⊂ IR∞ classified byB, so it consists of those (δ, υ) for which B(δ, υ) is true. By Lemma 5.9, IR ⊂ ΣQ × ΣQ is definedby the nucleus
Erdb Φ(δ, υ) ≡ ∇(δ̂, υ̌) ∨ Φ(δ̂, υ̌) ∧ B(δ̂, υ̌),
which may be bracketed either way, since ∇ 6 B.
Warning 7.9 Here we are selecting the bounded pseudo-cuts from spaces of not necessarily
bounded ones. Nuclei that do this do not preserve >. This is related, via Lemma 5.13, to the factthat [d, u] is compact, but R is not.
The following rule of inference will simplify matters a lot in the next section. Abstractly, it isjust (monotonicity of) the I operator in Section 5 for the subspace IR ⊂ ΣQ × ΣQ .
Proposition 7.10 In proving any implication Φ 6 Ψ, we may assume that the pseudo-cuts
to which they are applied are rounded, bounded and disjoint (or even that they have rational
endpoints), at the cost of applying E1 to the result, in the sense thatΓ, (δ, υ) : IR ` Φ(δ, υ) ⇒ Ψ(δ, υ)Γ, δ, υ : ΣQ ` E1 Φ(δ, υ) ⇒ E1 Ψ(δ, υ).
Proof

If d < u then (δd , υu ) is rounded, bounded and disjoint, so
E1 Φ(δ, υ)≡∃d < u. δ̂d ∧ υ̌u ∧ Φ(δd , υu )⇒∃d < u. δ̂d ∧ υ̌u ∧ Ψ(δd , υu ) ≡ E1 Ψ(δ, υ).



Exercise 7.11 Use the following result to sharpen this rule to show that the premiseΓ, q : Q ` Φ(δq , υq ) ⇒ Ψ(δq , υq )is sufficient to deduce E1 Φ 6 E1 Ψ, and indeed EΦ 6 EΨ, as we shall see in the next section.
Next we invoke Scott continuity of Φ, cf. Lemma 2.16.
Q

Q

Proposition 7.12 If (δ, υ) are rounded and bounded then, for any Φ : ΣΣ ×Σ ,Φ(δ, υ) ⇐⇒ ∃du. δd ∧ υu ∧ Φ(δd , υu ).
If (δ, υ) are also disjoint then Φ(δ, υ) ⇐⇒ ∃d < u. δ̂d ∧ υ̌u ∧ Φ(δd , υu ) ≡ E1 Φ(δ, υ).
Proof We have to show that the joins in Notation 7.1,
δ̂ = ∃d. δd ∧ (λx. x < d)andυ̌ = ∃u. υu ∧ (λx. u < x),are directed in the sense of Definition 4.20, so consider
N ≡ Q,

αd ≡ δdand φd ≡ δd ≡ λx. x < d.
35Then ∃d. αd ⇔ > by boundedness, and the binary operation @ ≡ max satisfies

αd@e ≡ δ max(d, e) ⇐⇒ δd ∧ δe ≡ αd ∧ αeas δ is lower, and φd@e x ≡ x < max(d, e) ⇐= (x < d) ∨ (x < e) ≡ (φd ∨ φe )x.
For the second, we use @ ≡ min instead. Then we deduce the result for rounded and bounded(δ, υ) = (δ̂, υ̌) from Axiom 4.21. If they are also disjoint then δd ∧ υu ⇒ d < u by Lemma 7.5. It may perhaps be surprising that this is the (one) place where Scott continuity is used in theconstruction, given that the manipulation of finite lists will happen in the next section. The reason
is that this is the section in which we do domain theory. The intervals with rational endpoints
provide a basis for the domain of general intervals in the sense of Remark 2.9, and the Propositionshows how we extend the definition of Φ from the basis to the whole domain.
In fact, we have shown that there is at most one extension. We need another condition toensure that the extension exists, i.e. that we recover the given formula when we restrict back tothe basis. This requirement is more than monotonicity with respect to interval inclusions, since
the bounded interval predomain is a continuous but not algebraic dcpo.
Proposition 7.13 Let φ(d, u) be any predicate on d, u : Q, which are intended to be the endpointsof an interval. ThenΦ(δ, υ) ≡ ∃du. δd ∧ υu ∧ φ(d, u)
extends φ : Q × Q → Σ to Φ : ΣQ × ΣQ → Σ, in the sense that Φ(δd , υu ) ⇔ φ(d, u), iff
φ is rounded , φ(e, t) ⇔ ∃du. (d < e) ∧ (t < u) ∧ φ(d, u).
If φ satisfies the same condition in just the restricted case where d ≤ u, then it extends to thebounded interval predomain, Φ : IR → Σ, i.e. to rounded, bounded, disjoint pseudo-cuts (δ, υ). 
We shall use this condition in the definition of the nucleus E in the next section, and again forarithmetic in Sections 11–13. Here we may complete the construction of the (bounded) interval(pre)domain in ASD:
Theorem 7.14 E1 is a nucleus (Definition 5.5), and (δ, υ) is admissible for it (Definition 5.7) iff
QQ
it is rounded, bounded and disjoint, so IR ∼= {ΣΣ ×Σ | E1 }.
Proof If (δ, υ) are rounded, bounded and disjoint, Φ(δ, υ) ⇔ E1 Φ(δ, υ) by Proposition 7.12,
i.e. (δ, υ) is admissible. On the same hypothesis, therefore,(Φ ∧ Ψ)(δ, υ) ⇐⇒ (E1 Φ ∧ E1 Ψ)(δ, υ).
We deduce from this, using Proposition 7.10, that, for arbitrary (δ, υ),
E1 (Φ ∧ Ψ)(δ, υ) ⇐⇒ E1 (E1 Φ ∧ E1 Ψ)(δ, υ),which was one of the equations for a nucleus. We can prove the ∨-equation in the same way, orby observing that E1 is idempotent and preserves ∨.
Conversely, we have to deduce roundedness, boundedness and disjointness from instances ofadmissibility with respect to the new formula for E1 , using carefully chosen Φ, which are provided
by Lemmas 7.5 and 7.7.
For disjointness, let Φ ≡ ∇, so by admissibility, ∇(δ, υ) ⇔ E1 ∇(δ, υ) ⇔ ⊥.
For boundedness, let Φ ≡ λαβ. >, so B(δ, υ) ⇔ E1 Φ(δ, υ) ⇔ Φ(δ, υ) ⇔ >.
36

For roundedness, consider Φ ≡ λαβ. αc ∧ βw with c, w : Q, soΦ(δd , υu )Then⇔

E1 Φ(δ, υ) ⇔δd c ∧ υu w ⇔ (c < d) ∧ (u < w).
∃d < u. δ̂d ∧ υ̌u ∧ Φ(δd , υu )⇔∃du. δ̂d ∧ υ̌u ∧ (c < d) ∧ (d < u) ∧ (u < w)⇔δ̂c ∧ υ̌w ∧ (c < w) ⇔ δ̂c ∧ υ̌w,

since (δ̂, υ̌) are rounded and disjoint. By admissibility,δc ∧ υw ≡ Φ(δ, υ) ⇔ E1 Φ(δ, υ) ⇔ δ̂c ∧ υ̌w.



We conclude by looking at two other nuclei that also define IR.
Exercise 7.15 Show that(a) Er (Definition 7.3), Ed and Eb are nuclei, whereEr Φ(δ, υ) ≡ Φ(δ̂, υ̌),Ed Φ ≡ Φ ∨ ∇andEb Φ ≡ Φ ∧ B;(b) (δ, υ) is admissible for Er , Eb or Ed iff it is rounded, bounded or disjoint respectively (the last
being in the sense that we used in Definition 6.8 and Lemma 7.5(a,d,e,f));(c) Er , Eb and Ed commute pairwise (hint: use Lemmas 7.5 and 7.7);(d) the composite Erb ≡ Er · Eb ≡ Eb · Er is
Erb Φ(δ, υ) ⇐⇒ ∃du. δ̂d ∧ υ̌u ∧ Φ(δd , υu ) ⇐⇒ ∃et. δe ∧ υt ∧ Φ(δe , υt )(hint: use Axiom 4.7 with B(δ, υ) ⇔ > and Proposition 7.12); and(e) the composite Erdb (Definition 7.8) is Erdb = ∇ ∨ E1 (hint: use Axiom 4.7 with ∇(δ, υ) ⇔ ⊥and Lemma 7.5).
We prefer E1 because it preserves ⊥, whereas Erdb ⊥ = ∇. We use this property in Theorem 9.2 toconstruct the existential quantifier.

Exercise 7.16 Let E10 Φ(δ, υ) ≡ ∃d < u. δd ∧ υu ∧ Φ(δd , υu ) and show that(a) E10 is a nucleus;(b) (δ, υ) is admissible for E10 iff it is rounded, bounded and disjoint (hint: the only difficulty withcopying the proof for E1 is that it only shows that admissible (δ, υ) are disjoint, bounded andsatisfy δ 6 δ̂ and υ 6 υ̌, so a little more work is needed to deduce roundedness);(c) E10 also satisfies E10 = E10 · Er = E10 · Er · E10 6 E1 = Er · E10 = Er · E10 · Er ; but(d) there are δ, υ : ΣQ for which E1 >(δ, υ) ⇔ > and E10 >(δ, υ) ⇔ ⊥ (hint: cf. Lemma 7.7).
We prefer E1 because it commutes with Er (cf. Lemma 5.11), so the Σ-splitting for IR  ΣQ × ΣQgiven by E1 restricts to IR  R × R.

8

The real line as a space in ASD

We are at last ready to construct R as a Σ-split subspace of the bounded interval predomain IR,
and hence of ΣQ × ΣQ .
Remark 8.1 Because of Lemma 5.11, the process of defining R by means of a nucleus E on IR,
where IR is in turn defined by a nucleus E1 on ΣQ × ΣQ , is the same as giving a nucleus E on thelarger space for which
E · E1 = E = E · E = E1 · E.
37

Naturally, it will simplify the proof if we can restrict attention to (δ, υ) : IR, i.e. pseudo-cuts thatare rounded, bounded and disjoint, thereby isolating locatedness.
However, another reason for considering R as a subspace of IR is that E then becomes a nucleus
in the sense of both ASD and locale theory (Definition 5.5). The latter says that id 6 E = E 2 andit preserves meets, so we have to prove that
Φ(δ, υ) ⇔ E1 Φ(δ, υ) ⇒ EΦ(δ, υ)andEΦ(δ, υ) ∧ EΨ(δ, υ) ⇒ E(Φ ∧ Ψ)(δ, υ),on the assumption that (δ, υ) : IR. (Only the last of these actually remains to be done.) We use
Proposition 7.10 to eliminate this hypothesis, by applying E1 . In Proposition 8.9 we shall deduce
the equations in Lemma 5.4 from these results.
Notation 8.2 As the formula in Proposition 2.17 only involves variables ranging over Q, ΣQ andQQΣΣ ×Σ , we may import it into the logic of ASD. However, we prefer to useEΦ(δ, υ) ≡ ∃n ≥ 1. ∃q0 < · · · < qn . δ̂q0 ∧ υ̌qn ∧n−1^

Φ(δqk , υqk+1 ),k=0with δ̂ and υ̌ instead of δ and υ, and no n ≡ 0 term (which would be ∇). The reason is the same
as for the choice of E1 in preference to E10 or Erdb , namely that it commutes with Er and preserves⊥ (Exercises 7.15f). Propositions 2.15 and 2.17 could be adapted to this choice by replacing I
there withIV ≡ {(D, U ) | ∃deut. d < e ∧ e ∈ D ∧ [d, u] ⊂ V ∧ t ∈ U ∧ t < u}.
We have already said in Remark 6.15 that equality on Q must be decidable in order to use ASD’s
methods of “discrete mathematics”. In particular, note that “∃q0 < · · · < qn ” is existential
quantification over List(Q), not just n + 1-fold quantification over Q.
Notice that E1 is the n ≡ 1 disjunct of E, so E1 6 E.
We begin with some lemmas for managing the sequence.
Lemma 8.3 For any (δ, υ), suppose EΦ(δ, υ) holds by virtue of the sequence q0 < · · · < qn , andthat q0 ≤ r ≤ qn . Then EΦ(δ, υ) also holds by virtue of the sequence obtained by inserting r.
Proof If qk < r < qk+1 then Φ(δqk , υqk+1 ) ⇒ Φ(δqk , υr ) ∧ Φ(δr , υqk+1 ).
Lemma 8.4 For any Φ, and understanding that q0 ≡ d and qn ≡ u, the predicate
θ(d, u) ≡ ∃d < q1 < · · · < qn−1 < u.

n−1^

Φ(δqk , υqk+1 )k=0

is rounded, in the sense that θ(e, t) ⇐⇒ ∃du. (d < e) ∧ (t < u) ∧ θ(d, u) =⇒ e < t.
Proof First, θ(d, u) ⇒ d < u because there are d < q1 < · · · < qn−1 < u.
[⇐] If θ(d, u) holds by virtue of some sequence d = q0 < · · · < qn = u, and d < e < t < u, thenthe same sequence with e and t in place of q0 and qn , but omitting any qi < e or > u, justifies
θ(e, t).
[⇒] By Lemma 8.3, we may assume that n ≥ 3 in the expansion of θ. The idea is to separate
the left- and rightmost conjuncts from the rest, and then enlarge them using Proposition 7.12:
θ(d, u) ⇔∃d < e < t < u. Φ(δd , υe ) ∧ θ(e, t) ∧ Φ(δt , υu )⇔∃c < d < e < t < u < w. Φ(δc , υe ) ∧ θ(e, t) ∧ Φ(δt , υw )⇒∃c < d < u < w. θ(c, w).
38This was the condition in Proposition 7.13 for θ to extend from intervals with rational endpoints
to more general rounded, bounded and disjoint ones:
Lemma 8.5 If d < u thenEΦ(δd , υu ) ⇐⇒ ∃d < q1 · · · < qn−1 < u.

n−1^

Φ(δqk , υqk+1 ).

k=0

Although θ(d, u) ⇔ ⊥ when d ≥ u, we shall see in Propositions 8.12 and 10.5 that, in this case,EΦ(δx , υx ) ⇐⇒ Φ(δx , υx )EΦ(δd , υu ) ⇐⇒ ∃x:[u, d]. Φ(δx , υx ).

andProof The expansion of EΦ(δd , υu ) involves δd q0 ∧υu qn ≡ (q0 < d < u < qn ). So, by Lemma 8.3,
we may assume that d and u occur in the given sequence, say as d ≡ qi , u ≡ qj . But thenq0 , . . . , qi−2 and qj+2 , . . . , qn are redundant, so without loss of generality d ≡ q1 and u ≡ qn−1 .
Hence by Lemma 8.4,
EΦ(δd , υu ) ⇐⇒ ∃q0 < d < u < qn . θ(q0 , qn ) ⇐⇒ θ(d, u).



We can now carry out the plan in Remark 8.1. The first two results say that the subspace R
that will be defined by E is contained in that defined by E1 , which is IR. Notice that the expansionof E1 ·E in the second result inherits the δ̂ and υ̌ from E1 , so they must also be used in the definitionof E in order to obtain the equation E1 · E = E.
Lemma 8.6 E(E1 Φ)(δ, υ) ⇐⇒ EΦ(δ, υ) and E1 (EΦ)(δ, υ) ⇐⇒ EΦ(δ, υ).
Proof The first part involves the conjuncts E1 Φ(δqk , υqk+1 ) that occur in the expansion of theformula for E(E1 Φ)(δ, υ). Such (δqk , υqk+1 ) are rounded, bounded and disjoint, so
E1 Φ(δqk , υqk+1 ) ⇐⇒ Φ(δqk , υqk+1 )by Proposition 7.12. These are the same conjuncts that are used in the expansion of EΦ(δ, υ).
In the second part, using Lemma 8.5,
E1 (EΦ)(δ, υ) ≡≡≡∃d < u. δ̂d ∧ υ̌u ∧ EΦ(δd , υu )∃d < u. δ̂d ∧ υ̌u ∧ ∃d < q1 · · · < qn−1 < u.

n−1^

Φ(δqk , υqk+1 )k=0EΦ(δ, υ).



Lemma 8.7 E 2 Φ(δ, υ) =⇒ EΦ(δ, υ).
Proof The outer E of E 2 involves a sequence q0 < · · · < qn and conjuncts EΦ(δqk , υqk+1 ) for
each 0 ≤ k ≤ n − 1. By Lemma 8.5, the expansion of each of these involves a sequence
qk = rk,0 < · · · < rk,mk = qk+1
with conjuncts Φ(δrk,j , υrk,j+1 ). All of these sequences can be concatenated, to yield one thatjustifies EΦ(δ, υ).
The final preparatory result is the one that says that E is a nucleus on IR in the sense of locale
theory, as well as that of ASD.
Proposition 8.8 If (δ, υ) are rounded, bounded and disjoint thenE>(δ, υ) ⇐⇒ >andEΦ(δ, υ) ∧ EΨ(δ, υ) =⇒ E(Φ ∧ Ψ)(δ, υ).
39

Proof As (δ, υ) are rounded and bounded, > ⇔ E1 >(δ, υ) ⇒ E>(δ, υ) by Lemma 7.7.
Suppose that EΦ and EΨ are justified by sequences q0 < · · · < qn and r0 < · · · < rm respectively. Letd ≡ max(q0 , r0 ) and u ≡ min(qn , rm ),so d is either q0 or r0 , which both satisfy δ, so δd holds, as similarly does υu. Since (δ, υ) arerounded and disjoint, d < u by Lemma 7.5. Now letd ≡ s0 < · · · < s` ≡ u
be the union of the given sequences q0 < · · · < qn and r0 < · · · < rm , removing duplicates
and those terms < d or > u. Such outlying points were already redundant in the expansion ofEΦ(δ, υ) and of EΨ(δ, υ), whilst by Lemma 8.3 we may adjoin the members of one sequence to theother. Hence the new combined sequence serves for both EΦ(δ, υ) and EΨ(δ, υ), and therefore forE(Φ ∧ Ψ)(δ, υ) too.

Q

Q

Proposition 8.9 E is a nucleus (Definition 5.5), as it satisfies, for Φ, Ψ : ΣΣ ×Σ ,E(Φ ∧ Ψ) = E(EΦ ∧ EΨ)Proof

and E(Φ ∨ Ψ) = E(EΦ ∨ EΨ).

For (δ, υ) : IR, Proposition 7.12 gives Φ(δ, υ) ⇔ E1 Φ(δ, υ) ⇒ EΦ(δ, υ), so(Φ ∧ Ψ)(δ, υ) ⇒ (EΦ ∧ EΨ)(δ, υ)(Φ ∨ Ψ)(δ, υ) ⇒ (EΦ ∨ EΨ)(δ, υ)andEΦ(δ, υ) ∨ EΨ(δ, υ) ⇒ E(Φ ∨ Ψ)(δ, υ),

whilstEΦ(δ, υ) ∧ EΨ(δ, υ) ⇒ E(Φ ∧ Ψ)(δ, υ)

by Proposition 8.8. Then we use Proposition 7.10 to eliminate the hypothesis (δ, υ) : IR, andobtain the first inequality in each row:
E1 (Φ ∧ Ψ) 6

E1 (EΦ ∧ EΨ)

6 E(EΦ ∧ EΨ)E1 (Φ ∨ Ψ) 6

E1 (EΦ ∨ EΨ)

6 E(EΦ ∨ EΨ)E1 (EΦ ∧ EΨ) 6 E1 (E(Φ ∧ Ψ)) 6
E1 (EΦ ∨ EΨ) 6 E1 (E(Φ ∨ Ψ)) 6

E 2 (Φ ∧ Ψ)
2

E (Φ ∨ Ψ)

6 E(Φ ∧ Ψ)
6 E(Φ ∨ Ψ).

The second inequality follows from E1 6 E, and the third, E 2 6 E, is Lemma 8.7. Finally, fromeach E1 Θ 6 EΩ, we deduce EΘ = E(E1 Θ) 6 E 2 Ω 6 EΩ by Lemmas 8.6 and 8.7.
This fulfils the obligation that we have before invoking the ASD technology in Section 5, so
QQ
we can now introduce the type R ≡ {ΣΣ ×Σ | E}. We still have to characterise its admissible
terms, i.e. to show that the equalisers in Remarks 5.2 and 6.9 are isomorphic.
The following is the main lemma to do this. In it, (δ, υ) need not be disjoint, so it may represent
a back-to-front interval like those in Remark 2.20, which we shall use to compute existential
quantifiers. In the proof, we have to switch back from using abutting closed intervals to overlapping
open ones, cf. the proof of Proposition 2.17.
Lemma 8.10 If (δ, υ) is located then EΦ(δ, υ) ⇐⇒ E1 Φ(δ, υ).

40

Proof [⇐] is trivial. For [⇒], we use Proposition 7.12 to widen the argument of each conjunctΦ a little towards the right, from [qk , qk+1 ] to [qk , rk+1 ], for any qk+1 < rk+1 < qk+2 :EΦ(δ, υ)≡∃q0 < · · · < qn . δ̂q0 ∧ υ̌qn ∧n−1^

Φ(δqk , υqk+1 )k=0⇒∃q0 < r0 < q1 < r1 < · · · < qn < rn . δ̂q0 ∧ υ̌rn ∧n−1^

Φ(δqk , υrk+1 ),k=0where υ̌qn ⇒ υ̌rn because υ̌ is upper. As (δ̂, υ̌) is located with δ̂q0 and υ̌rn , we may apply
Lemma 6.16 to this sequence. Because of the alternation of letters, it gives
n−1
_

n−1
_

(δ̂qk ∧ υ̌qk+1 ) ∨k=0(δ̂rk ∧ υ̌rk+1 ).

k=0

We already have the corresponding Φ(δqk , υqk+1 ) from the original abutting expansion, whilst theone with overlapping intervals provides
Φ(δqk , υrk+1 ) =⇒ Φ(δrk , υrk+1 ),since δqk 6 δrk . Hence, with e ≡ qk < t ≡ qk+1 or e ≡ rk < t ≡ rk+1 , we haveEΦ(δ, υ) =⇒ ∃e < t. δ̂e ∧ υ̌t ∧ Φ(δe , υt ) ≡ E1 Φ(δ, υ).



Lemma 8.11 If (δ, υ) is rounded and bounded, and EΦ(δ, υ) =⇒ E1 Φ(δ, υ) for all Φ, then (δ, υ)
is located.
Proof For any d < u, there is a sequence of rationals
q0 < d < q 1 < u < q 2

with δq0

and υq2 .

These numbers satisfy δq0 d ⇔ ⊥, υq1 u ⇔ >, δq1 d ⇔ > and υq2 u ⇔ ⊥, so∃q0 < q1 < q2 . δq0 ∧ υq2 ∧ (δq0 d ∨ υq1 u) ∧ (δq1 d ∨ υq2 u).
This is the n ≡ 2 disjunct of EΦ(δ, υ), where Φ(α, β) ≡ αd ∨ βu. By hypothesis, this implies
E1 Φ(δ, υ), whereE1 Φ(δ, υ) ≡≡∃e < t. δe ∧ υt ∧ Φ(δe , υt )∃e < t. δe ∧ υt ∧ (d < e ∨ t < u) ⇒ δd ∨ υu.



Proposition 8.12 (δ, υ) is a cut iff it is admissible for E.
Proof If it’s a cut then in particular it’s rounded, bounded and disjoint, so Φ(δ, υ) ⇔ E1 Φ(δ, υ)
by Proposition 7.12. As it’s also located, EΦ(δ, υ) ⇔ E1 Φ(δ, υ) by Lemma 8.10, so (δ, υ) is
admissible.
Conversely, admissibility of (δ, υ) for E with respect to both Φ and E1 Φ, giveΦ(δ, υ) ⇐⇒ EΦ(δ, υ) ⇐⇒ E(E1 Φ)(δ, υ) ⇐⇒ E1 Φ(δ, υ),
where the middle implication is Lemma 8.6. Hence (δ, υ) is also admissible for E1 , so it is rounded,bounded and disjoint by Theorem 7.14. It is also located, by Lemma 8.11.
Q

Q

Theorem 8.13 The type R ≡ {ΣΣ ×Σ | E} is the equaliser in Remark 6.9, i.e. its terms are
Q
Q
Dedekind cuts, and the inclusion R  ΣΣ ×Σ is Σ-split.
In the following two sections, we shall show that this construction does make the real line Dedekindcomplete and the closed interval compact.
41

9

Dedekind completenessIn this section we shall prove Dedekind’s main result, that any cut of R corresponds to an elementof R, and not one of a yet more complicated structure. However, in order to say what a “Dedekind
cut of R” is, we must finish the proof that its order (Definition 6.10) is dense without endpoints,
i.e. that it satisfies Definition 6.1. This in turn requires that the object R be overt and Hausdorff.
In this section we shall be particularly careful to state the inclusion j : Q → R that we definedin Lemma 6.12 by q 7→ (δq , υq ), although we usually elide it elsewhere.
Lemma 9.1 Any property Φ that is true of some real number (i.e. a cut a ≡ (δ, υ)), is also trueof some interval [e, t] around it, in the sense that
Φ(δ, υ) ⇔⇒∃e < t:Q. δe ∧ υt ∧ Φ(δe , υt )∃e < t:Q. δe ∧ υt ∧ Φ(δe , υe ) ∧ Φ(δt , υt ).

So in particular it is true of any sufficiently close rational e or t, i.e.
Φ(ix) ≡ Φ(δ, υ) =⇒ ∃q:Q. Φ(δq , υq ) ≡ ∃q:Q. Φ(ijq).
Note, however, that we cannot yet write ∀x:[e, t]. Φ(ix), but see Corollary 10.8.
Proof The first part is Proposition 7.12 in the case where (δ, υ) is a cut (rounded, bounded,disjoint and located). For the second part, δe 6 δt and υt 6 υe .
Theorem 9.2 R is overt, in which the existential quantifier satisfies the ruleΓ, x : R ` φx ⇒ σ=================Γ ` ∃x:R. φx ⇒ σ
for any Γ ` φ : ΣX , σ : Σ, where∃x:R. Φ(ix) ⇔ ∃q:Q. Φ(ijq) ⇔ E1 Φ(>, >) ⇔ EΦ(>, >) ⇒ Φ(>, >).
However, the converse of the last implication fails for Φ ≡ ∇ (Lemma 7.5).
Proof This is an application of Lemma 5.13, using the fact that ΣQ × ΣQ is a lattice and IR is
the subspace of it that is defined by the nucleus E1 , which preserves ⊥.
Let’s also give the proof directly. As Q is overt, we already have the rule with Q in place of
R. The top line (for R) entails the similar judgement for Q by restriction, and then this entails
the common bottom line. Conversely, by Lemma 9.1, φx ⇒ ∃q:Q. φ(jq) ⇒ σ. Using it again,∃q:Q. Φ(δq , υq ) ⇔ ∃d < q < u. Φ(δd , υu ) ⇔ ∃d < u. Φ(δd , υu ) ≡ E1 Φ(>, >)by Proposition 7.12.
Finally, we can use Lemma 8.10 to interchange E and E1 in the definition of ∃, that is,EΦ(>, >) ⇔ E1 Φ(>, >), because (>, >) is located.

Next we consider the application to R of the axioms that we introduced for Q in Section 6,
namely dense linear orders, roundedness, boundedness, disjointness and locatedness. Their definitions involve existential quantification over R, but by Theorem 9.2 we may replace this byquantification over Q.
Theorem 9.3 R is Hausdorff (Definition 4.12), and < (Definition 6.10) is a dense linear
order without endpoints (Definition 6.1).
42

ProofBy Proposition 6.14, if a ≡ (δ, υ) and b ≡ (, τ ) are cuts thena = b:R================
=====(a < b) ∨ (b < a) ⇔ ⊥so R is Hausdorff, and the order satisfies the trichotomy law (Definition 6.1(c)); this is transitive
by Lemma 6.11. It is extrapolative and interpolative in the sense that> ⇐⇒ ∃du:Q. δd ∧ υu ⇐⇒ ∃du. (δd , υd ) < (δ, υ) < (δu , υu )and(δ, υ) < (, τ )=⇒∃q:Q. (δ, υ) < (δq , υq ) < (, τ ),but this existential quantification over Q may be considered as one over R.

We can now define Dedekind cuts over R, i.e. to formulate Definition 6.8 and essentially torepeat the construction with R in place of Q. In doing so, we find once again that the ascending
and descending reals are natural intermediate steps. As before, it is easy to define them, and toshow that they are the same, whether we start from Q or from R, cf. Exercise 2.2. After that,
we simply have to show that the other conditions carve out R ⊂ R × R in the same way in bothversions.
Proposition 9.4 The maps ΣQ  ΣR given byδ 7→ λr:R. ∃e:Q. r < je ∧ δe and λd:Q. ∆(jd) ←7 ∆restrict to a bijection between rounded lower δ : ΣQ and ∆ : ΣR . Hence the two constructions of
R agree. Those for R do so too, with
υ 7→ λr:R. ∃t:Q. jt < r ∧ υt
Proofand λu:Q. Υ(ju) ←7 Υ.

Recall from Lemmas 6.12f that jd <R je ⇔ d <Q e and (δ, υ) <R ju ⇔ υu. Thenˆ
∆ 7→ δ 7→ λr. ∃e:Q. r < je ∧ ∆(je) = λr. ∃s:R. r < s ∧ ∆(s) ≡ ∆by Theorem 9.2, and δ 7→ ∆ 7→ λd. ∃e. jd <R je ∧ δe ≡ λd. ∃e. d <Q e ∧ δe ≡ δ̂.

Proposition 9.5 Under this correspondence, the rounded pseudo-cut (∆, Υ) of R is respectively
disjoint, bounded or located iff the pseudo-cut (δ, υ) of Q has the same property.
Proof

For disjointness, using Theorem 9.2,∇(∆, Υ)≡∃rs:R. ∆r ∧ (s < r) ∧ Υs⇔⇔

∃du:Q. ∆(jd) ∧ (u < d) ∧ Υ(ju)∃du:Q. δd ∧ (u < d) ∧ υu ≡ ∇(δ, υ),and the argument for B and boundedness just omits s < r and u < d.
If (δ, υ) is located then so is (∆, Υ), because, since jd <R jt ⇔ e <Q t ⇒ δe ∨ δt,r < s ⇒ ∃et:Q. r < je < jt < s ⇒ (∃e. r < je ∧ δe) ∨ (∃t. jt < s ∧ υt) ≡ ∆r ∨ Υs.
Conversely, if (∆, Υ) is located then so is (δ, υ), becaused <Q u ⇐⇒ jd <R ju ⇒ ∆(jd) ∨ Υ(ju) ≡ δd ∨ υu.
43Theorem 9.6 (R, <) is a Dedekind-complete dense linear order without endpoints, in the sensethat every cut (∆, Υ) : ΣR × ΣR (possibly involving parameters) is of the form
∆ = λx. (x < a)and

Υ = λy. (a < y)for some unique a : R (with the same parameters).
Proof The real number a is the cut (δ, υ) of Q given by the above correspondence. It satisfies
x < a < y ⇐⇒ (∃e:Q. x < je ∧ δe) ∧ (∃t:Q. jt < y ∧ υt) ≡ ∆x ∧ Υy.

Remark 9.7 In the previous section, the construction of R from Q involved the formulation of
the nucleus E. However, we cannot repeat this step with R in place of Q, because existential
quantification over finite lists in R is not allowed in Notation 8.2.
Why on Earth not? This has nothing to do with rational or irrational numbers: so far theelements of Q are only nominally “rational”, as we have not introduced any arithmetic yet. The
point is topological: Q is overt discrete — essentially a “set” — and List(Q) is the overt discrete“hyperspace” of its overt compact subspaces (Theorem 5.21). On the other hand, R is not discrete
but Hausdorff, and its overt compact subspaces can be infinite — bounded closed intervals, forexample. In the hyperspace of such subspaces, the finite ones form a dense subspace, so there is
no way to distinguish them from the infinite ones.
But this does not matter. We do not need to define another space S  ΣR × ΣR from such
an E, as we have already done enough to prove completeness, so R itself serves for S. ThenR  IR  R × R  ΣR × ΣR
is a composite of Σ-split inclusions. In fact, the splitting will be expressible in the same way as in
Proposition 2.15, after we have proved compactness of [d, u] (Proposition 14.7).
Two other important notions of completeness for the real line are considered in [J], namely theconvergence of Cauchy sequences and the existence of suprema of nonempty bounded subsets. In
any form of constructive analysis, the latter result requires additional hypotheses; in ASD these
are that the subset be compact and overt.
A natural special case of the supremum is the maximum of a pair:
Proposition 9.8 R has binary join and meet with respect to ≤,
max (δ1 , υ1 ), (δ2 , υ2 ) ≡ (δ1 ∨ δ2 , υ1 ∧ υ2 )
min (δ1 , υ1 ), (δ2 , υ2 )
≡ (δ1 ∧ δ2 , υ1 ∨ υ2 ).
satisfying min(a, b) ≤ a, b ≤ max(a, b) and(a < x) ∧ (b < x) ⇔(a > x) ∨ (b > x) ⇔(a ≤ x), (b ≤ x) a`(a > x) ∧ (b > x) ⇔(a < x) ∨ (b < x) ⇔(a ≥ x), (b ≥ x) a`

max(a, b) < xmax(a, b) > xmax(a, b) ≤ x

min(a, b) > x
min(a, b) < x
min(a, b) ≥ x.

We have said that the two halves of a Dedekind cut play symmetrical roles. Adding an operationthat makes this literally so, we have the beginnings of arithmetic:
Proposition 9.9 If (Q, <) has an order-reversing automorphism (−) then so does R, and thishas a unique fixed point (0):(δ, υ) ≡ λd. υ(−d), λu. δ(−u)
0 ≡ (λd. d < −d, λu. − u < u).
44This agrees with Moore’s interval arithmetic, since (δd , υu ) = (δ−u , υ−d ). Since it preserves
roundedness, it defines an isomorphism R ∼= R (Definition 7.3), but not an automorphism of eitherof them. Since it also preserves disjointness, boundedness and locatedness, we have : IR ∼= IRand − : R ∼R.
=
From negation and maximum we may define the absolute value function,|(δ, υ)| ≡ max (δ, υ), −(δ, υ) = λd. δd ∨ υ(−d), λu. υu ∧ δ(−u) ,so |x| = x if x ≥ 0 and |x| = −x if x ≤ 0. This satisfies (x 6= 0) ≡ (δ0 ∨ υ0) ⇔ |x| =6 0.



We shall develop addition and multiplication in Sections 11 and 12, and we use Dedekind
completeness to find the inverses of strictly monotone functions in Section 13, but now we turn to
the Heine–Borel theorem.

10Open, compact and overt intervals

In this section we prove that the closed interval is compact and overt, in the sense of Definition 4.14,
namely that it admits both “quantifiers”, ∀ and ∃. The constructions formalise in ASD some of
the ideas that we met in the context of interval analysis in Section 2. We compute the universal
quantifier ∀x:[d, u]. φx by splitting the interval into sufficiently but finitely many sub-intervals,
and applying φ to each of them à la Moore. The existential quantifier, on the other hand, isrelated to the back-to-front (Kaucher) intervals that we saw in Remark 2.20.
First, of course, we have to construct the closed interval itself, and for the sake of symmetry
the open one too, as objects of ASD. These are defined by means of terms of type ΣR .
Definition 10.1 For d ≤ u : R, the open and closed intervals (d, u), [d, u] ⊂ R are(a) the open subspace classified by (λx. d < x < u) ≡ (υd ∧ δu ) : ΣR , and(b) the closed subspace co-classified by (λx. x < d ∨ u < x) ≡ (δd ∨ υu ) : ΣR respectively.
More generally, for any rounded pair (δ, υ),(c) (υ, δ) ⊂ R is the open subspace classified by υ ∧ δ : ΣR , and(d) [δ, υ] ⊂ R is the closed subspace co-classified by δ ∨ υ : ΣR ,where we expect the pseudo-cut (δ, υ) to be located (maybe overlapping or back-to-front) in thefirst case and disjoint in the second.
Remark 10.2 The ASD subspaces that are defined by these terms were constructed in Remarks 5.8ff. However, as we have not allowed dependent types in the calculus, we must temporarily restrict attention to intervals with constant endpoints, so d, u, δ and υ cannot have parameters.
In other words, we are essentially just dealing with the unit interval I ≡ [0, 1], where d ≡ 0, u ≡ 1.
But this is no real handicap, since (when we have some arithmetic) the general interval [d, u] withendpoints will be the direct image of [0, 1] under the function t 7→ d(1 − t) + ut. This actually
generalises to all rounded bounded (δ, υ). The outcome is that the formulae that we obtain in theend remain valid with parametric endpoints [J].
Even if we had a theory of dependent types and tried to use it to prove the results in thissection, we would still have to demonstrate that the formulae that look like nuclei or quantifiers
actually correspond to (dependent) subspaces. That would be at least as difficult as the approachthat we take here.
On the other hand, terms with parameters have been familiar for centuries, and translate more
directly into programs. In [J] we will use modal operators (quantifiers over subspaces) derived
from f as a tool for solving the equation f (x) = 0, naturally involving the same parameters as45

the function. These operators are (Scott) continuous in the parameters, which means that wemay still work with them in the vicinity of singularities of the equation, where the sets or typesof zeroes are discontinuous.
Proposition 10.3 Any open subspace U ⊂ R classified by θ : ΣR is overt. This applies inparticular to the open intervals (d, u) and (υ, δ) in Definition 10.1. The existential quantifiers aredefined for φ : ΣR by∃x:U . φx≡∃x:R. θx ∧ φx∃x:(d, u). φx ≡∃x:R. (d < x < u) ∧ φx∃x:(υ, δ). φx∃x:R. υx ∧ δx ∧ φx,≡in which ∃x : R was defined in Theorem 9.2 and is the same as ∃x : Q.
Proof We may deduce in both directions:Γ, x : U`Γ, x : R, θx ⇔ >` φx ⇒ σ

φx ⇒ σΓ, x : RΓ``θx ∧ φx ⇒ σ(∃x:R. θx ∧ φx) ⇒ σ

Axiom 4.7
R overtso ∃x:R. θx ∧ φx satisfies the defining property of ∃x:U . φx.

Remark 10.4 The main task of this section is to show that, for d ≤ u, the closed interval [d, u]
is overt and compact. The quantifiers ∃ and ∀ will be given by∃x:[d, u]. φx ⇔ E1 Φ(δu , υd ) ⇔ EΦ(δu , υd )and∀x:[d, u]. φx ⇔ EΦ(δd , υu ),where Lemma 8.10 allows us to interchange E with E1 in the existential quantifier, because theargument (δu , υd ) is located.
Here Φ : ΣQ × ΣQ → Σ is any extension of φ : R → Σ. As in Remark 2.5, the canonical one isΦ ≡ Iφ, but the Moore–Kaucher interpretation of the arithmetical operations may be used to findanother extension in a more practical way. In any case, the notation is simpler if we put things
the other way round, working primarily with Φ, so that φx ≡ Φ(ix) ≡ Φ(δx , υx ).
We first show that the closed interval, like the open one, is overt, by a generalisation ofTheorem 9.2. Since E1 preserves ⊥, this may also be seen as an application of Lemma 5.13 to thelattice R × R ↓ (δu , υd ) of rounded pseudo-cuts with (δ, υ) ≤ (δu , υd ). Recall that L ↓ α means{β : L | β 6 α}.
Proposition 10.5 The closed interval [d, u] is overt, with ∃x:[d, u]. Φ(ix) ≡ E1 Φ(δu , υd ).
Γ, x : R, d ≤ x ≤ u ` φx ⇒ σ==========================Γ ` ∃x:[d, u]. φx ⇒ σ
Notice that, as in Remark 2.20, u and d are the “wrong” way round.
Proof This is similar to Proposition 10.3. By Lemma 9.1, the top line of the rule isΓ, x, d, u : R, d ≤ x ≤ u ` φx ≡ ∃et. e < x < t ∧ Φ(δe , υt ) ⇒ σ,which, by Definition 4.14 (for ∃) and Axiom 4.7, is equivalent to
Γ, x, d, u, e, t : R, d ≤ x ≤ u, e < x < t ` Φ(δe , υt ) ⇒ σ.
46

The inequalities on the left of the ` are equivalent tod ≤ u,

max(d, e) ≤ x ≤ min(t, u),e < t,

e < u,

d < t,

the last three of which can be moved back across the `, using Definition 4.14 and Axiom 4.7 again,
whilst x is now redundant. HenceΓ, d, u : R, d ≤ u ` E1 Φ(δu , υd ) ≡ ∃e < t. e < u ∧ d < t ∧ Φ(δe , υt ) ⇒ σ,which is the bottom line of the rule.



Exercise 10.6 Show that ∃x:[d, u]. φx =⇒ φd ∨ (∃x:R. d < x < u ∧ φx) ∨ φu.



Now we come to the principal result of this paper, that the closed interval [d, u] is compact.
The proof may be considered as another example of Lemma 5.13, with[d, u] ⊂ {(δ, υ) : IR | δd 6 δ & υu 6 υ}.
Theorem 10.7 The closed interval [d, u] ⊂ R is compact in the sense of Definition 4.14:
Γ, x : [d, u] ` σ ⇒ φx ≡ Φ(ix)==========================================Γ ` σ ⇒ ∀x:[d, u]. φx ≡ Iφ(δd , υu ) ≡ EΦ(δd , υu )
Proof
Then

In the upward direction, let (δ, υ) ≡ (δx , υx ) > (δd , υu ) be the cut corresponding to x : R.
Γ ` σ ⇒ Iφ(δd , υu ) ⇒ Iφ(δ, υ) ≡ Iφ(ix) ⇔ φx.
Q

Q

For the converse, first let ψ ≡ λx. (x > u ∨ x < d) : ΣR and Ψ ≡ λαβ. αu ∨ βd : ΣΣ ×Σ , so
ψ = Σi Ψ co-classifies [d, u] (Definition 10.1). Using Axiom 4.7, the top line says
Γ, x : R ` φx ∨ ψx ≡ φx ∨ (x < d) ∨ (x > u) ⇔ >.
This captures universal quantification as a judgement (Definition 4.4). By λ-abstraction,Γ ` Σi (Φ ∨ Ψ) = Σi Φ ∨ Σi Ψ = φ ∨ ψ = > = Σi > : ΣR ,so if we apply I to this, where E = I · Σi , and the result to (δd , υu ), we haveE(Φ ∨ Ψ)(δd , υu ) ⇔ E>(δd , υu ) ⇔ >by Lemma 8.5. In the expansion of E(Φ ∨ Ψ)(δd , υu ), the same Lemma uses conjuncts like(Φ ∨ Ψ)(δqk , υqk+1 ) ⇔ Φ(δqk , υqk+1 ) ∨ (u < qk ∨ qk+1 < d) ⇔ Φ(δqk , υqk+1 ) ∨ ⊥.
Hence

> ⇔ EΦ(δd , υu ) ⇔ E(Φ ∨ Ψ)(δd , υu ).

Corollary 10.8 Re-substituting Definition 8.2 of E,∀x:[d, u]. Φ(ix)⇔EΦ(δd , υu )⇔∃d < · · · < u.

⇐
Φ(ix) ≡ Φ(δx , υx ) ⇒∃x:[d, u]. Φ(ix)Φ(δd , υu )n−1^

Φ(δqk , υqk+1 )k=0∃d < x < u. Φ(δd , υu )⇒ ∃d < x < u. ∀y:[d, u]. Φ(iy) ⇒ Φ(ix)⇔ E1 Φ(δu , υd )⇔∃et. t < u ∧ d < e ∧ Φ(δt , υe )⇒Φ(δu , υd ),47

using Notation 7.1, Lemmas 8.3, 8.5 and 9.1 and Proposition 10.5.

Warning 10.9 In view of the fact that both quantifiers are given by almost the same formula,
the hypothesis d ≤ u must be important. If we do not know this, we can still obtain the bounded
universal quantifier as∀d ≤ x ≤ u. Φ(ix) ≡ (d > u) ∨ EΦ(δd , υu ),but for the existential quantifier we have to writeQQΦ : ΣΣ ×Σ , d ≤ u : R ` ∃d ≤ x ≤ u. Φ(ix) ≡ EΦ(δu , υd ).
This is because (∃d ≤ x ≤ u. >) ⇔ > a` (d ≤ u) a` (d > u) ⇔ ⊥, making a positive statement
equivalent to a negative one. But that would make the predicate (d > u) decidable, which it can
only be if we had already assumed that it was either true or (in fact) false.
Notice that the intersection of two overt subspaces need not be overt, even in the simple case of[d, u] ∩ [e, t]. This is because we need to be able to decide whether they are disjoint (t < d ∨ u < e)or overlap (t ≥ d & u ≥ e). We shall see more examples of this in [J].
While we’re looking at awkward cases, recall from Theorem 9.2 that
∃x:R. Φ(ix) ⇐⇒ EΦ(>, >),and it’s easy to check that ∃x ≤ u. Φ(ix) ⇔ EΦ(δu , >) and ∃x ≥ d. Φ(ix) ⇔ EΦ(>, υd ).
So what happens if we let one or both of the arguments of EΦ be ⊥? Does this give a meaningto φ(∞) ≡ limx→∞ φx or to ∀−∞ ≤ x ≤ ∞. φx? Unfortunately not: putting δ or υ ≡ ⊥ in
Notation 8.2 just gives ⊥.
Remark 10.10 You are probably wondering where the “finite open sub-cover” has gone. Essentially, it was absorbed into the axioms, in the form of general Scott continuity (Axiom 4.21).
Compactness is often said to be a generalisation of finiteness. We dissent from this. The
finiteness is a side-effect of Scott continuity. The essence of compactness lies, not in that thecover be finite, but in what it says about the notion of covering. Recall how the statement ofequality became an (in)equality predicate in a discrete or Hausdorff space (Remark 4.6). Similarly,
compactness promotes the judgement (Definition 4.4),. . . , x : [d, u] ` φx ⇔ >,that an open subspace covers into a predicate (Axiom 4.2),∀x:[d, u]. φx ≡ Iφ(δd , υu ) ⇔ >.
R

Now, λφ. ∀x:[d, u]. φx is a term in the ASD λ-calculus of type ΣΣ , and, like all such terms,
it preserves directed joins. So if φ` x is directed with respect to ` : D then__∀x:[d, u].  φ` x ⇐⇒  ∀x:[d, u]. φ` x.
``

Restating this for general joins, we have∀x:[d, u]. ∃n:N . φn x ⇐⇒ ∃`:Fin(N ). ∀x:[d, u]. ∃n ∈ `. φn x,
where ` provides the finite open sub-cover.

48

Now, it is a little surprising that the Heine–Borel property is traditionally expressed using
finite open sub-covers, when a very common situation in analysis is that the cover is indexed by
the real numbers, which are directed. In this case, just one member of the family covers, and wehave uniform values, for example∀x:[d, u]. ∃δ > 0. φδ x ⇐⇒ ∃δ > 0. ∀x:[d, u]. φδ x,
so long as φ is contravariant in the sense that δ ≤  ` φ ⇒ φδ .

Warning 10.11 Our “∃` : Fin(N )” and ∃δ > 0 do not have the same strength as they do in otherconstructive systems. The computational implementation only produces ` or δ in the case where
the predicate (is provably true and) has at worst variables of type N (Remark 3.5). In particular, if
the predicate φ (and maybe even the bounds d and u) are expressions with real-valued parameters,neither δ nor even the length of the list ` can be extracted as functions of these parameters.
Lemma 10.12 The open interval (0, 1) is not compact.
Proof By Definition 6.10 for 0 < x,x : (0, 1) ` > ⇔ ∃q:Q. 0 < q < x,where ∃ is directed, so if (0, 1) were compact we could interchange the quantifiers, but> ⇐⇒ ∀x:(0, 1). ∃q > 0. q < x ⇐⇒ ∃q > 0. ∀x:(0, 1). q < x ⇐⇒ ⊥.

11

Arithmetic

Real arithmetic is a case where familiarity breeds contempt. Most of the issues that we need toconsider are extremely well known as folklore, but we do not know of a published account thatconsiders them all and gives the details in a coherent form that is suitable for us. See [TvD88,
p260] for a metrical approach involving 2−n , but our paper is about Dedekind cuts and intervals,
which are fundamentally order -theoretic ideas.
Dedekind himself considered addition and square roots but not multiplication [Ded72]. Evenin the classical situation, the proof that the positive and negative reals form a commutative ringor field involves either an explosion of cases or considerable ingenuity. One ingenious solution isJohn Conway’s definition of multiplication [Con76, pp.19–20], but we shall not use it.
Working with intervals instead of numbers makes this problem worse, whilst its usual solution— case splitting — is unacceptable, at least for R, in constructive analysis [TvD88, §5.6], topos
theory [FH79] [Joh77, §6.6] or ASD.
On the positive side, general continuity will relieve us of the burden of checking the arithmetic
laws, and in particular the case analysis in R. However, (Scott) continuity is only applicable after
we have verified an order-theoretic property of discrete rational arithmetic (cf. Proposition 7.13).
In Q we can and do use case analysis.
For reasons of space we omit the multiplication sign (×) in the usual way. Juxtaposition
may therefore denote either multiplication or function application, but our alphabetic conventions
distinguish them: ab with two italic letters is multiplication, whilst φa with a Greek letter isapplication. Despite the weight of tradition, we use p instead of  for a small positive tolerance,saving (δ, υ) and (, τ ) for the arguments of an arithmetic operation on cuts, with result (α, σ).
As usual, multiplication and λ-application bind more tightly than <, which is tighter than ∧ .
Axiom 11.1 Q is a discrete, densely linearly ordered (Definition 6.1) commutative ring.
49

There is a unique “inclusion” map Z ⊂ Q that preserves and reflects =, <, 0, 1, +, − and ×.
Axiom 11.2 Q obeys the Archimedean principle, for p, q : Q,
q > 0 =⇒ ∃n:Z. q(n − 1) < p < q(n + 1).
In view of Proposition 6.5, this cannot be a property of the order (Q, <) alone: it says how Z(i.e. the additive subgroup generated by q) lies within the order. We isolate our use of this principle
in Propositions 11.15 and 12.7, in the hope that some future development may avoid it altogether(Remark 12.13).
Remark 11.3 We do not ask that Q be a field, with (exact) division, because we have in mind
the ways in which it might be represented computationally: the axioms ought at least to allow
the dyadic and decimal rationals as examples. We could weaken the properties of addition andmultiplication on Q still further, since (in Example 11.9 and Proposition 12.3) we shall only use
them in the form of the four ternary relations
a<d+e

a<d×u

u+t<z

u × t < z,whose axiomatisation we leave to the interested reader. Such a person may be an interval analyst
or programmer who wants to use ASD to obtain mathematically provable results from the floating
point arithmetic that is built in to computer hardware [Ste85].
Whilst the likely applications have it, we do not actually even need to assert division by 2 asan axiom:
Lemma 11.4 There is an approximate half , h : Q, with 0 < h + h < 1.
Proof

Let a, h : Q with 0 < a < 1 and 0 < h < min(a, 1 − a).



Since the operations of arithmetic take two arguments, and its equations involve (up to) threevariables, our first task is to define the objects R2 and R3 . By Rn here we simply mean the
product of 2, 3, . . . copies.
Proposition 11.5 The product spaces Rn exist, and they are overt, with ∃Rn = ∃Qn .
Proof

Axiom 4.1 gives product types, and by Lemma 9.1 the quantifiers are given by∃(x, y):R2 . φ(x, y)≡∃x:R. ∃y:R. φ(x, y)⇔∃x:Q. ∃y:Q. φ(x, y) ≡ ∃(x, y):Q2 . φ(x, y).

Remark 11.6 Now we have a diagram that combines those in Remarks 2.13 and 6.9,
- S×2
- R2- - (ΣQ × ΣQ )2
Q2
- Σ
..
..
..
..
..
∗
~
..
..
..
?
.?
?
- S
Q
Q
R
Σ × ΣQ- Σ
where - - denotes an equaliser and S ≡ Q + Q + 1 + 1 + Q × Q + Q × Q.

50

This means that a term of type R2 is a pair of solutions of equations, defining a pair of cuts
or a “Dedekind cross-hair”, i.e. a division of the rational plane into quadrants. R2 is, in fact, aΣ-split subspace [B], though the splitting I2 is not simply the square of that for R. But that does
not matter, as we shall not need it anyway.
Q

Q

Q

Q

Exercise 11.7 By analogy with Proposition 2.15, find I2 : ΣR×R  ΣΣ ×Σ ×Σ ×Σ .
Remark 11.8 The plan, for each arithmetic operation ∗ (+ or ×), is(a) first to define some operation ~ on ΣQ × ΣQ that extends the given operation ∗ on therationals, in the sense that the rectangle above commutes, i.e. for each q, r : Q,
(δq , υq ) ~ (δr , υr ) = (δq∗r , υq∗r ) : ΣQ × ΣQ ;(b) then to show that (δ, υ) ~ (, τ ) is a Dedekind cut whenever (δ, υ) and (, τ ) are (so thecomposites R2 ⇒ ΣS above are equal), thereby filling in the dotted arrow above;(c) and finally to verify the usual laws of arithmetic for the extended operations.
Classically, Ramon Moore has already done the first of these tasks, but we need to take accountof the more general intervals that exist constructively (Remarks 2.3f). Recall from Propositions
7.12f that the intervals with (rational) endpoints provide a basis in the sense of domain theory,and that we may extend a predicate φ(d, u) to Φ(δ, υ) such that Φ(δd , υu ) ⇔ φ(d, u) so long as φis rounded, in the sense thatφ(e, t) ⇐⇒ ∃du. (d < e) ∧ (t < u) ∧ φ(d, u).
This condition may easily be generalised to an n-ary operation, but that would lead to anotherexplosion of symbols and cases. It is therefore wise to consider the arguments and the bounds one
at a time, which is enough.
Example 11.9 Consider the bounds a, z on addition of a fixed rational interval [e, t], soφ(d, u)≡a < [d, u] ⊕ [e, t] < z≡

a < d + e ∧ u + t < z.

Then this condition requires a < d + e ⇔ ∃d0 . (d0 < d) ∧ (a < d0 + e), for which we choose d0 witha − e < d0 < d, using subtraction and interpolation, and similarly for the upper bound.

Notation 11.10 For (δ, υ), (, τ ) : ΣQ × ΣQ , let(δ, υ) ⊕ (, τ )≡λa. ∃de. (a < d + e) ∧ δd ∧ e,
λz. ∃ut. (u + t < z) ∧ υu ∧ τ t .

Remark 11.11 It’s worth spelling out the condition in Proposition 7.13 once more in interval
notation. Write x for (the name of) an interval with rational endpoints [x, x], andxby≡[x, x] ⊂ (y, y)≡y<x ∧ x<yfor the strict containment relation that relates the basic compact subspace [x, x] to the basic open
one (y, y), cf. [K]. (Beware that b corresponds to  in the bounded interval predomain IR, which
is a continuous dcpo.) Then the condition for ~ to be well defined isx ~ y b w ⇐⇒ ∃x0 y0 . x b x0 ∧ y b y0 ∧ x0 ~ y0 b w.

51

Note that ∃ here ranges over the names of the intervals, i.e. over {(d, u) | d ≤ u} ⊂ Q2 , which isa discrete space, not over the domain IR, since b is not defined there as an ASD predicate in thesense of Axiom 4.2, but see [G, § 11].
Since it is only required to compute x~y to the limited precision w, it is standard programming
practice to use less precise versions x0 and y0 of x and y in this way, thereby saving space and hence
time.
Using roundedness, Proposition 7.12 extends Moore’s operations to general intervals by(δ, υ) ~ (, τ ) ≡ (α, σ),

whereαw ∧ σw ≡ ∃xy. δx ∧ υx ∧ y ∧ τ y ∧ x ~ y b w.

Turning to stage (b) of the plan in Remark 11.8, we have to check that each formula that
we introduce for an operation actually gives rounded, bounded, disjoint and located pairs (α, σ).
Roundedness and boundedness follow immediately from the form of the definition that we havejust given. We also get disjointness for free:
Lemma 11.12 Let α, σ : Rn ⇒ ΣQ be “disjoint” on Qn , in the sense thata, z : Q, ~q : Qn ` α~qa ∧ (z < a) ∧ σ~qz ⇒ ⊥.
Then they are also disjoint on Rn in the same sense, cf. Proposition 9.5.
Proof By Proposition 11.5, α~xa ∧ (z < a) ∧ σ~xz ⇒ ∃~q. α~qa ∧ (z < a) ∧ σ~qz ⇒ ⊥.

Lemma 11.13 Addition (Notation 11.10) takes intervals (i.e. rounded, bounded and disjoint
pseudo-cuts) to intervals, ⊕ : IR × IR → IR.
Proof (δ, υ) ⊕ (, τ ) is rounded by transitivity and interpolation in (Q, <), keeping the samed, e, u, t. It is bounded because (δ, υ) and (, τ ) are bounded, and by extrapolation in (Q, <). It isdisjoint by the previous Lemma, but more directly,∇ (δ, υ) ⊕ (, τ )≡ ∃azduet. δd ∧ υu ∧ e ∧ τ t ∧ (u + t < z < a < d + e)⇒≡(∃du. δd ∧ u < d ∧ υu) ∨ (∃et. e ∧ t < e ∧ τ t)∇(δ, υ) ∨ ∇(, τ ) ⇔ ⊥since u + t < d + e ⇔ (u − d) + (t − e) < 0 ⇒ (u < d) ∨ (t < e).

Remark 11.14 Locatedness always seems to be the most difficult step, because we need to
calculate the result arbitrarily closely. Recall that we defined this in a purely order-theoretic way
in Definition 6.8, namely d < u ⇒ δd ∨ υu.
However, to prove this property of a sum, we shall need a stronger hypothesis on the summands.
This is actually the version of locatedness that most accounts of Dedekind cuts use, except that
we allow the tolerance p to be any positive element of Q, not just 2−n for n : N.
It is not difficult to see the necessity of the stronger hypothesis for what we’re trying to achieve,
namely that Q is to be dense in a Dedekind-complete Abelian group R. In this situation, for anyx ≡ (δ, υ) : R, there must be d, u : Q with x − 21 p < d < x < u < x + 12 p. This is the (apparently
essential) use of the Archimedean principle, to which we shall return in Remark 12.12.
Proposition 11.15 Any cut (δ, υ) is arithmetically located , i.e. for p : Q,
p > 0 =⇒ ∃et:Q. δe ∧ υt ∧ (0 < t − e < p).
Conversely, if (δ, υ) is rounded and arithmetically located then it is bounded and located.
52

Proof By boundedness, δd ∧ υu for some d < u : Q. Then the Archimedean principle gives somek : N with u − d < khp, where 0 < h + h < 1 by Lemma 11.4. So qj ≡ d + jhp satisfy
q0 ≡ d < q1 < q2 < · · · < qk−1 < qk > u,
to which we may apply Lemma 6.16, as (δ, υ) is order-located with δq0 and υqk . This givesδe ∧ υt ∧ (t − e < p), where e ≡ qj , t ≡ qj+2 and t − e = 2hp < p, for some 0 ≤ j ≤ k − 2.
Conversely, given d < u, let e, t : Q with t − e < u − d such that δe, υt, so (δ, υ) are bounded.
By locatedness of < (Lemma 6.2), e < d ∨ t < u, so δd ∨ υu by roundedness.
Lemma 11.16 Addition takes cuts to cuts.
Proof Given a < z, we use arithmetic locatedness of one summand, (δ, υ), with p ≡ z − a, togive d, u : Q such that δd, υu, d < u and (u − d) < (z − a). Since a − d < z − u, by interpolation
there are e, t : Q with a − d < e < t < z − u, so a < d + e and u + t < z. By order locatedness ofthe other summand, e ∨ τ t, so we have shown that∃deut:Q. (a < d + e) ∧ δd ∧ (e ∨ τ t) ∧ (u + t < z) ∧ υu.
This implies that (α, σ) is order-located, i.e.
∃de. (a < d + e) ∧ δd ∧ e ∨

∃ut. (u + t < z) ∧ υu ∧ τ t .

Exercise 11.17 Show directly that(a) (δq , υq ) ⊕ (δ, υ) is order-located iff (δ, υ) is, for any q : Q; and(b) if (δ, υ) and (, τ ) are both arithmetically located then so is their sum.

In the final step (c) of Remark 11.8, topology plays to our advantage, particularly in ASD,
where all definable maps are automatically continuous. Once we have thought of a definition for
the extended operations, and verified that they have real results (i.e. cuts), the laws of arithmetic(both equations and inequalities) transfer automatically from Qn to Rn .
Lemma 11.18 For f, g : Rn ⇒ R,
if ~q : Qn ` f (~q) ≤ g(~q) : R
Proofthen ~x : Rn ` f (~x) ≤ g(~x) : R.

In traditional notation, since R is Hausdorff and f, g are continuous, the subspaceC ≡ {~x : Rn | f (~x) ≤ g(~x)} ⊂ Rn

on which the laws actually hold is closed; on the other hand, Qn ⊂ Rn is dense, whilst Qn ⊂ Cby hypothesis, so C = Rn . In ASD, C is co-classified by θ, whereθ(~x) ≡ f (~x) > g(~x),

and θ(~x) ⇒ ∃~q. θ(~q) ⇔ ⊥by Proposition 11.5, so θ = ⊥.

Proposition 11.19 R is an ordered Abelian group.



53

12

Multiplication

We would like to develop multiplication in a way that follows addition as closely as possible. Inthat case, Example 11.9 showed that the extension of the Moore operation is well defined, andLemma 11.16 that it preserves locatedness. The first of these tasks is complicated for multiplication
by negation and intervals, including the back-to-front ones (Remark 2.20):
Lemma 12.1 Kaucher multiplication 3 [a, z] ≡ [d, u] ⊗ [e, t] is defined by[d, u] ⊗ [e, t]
0≤e

e≤0

d≤0
u≤0
u≥0

0≤d
u≤0
u≥0

0≤t

[ dt, ue]

[ dt, ut] [ de, ue][ de, ut]t≤0

[ ut, ue][0, 0][q, p][ de, dt]

0≤t

[ dt, de][p, q][0, 0][ ue, ut]t≤0

[ ut, de][ ue, de] [ ut, dt][ ue, dt]

where p ≡ min(dt, ue) ≤ 0 and q ≡ max(de, ut) ≥ 0. It agrees with ordinary multiplication in Q
when d = u and e = t, and with Moore’s operation (Definition 2.3) when d ≤ u and e ≤ t. Also,a is a monotone function of d and e and an antitone one of u and t, and vice versa for z.
Even though this is rather complicated, we can break it up into small pieces:Lemma 12.2 The following functions are defined on the ascending reals, R:(a) constants;(b) multiplication by q ≥ 0: δ 7→ λa. ∃d. δd ∧ (a < dq);(c) minimum, min(δ, ) ≡ λd. δd ∧ d;(d) maximum, max(δ, ) ≡ λd. δd ∨ d; and(e) addition, δ ⊕  ≡ λa. ∃de. δd ∧ e ∧ a < d + e.
There are similar functions on R, and negation interchanges them.

Proposition 12.3 Kaucher multiplication provides a map(ΣQ × ΣQ ) × (ΣQ × ΣQ ) −→ (ΣQ × ΣQ )that extends multiplication on Q in the sense of Remark 11.5. It also preserves roundedness,boundedness and disjointness.
Proof Looking at pairs of entries in the table, we observe, for example, that a depends on d for
fixed e, t and u in at worst a piecewise linear way. The pieces are either constant or multiplication
by some q ≥ 0 (or q ≤ 0 in the order-reversing cases), and they are combined using min or max.
These functions are rounded on Q, or defined R → R etc., by the previous lemma, and it’s enoughto check this componentwise.
Alternatively, we may follow Example 11.9 directly:
a < [d, u] ⊗ [e, t] < zmeans

a < 0, de, dt, ue, ut , min(dt, ue), max(de, ut) < z

in various cases, in each of which there is d0 < d, e0 < e, t < t0 or u < u0 with the same property.
3 We computed the table ourselves with the help of Chris Stone, before we obtained a copy of [Kau80], and thenchecked that they agree.

54

Hence we have a map (R × R) × (R × R) → (R × R), but R and R are retracts of ΣQ , so we
also have one (ΣQ × ΣQ ) × (ΣQ × ΣQ ) → (ΣQ × ΣQ ) that preserves roundedness.
Since the Kaucher product of intervals with rational endpoints, i.e. as in the table, is finite,
it preserves boundedness of general intervals. Similarly, since it agrees with Moore’s operation
for disjoint intervals, it also preserves disjointness of general intervals. Beware, however, that the
product of a forward and a backward interval may be either way round, depending on the widthsof the arguments.

Exercise 12.4 Use the argument so far to show that R is a Q-module, cf. [Joh77, §6.6].
Remark 12.5 The final task is to show that products are located, cf. Lemma 11.16. Let’s lookat this from a programmer’s perspective again. If we are asked to calculate xy to precision 0 <p < 1, we need to decide how precisely to compute the factors x and y. For addition, p/2 is fine(cf. Exercise 11.17(b)), but for multiplication,(a) if x and y are both small in magnitude, i.e. |x|, |y| < 1, then it suffices to find each of themto within p; but(b) if x is large (legally, if 0 < M < |x|, but we’re thinking of the situation where M is in the
millions), we need to find y correspondingly more precisely, to within p/M ;(c) similarly, if y is large then we need to know x more precisely.
Since we did not include division in the assumptions about Q, whereas we used subtraction
in Example 11.9, we have a difficulty in the construction of multiplication even for positive real
numbers. In any place-value representation, such as binary floating point, division may be performed as accurately as required, by first shifting the divisor by sufficiently many (n) places andthen dividing to give an integer quotient. Proposition 12.7 is the same idea in abstract form; inthe next section we shall show that this is enough to provide genuine division in R.
Lemma 12.6 Any linearly ordered ring Q is an integral domain, admitting cancellation:
if q > 0then bq = cq ⇐⇒ b = c and bq < cq ⇐⇒ b < c.

Proposition 12.7 Q has approximate division, for a, q, z : Q,
(a < z) ∧ (q > 0) =⇒ ∃m:Q. (a < mq < z).
Proof Either 0 < 4q < z − a or 0 < z − a < 8q.
In the first case, we may apply the Archimedean principle directly with the given q:
for some k, k 0 : Z,q(k − 1) < a < q(k + 1)

andq(k 0 − 1) < z < q(k 0 + 1).

Then 4q < z−a < q(k 0 +1)−q(k−1), so k < k 0 −2 by the previous lemma. Hence m ≡ k+1 < k 0 −1,
where m : Z ⊂ Q, has the required property.
In the second case, the Archimedean principle for 8q (as p) and z − a (as q) provides k : Z with
8q < 2n(z − a), and then 0 < k < 2n for some n : N. Let h satisfy 0 < h + h < 1 (Lemma 11.4).
Then
4q 0 ≡ 4qhn < khn (z − a) < (2h)n (z − a) < (z − a),for which the first case gives a < m0 q 0 = m0 qhn < z, so m ≡ m0 hn is the required approximate
quotient.
55

Returning to the question of locatedness, recall that we needed to strengthen this notion in
Proposition 11.15 in order to define addition. Curiously, we do not need to do this (or to apply
the Archimedean principle) again for multiplication.
Lemma 12.8 Any arithmetically located positive cut (δ, υ) : R is multiplicatively located :(0 < a < z) ∧ δ0 =⇒ ∃du:Q. (0 < d < u) ∧ δd ∧ υu ∧ (ua < dz),
where the last conjunct corresponds to u − d < p in Proposition 11.15.
Proof By roundedness of δ, let 0 < r : Q with δr. By approximate division in Q, let 0 < p : Q
with 0 < zp < r(z − a). By arithmetic locatedness, let 0 < d < u : Q with δd ∧ υu ∧ (u − d < p).
Since we have δr ∧ υu, disjointness of (δ, υ) gives r < u, so z(u − d) < zp < r(z − a) < u(z − a).
Hence ua < zd as required.

Lemma 12.9 The product of an arithmetically located positive cut (δ, υ), i.e. such that δ0, withany cut (, τ ) is another cut (α, σ), cf. Lemma 11.16.
Proof Suppose that 0 < a < z. By multiplicative locatedness of (δ, υ), there are 0 < d < u withδd ∧ υu ∧ (ua < dz). Then, using approximate division by du, there are e, t with
au < due < dut < zd.
So a < de, e < t and ut < z by Lemma 12.6, whilst e ∨ τ t by order-locatedness. Hence(∃de. a < de ∧ δd ∧ e) ∨ (∃ut. ut < z ∧ υu ∧ τ t) ≡ αa ∨ σz.
More generally, given a < z, either• 0 < z, in which case there is some a0 with 0, a ≤ max(0, a) < a0 < z, so αa0 ∨ σz by theforegoing argument, and hence αa ∨ σz since α is lower; or• a < 0, where we apply the previous case to −z < −a, (, τ ) and (α, σ).
It only remains to prove locatedness of the product of two numbers that are both small. Notethat we can bound a product away from zero iff we can do so for both factors, and in that casethe previous result applies. The point of the fifth case below is therefore to constrain the productto be near to zero.
Lemma 12.10 The product of any two real numbers (cuts) x, y : R is another cut.
Proof

If a < z then a < 0 ∨ 0 < z, so 0 < m ≡ max(z, −a) and(x > 0) ∨ (x < 0) ∨ (y > 0) ∨ (y < 0) ∨ (|x| < 1 ∧ |y| < m).

It only remains to consider the last of these five cases, which is itself a disjunction because of thedefinition of < max (Proposition 9.8). Then essentially|x| < 1 ∧ |y| < m=⇒a < −|y| < xy∨xy < |y| < z.

We need to explain these inequalities in terms of cuts x ≡ (δ, υ) and y ≡ (, τ ):|x| < 1≡a < −|y| ≡a < xy⇐−1 < x < +1 ≡ δd ∧ υu,whered ≡ −1,u ≡ +1∃et. e ∧ τ t ∧ (a < e) ∧ (a < −t)∃duet. δd ∧ υu ∧ e ∧ τ t ∧ a < min(de, dt, ue, ut).

56Proposition 12.11 R is an ordered commutative ring.



We shall use division in the next section to prove that R is Archimedean, but let us consider
very briefly the necessity of that hypothesis on Q.
Remark 12.12 There are Cauchy-complete ordered fields with infinitesimals but, classically, any
Dedekind -complete Abelian group must be Archimedean. This is because the setsD ≡ {d | ∃n:N. d < n}and U ≡ {u | ∀n:N. n < u}form a Dedekind cut that is located only in the weaker order-theoretic sense: since every u − d isinfinite, (D, U ) is not arithmetically located.
The significance of the Archimedean property in Greek mathematics was recognised by Otto
Stolz [Sto83]. He coined the name because, although the principle had been used “implicitly” by
Eudoxus and Euclid, Archimedes had stated it as an Axiom. (He had also made far deeper useof it, in his Method, but Stolz was writing before the discovery of the most important Archimedes
codex.)
Stolz also gave this argument that Dedekind completeness implies the Archimedean principle[ibid., p. 511]. His result was disputed by his contemporaries, possibly because of its context in thedebate at the time over the axiomatics of Euclid, but there is also a lot of extraneous discussionthat makes one wonder whether he fully understood Dedekind completeness. However, we consider
that his proof is valid, because it includes the two key points, namely the construction of the limitof an increasing sequence as the cut (D, U ), and the problem with the value (D, U ) − 1. The
constructive least upper bound principle and arithmetic locatedness are also “implicit” in thispaper.
Remark 12.13 What does this argument say about Conway’s number system? Recall that it isa proper class. Although the class D above is equivalent as a left cut to the set N, the class U
cannot be expressed as a right cut, so {D | U } is not a legitimate Conway Number — he calls it
a gap [Con76, p. 37].
The argument also fails in ASD, for an analogous reason: U is not definable in the calculus as
an open subspace. The point is really that the space D of finite numbers is overt, as it is given by
an existential quantifier, or as the numbers for which repeated decrementation terminates. On theother hand, U consists of infinite or non-terminating numbers, so it is the canonical example of anon-overt subspace in recursion theory. Since U is not overt, it’s not open, so it’s not defined bya predicate. Hence D is not closed or compact, so we do not expect [J] to provide its supremum.
We do not know whether there is in fact a Dedekind-complete but non-Archimedean “realline” in ASD. This is a difficult but intriguing problem in recursion theory. Careful study ofJohn Conway’s construction may yield a recursive analogue (when this conjecture was put to him,
he considered it plausible). The principal difficulty arises from the alternating quantifiers in thedefinition of <, as the arithmetic operations are clearly constructive [Ros01]. Even if such a model
does exist, Stolz’s argument would still show that the sequence 0, 1, . . . , has no limit: any infinite
element ω is “inaccessible” from finite values.
Such an object could, of course, be rather useful to develop differential calculus in a “nonstandard” way [Koc06, Rob66]. It would also illustrate the importance of overtness very clearly.
Here we have simply “left the door open” to such a possibility, by using approximate division andarithmetic locatedness in the proof, instead of the Archimedean principle itself.
Theorem 12.14 Let Q be any linearly ordered field (or commutative ring with approximate division) for which every Dedekind cut is arithmetically located. Then these cuts form a commutative
ring.

57

13

Reciprocals and roots

Arithmetic, of course, provided one of the principal reasons for introducing Dedekind cuts in thefirst place, namely the solution of (algebraic and other) equations. Equations involving generalcontinuous functions may be solved using the Intermediate Value Theorem, which we prove for
ASD in [J].
In this section we present a simpler technique that manipulates Dedekind cuts directly. Thisis sufficient to define the inverse of a strictly monotone function, for example to find cube roots.
However, it is more natural to present the method symmetrically in the given function and its
inverse, and then x 7→ x5/3 , exp and log are equally simple examples. A particular problem of thiskind is then formulated as a pair of binary relations. Anyone with a little knowledge of lattice or
category theory will recognise this situation as an adjunction, or rather a pair of them.
Definition 13.1 A strictly monotone graph Q1 ↔ Q2 between dense linear orders without
endpoints (Definition 6.1) is a pair (<7 , 7<) of binary relations that satisfy∃b. a <1 b <7 x ⇔∃b. x 7< b <1 a ⇔∃x. a <7 x 7< b ⇔a <7 xx 7< aa <1 bx <2 y⇔ ∃y. a <7 y <2 x
⇔ ∃y. x <2 y 7< a⇔ ∃a. x 7< a <7 ywhere a, b : Q1 and x, y : Q2 . These objects could, for example, consist of just positive rationals,
or carry the opposite of the usual order. Let R1 and R2 be their Dedekind completions. Semicontinuous functions may be encoded in a similar way, but using just one of the two relations.
Proposition 13.2 Any strictly monotone graph defines inverse functions R1 ∼= R2 byf (δ, υ) ≡ (λe. ∃d. e <7 d ∧ δd,λt. ∃u. u 7< t ∧ υu)≡ (λd. ∃e. d 7< e ∧ e,

λu. ∃t. t <7 u ∧ τ t),g(, τ )for which a <7 x ⇐⇒ a <1 f x ⇐⇒ ga <2 x and x 7< a ⇐⇒ f x <1 a ⇐⇒ x <2 ga.
Proof The first four axioms make f (δ, υ) and g(, τ ) rounded if (δ, υ) and (, τ ) are. The othertwo transfer boundedness, disjointness and locatedness, and also make the maps inverse.

We can use this to define reciprocals and roots, but since their domains are restricted andreciprocals reverse the order, we must modify Q and R before using them in the Proposition.
Lemma 13.3 Let Q be a linearly ordered ring that has approximate division, and let Q1 ≡ Q2 ⊂ Q
be its open subspace of positive elements. Thena <1 b ≡ a < b,x <2 y ≡ x > y,a <7 x ≡ ax < 1,x 7< a ≡ 1 < axdefine a strictly monotone graph Q1 ↔ Q2 .
Proof Approximate division provides the six conditions∃b. a < b ∧ bx < 1 ⇔∃b. 1 < bx ∧ b < a ⇔∃x. ax < 1 < bx ⇔ax < 1
1 < ax
a<b
x>y

⇔
⇔
⇔

∃y. ay < 1 ∧ y > x∃y. x > y ∧ 1 < ay∃a. ay < 1 < ax,

in particular 0 < a < b ⇒ ∃x. a < abx < b ⇒ ∃x. bx > 1 > ax.
Theorem 13.4 R is an ordered field, in which x−1 is defined for x 6= 0 by(δ, υ)−1≡λd. ∃u. υu ∧ ((du < 1 ∧ δ0) ∨ (1 < du ∧ d < 0)),
λu. ∃d. δd ∧ ((du < 1 ∧ u > 0) ∨ (1 < du ∧ υ0)) .
58

In the strictly positive or negative cases this is respectively
λu. (u > 0) ∧ (∃d. δd ∧ du < 1)
λu. (u > 0) ∨ (∃d. δd ∧ 1 < du) .

λd. (d < 0) ∨ (∃u. υu ∧ du < 1),or

λd. (d < 0) ∧ (∃u. υu ∧ 1 < du),

Proof The previous two results define an involution on {x : R | x > 0}. If Q is a field then thisagrees with the reciprocal on Q and with Moore’s formulae (Definition 2.3) in the legitimate case0 < a ≤ b, where(δa , υb )−1 = (δ1/b , υ1/a )and(δ−b , υ−a )−1 = (δ−1/a , υ−1/b ).

Without assuming that Q is a field, (q , τq ) ≡ (δq , υq )−1 for q > 0 is given by q d ≡ (dq < 1) andτq u ≡ (1 < qu). The arithmetical laws follow from Lemma 11.18. The negative case is similar,
and we observe that the given formula combines the two cases.
Remark 13.5 We do not need to consider 0 this time, but since∃du. (δ, υ)−1 (d, u) =⇒ δ0 ∨ υ0,
the value in any illegitimate case, including 0−1 and (δ−1 , υ1 )−1 , is (⊥, ⊥). This denotes theinterval [−∞, +∞].
More generally, the reciprocal of a general (and possibly back-to-front) interval with endpoints
is given by[d, u]−1
d<0
d=0
d>0
u < 0 [ u−1 , d−1 ] [u−1 , −∞] [+∞, −∞]u = 0 [−∞, +∞] [−∞, +∞] [+∞, d−1 ]u > 0 [−∞, +∞] [−∞, +∞] [ u−1 , d−1 ],illustrating the one-sided nature of Scott continuity: over d ≤ 0 for the ascending real number dand over u ≥ 0 for the descending one u.
Theorem 13.6 If Q is Archimedean then so is R.
Proof Given x, y : R with y > 0, put z ≡ x/y. Then z − 12 < d < z < u < z + 12 for somed, u : Q with u − d < 1. Then n − 1 < d < z < u < n + 2 by the Archimedean principle for Q,
whence either (n − 1)y < x < (n + 1)y or ny < x < (n + 2)y.

Lemma 13.7 Q has approximate roots in the sense that, for d, u : Q and 1 ≤ n : N,
(0 < d < u) ⇒(d < u)⇒∃x:Q. d < x2n < u∃x:Q. d < x2n+1 < u.

Proof These may be found in an Archimedean ordered commutative ring with approximate
division by an algorithm similar to Proposition 12.7, for which we cite Babylonian clay tablets as
the original source.
Alternatively, and without relying on the Archimedean principle, we may use the constructive
approximate intermediate value theorem, namely
f e < d < u < f t =⇒ ∃x:[e, t]. d < f x < u.
The usual proof is that the non-empty open subspacesD ≡ {x | f x < u}and59

U ≡ {x | d < f x}

cover the interval [e, t], and so must intersect. This is one of the ways of saying that the realinterval is connected , which we prove for ASD in [J]. As the intersection is open, it must containa rational.
The result is applicable to f x ≡ x2n when we putdif 0 < d < 1
u if 1 < u
e≡ 1
and
t≡
1
2 if u < 2
if
<
d
2
2
and to f x ≡ x2n+1 whenwe putd
if d < −1e≡−2 if − 2 < d


and

t≡

u if 1 < u
2 if u < 2.

Proposition 13.8 R has (2n + 1)st roots and [0, ∞) has 2nth roots, wherep
2n+1(δ, υ) ≡ λd. δ(d2n+1 ), λu. υ(u2n+1 )p+ 2n (δ, υ) ≡ λd. (d < 0) ∨ δ(d2n ), λu. (u > 0) ∧ υ(u2n ) .
In the illegitimate case,√−1 = 0.

Proof The strictly monotone graph is given by the relations (a < xm ) and (xm < a), wherem ≡ 2n or 2n + 1. If a < xm and 0 < x then, by m-fold application of roundedness of division,∃0 < y1 , y2 , . . . , ym < x. max(0, a) < y1 y2 · · · ym < · · · < y1 y2 xm−2 < y1 xm−1 < xm ,so a < y m , where 0 < y ≡ max(y1 , . . . , ym ) < x. Similarly if 0 < x and xm < a then ∃y > x. y m <a, whilst if m ≡ 2n + 1 and x < 0 then we switch the signs. Approximate roots provide thefifth interpolation property, and also the case x ≡ 0, since Q has decidable equality. The otherconditions are trivial.
Finally, we leave the interested reader to use this method to develop the exponential and−nlogarithm functions R  (0, ∞) with base b, using 0 < d < bk·2 < u.

14

Axiomatic completenessOur construction of the real line in ASD is finished. At any rate, we have found an object thathas all of the properties that we listed in Definition 1.1, so we shall now write R for it.
Are these axioms sufficient to characterise the reals? We shall show that any object R thatsatisfies 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 needit, 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 ofmaking 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 findthe limit of any Cauchy sequence as a Dedekind cut in [J].
We begin with the well known argument for the uniqueness of R 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 N → R, Z → R and60

j : Q → 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 : 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 : Z.
Proof First apply the Archimedean axiom to q ≡ u − d > 0 and p ≡ 2, giving m, n : Z with(m − 1)(u − d) < 2 < (m + 1)(u − d) < 2n (u − d).
Then use it again with q 0 ≡ 2−n , giving k : N withd < 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  R thatfixes Q, and preserves and reflects <.
Proof For x : R, consider δx , υx : ΣQ , defined by δx d ≡ (d <R x) and υx u ≡ (x <R u). Since
Q → R preserves and reflects order, for x : Q, 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 locatedin the sense of Definition 6.8. Boundedness follows directly from the Archimedean principle, androundedness by Lemma 14.2.
Hence (δx , υx ) is a Dedekind cut of Q, and we have defined a map ` : R → R. Using Lemma 14.2
for R again, together with Definition 6.10 for <R ,x <R y ⇐⇒ ∃q:Q. x <R q <R y ≡ ∃q:Q. δx q ∧ υx q ≡ `x <R `y,so the order relations <R and <R 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 theprevious result is an isomorphism. Definition 1.1 therefore characterises R uniquely up to unique
isomorphism.
Proof Members of R are by definition Dedekind cuts of Q, 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 ∼= R from
the principles of ASD, without assuming Dedekind completeness. The arguments are essentiallythose that led up to the formulation of E in Section 2.
Proposition 14.5 For x : R and φ : ΣR , φx ⇐⇒ ∃du. (d < x < u) ∧ ∀y:[d, u]. φy.
Proof Whilst Corollary 10.8 has already shown that the Dedekind reals R (as we have constructed them) satisfy this property, we claim here that it also follows from Definition 1.1. Thisis proved in detail in [J]. The key point is that, since [−1, +1] ⊂ R is compact, Hausdorff andtotally 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 ∃Q , as in Theorem 9.2.
61

ProofBy Proposition 14.5 and Lemma 14.2,∃x:R. φx ⇒ ∃dux:R. (d < x < u) ∧ ∀y:[d, u]. φy ⇒ ∃q:Q. φ(jq) ⇒ ∃x:R. φx.

Proposition 14.7 Σ` : ΣR ∼= ΣR .
Proof As in Proposition 2.15, we define, for φ : ΣR ,Q

Q

Iφ ≡ λδυ:ΣQ . ∃d < u:Q. δd ∧ υu ∧ ∀y:[d, u]. φy : ΣΣ ×Σ ,using the Heine–Borel property that we have assumed for [d, u] ⊂ R. ThenIφ(`x) ≡ Iφ(δx , υx ) ≡ ∃du. (d <R x <R u) ∧ ∀y:[d, u]. φy ⇔ φx,in which d and u may be chosen from either Q or R, by Lemma 14.6, and we recognise the formulain 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
Q
Q
in ASD. Hence ΣR and ΣR split the same idempotent E on ΣΣ ×Σ , cf. Remark 5.2, so they are
isomorphic.

The topology on R is therefore unique, when we assume the Heine–Borel property but notnecessarily 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 R.
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 R
as a base type, together with (all of) the structure of Definition 1.1.
In Axiom 4.24 we showed how descriptions for N may be formulated in a type-theoretic style bygiving the introduction rule for “the”. In this, the elimination, β- and η-rules are given by singletonand substitution, and there is a normalisation theorem [A, §8]. It is easy to overlook the key roleof equality (=) in this — it is to descriptions as application is to λ-abstraction and membershipis to set-formation. Since R is Hausdorff and not discrete, we cannot base an analogous treatmentof it on equality. We could use inequality (6=) (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 andelimination rules for the type R.
(a) R-introduction: given a cut (δ, υ) : ΣQ × ΣQ , we introduce a real number cut(δ, υ) : R;(b) R-elimination: given a real number a : R and rationals d, u : Q, we eliminate a in favour of(d < a), (a < u) : Σ, along with the other rules concerning the order <;(c) R-beta: δd ⇔ d < cut(δ, υ) and υu ⇔ cut(δ, υ) < u ;(d) R-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.

62

Theorem 14.11 R 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 tothe 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 arealso 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 R.
(a) If we are given a term a of type R, we use the R-η-law to wrap it in a cut:a = cut (λd. d < a, λu. a < u).
(b) Any cut that occurs as a proper sub-term of this is itself of type R, 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:Q. δ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 translationthat has the effect of replacing continuous variables by intervals, which is what programmers do
anyway, but it is justified formally in [K].
As R is no longer one of the types that are generated from N using powers and Σ-split subspaces,
we need to show that it is sober, cf. Proposition 4.25(b) for N.
R

Lemma 14.13 If P : ΣΣ is prime then(δ, υ) ≡
λd. P (λx. d < x), λu. P (λx. x < u)is a Dedekind cut, with cut(δ, υ) = focus P , so(d < focus P ) ⇔ P (λx. d < x)and(focus P < u) ⇔ P (λx. x < u).

Proof The last part is equivalent to the definition of δ and υ. These are rounded and boundedbecauseP (λx. d < x) ⇔ P (λx. ∃e. d < e < x) ⇔ ∃e. d < e ∧ P (λx. e < x)and> ⇔ 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).
63

Exercise 14.14 Using 6= 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 thisin a compact Hausdorff space such as I, instead of R. The existence and uniqueness conditions forω to classify a co-singleton are then the duals of those in Axiom 4.24:⊥ ⇐⇒ ∀x:[0, 1]. ωxandx 6= y =⇒ ωx ∨ ωy.

Consider any function f : [0, 1] → R. Use the Heine–Borel Theorem to show that ωx ≡ ∃z. f z < f xsatisfies 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 6= y) =⇒ ∃z. (f z < f x) ∨ (f z < f y), cf. [Sch03]. This is the uniquenesscondition 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 6= w) ⇒(f w < f x).
Show that definition by co-description is equivalent to sobriety and Dedekind completeness,using the translationsω ≡ δ∨υandP φ ≡ ∃d < u. δd ∧ υu ∧ ∀x:[d, u]. φx.

Expressing any co-description ω as a Dedekind cut is a special case of the characterisation ofconnected subspaces of R in [J].
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 ∨.


15

Recursive analysis

Whether the closed interval is, or ought to be, compact in computable and constructive mathematics is a question that never ceases to be interesting. This is partly because compactness is suchan important property for a topological space to have, and partly because there are several schoolsof constructive and computable mathematics that disagree about the answer, each of which sets
up its own framework, differing slightly from all the others. The matter is made all the more confusing by the number of different definitions of compactness that have been given, even classically[Bou66, §I 9]. In this section we make a few observations about compactness of the closed interval
in ASD and how it relates to various other schools of computability.
Most urgently, we hear alarm bells ringing in the minds of recursive analysts. On the one hand,
we saw in Remark 3.4 that there is a model of ASD in which maps are precisely the computablemaps between computably based locally compact spaces. On the other, Section 10 proved thatthe closed interval is compact. If all functions are computable, then surely we should be able touse some enumeration of the definable points of the closed interval to show that it is not compact?
Remark 15.1 In Recursive Analysis, the closed interval [0, 1] can be shown not to be compact
by means of a singular cover , i.e. a countable cover by open intervals with rational endpoints
whose total length is bounded above by 21 . It can be shown that no finite sub-cover of a singularcover is a cover of [0, 1], see [TvD88, §6.4.3] or [BR87, §3.4]. Such covers exist in Recursive
Analysis [TvD88, §6.4.2] because of the formal Church’s Thesis CT0 [TvD88, §3.3.2], which statesthat every function N → N has a Gödel code. (With hindsight, it would have been more natural
to enumerate N → N⊥ , but this is the way in which CT0 is usually stated.) It follows that every64real number has a Gödel code, too. In classical recursion theory, a singular cover is described as acomputable enumeration of open intervals with rational endpoints of bounded total length which
effectively covers all computable reals.
Example 15.2 The closed interval may also fail to be compact for reasons that have nothing to
do with computability. The construction of the “Dedekind reals” R as the equaliser in Remark 6.9
can be done in any category with finite limits, certain exponentials and some mild assumptions
on ΣN , as in Section 4. An example is the category Dcpo of posets with directed joins andScott-continuous functions. Here the equaliser carries the discrete (“specialisation”) order, but inthis category the order determines the topology. The object R therefore also carries the discrete
topology, so ΣR is the powerset P(R) with the Scott topology, and the only compact subsets of
R are the finite ones. Hence the predicate [d, u] ⊂ U is not continuous in U . The formula inQ
Q
Proposition 2.15 gives an element of ΣΣ ×Σ for each U ⊂ R, but the function I is not Scottcontinuous, so it does not yield a sound interpretation of the ASD calculus (Warning 5.17).
Remark 15.3 One resolution of the abnormalities of Recursive Analysis that has been adopted
by several schools is that of relative computability, in which the maps are computable, but the
spaces are the classical topological ones, i.e. they have “all” points instead of just the computableones. Each space is also equipped with a “computability” structure, such as an enumeration ofbasic open sets, that is used to specify which continuous maps are computable. Examples are (onevariant of) Type Two Effectivity [Wei00], and computable equilogical spaces [Bau00]. Another isMartı́n Escardó’s synthetic topology of data types [Esc04], but beware that, whilst this is very
similar to the calculus in Section 4, it lacks the crucial monadic property of ASD (Section 5). In
all of these three settings, the closed interval is compact, the proof being the well known classicalone. In particular, Escardó stresses the need for “all” points, as compactness would fail in a purely
recursive version of his theory.
Remark 15.4 The sceptical pupil from the Russian School will not be so easily convinced, butwill press us on the structure of the syntactic term model of ASD, in which the objects are types
and the morphisms are the definable maps. Since everything is enumerable in such a model, one
might expect to obtain a singular cover, and so non-compactness of the closed interval. Indeed, byfollowing the usual construction, we could define a sequence of intervals with rational endpoints,(an , bn ), whose total length is bounded by 12 , and prove the meta-theorem that“if

` t : [0, 1]` ∃n:N. an < t < bn ”.

thenHowever, it does not follow that (an , bn ) covers [0, 1], by which we meanx : [0, 1] ` ∃n:N. an < x < bn ,because that would be to confuse a family of theorems about all definable closed terms t with asingle theorem containing a free variable x. In category theory, the calculus is said to be not well
pointed. Even though its morphisms are recursively enumerable, there are not enough of them
1 → R to cover the equaliser.
Example 15.5 As a final attempt to break compactness of the closed interval in ASD, we might try
to interpret it in a setting, such as Markov’s Recursive Mathematics, in which the formal Church’s
Thesis CT0 holds. A useful formulation of this is the category PER of partial equivalence relations
over Stephen Kleene’s first algebra [Kle45], or Martin Hyland’s larger effective topos, Eff [Hyl82].
We try to interpret ASD in PER or Eff in the natural way, using the universal properties ofN, products, equalisers and exponentials. For Σ we take the object of semidecidable propositions.
65

This yields a valid interpretation of the language and construction of Sections 4 and 6, so that theequaliser R in Remark 6.9 is perhaps a reasonable candidate for the “real line” in these worlds.
However, we do not have a sound interpretation of Σ-split subspaces, because the map I that
Remark 5.17 requires need not exist. In particular, the object ΣR does not have the properties of
the “Euclidean” topology, and the closed interval is not compact.
In PER, the formula in Proposition 2.15 does not define a morphism I because [d, u] ⊂ U is
not a completely r.e. predicate (in d, u and U ). In the internal language of Eff , the sub-expression∀x:[d, u]. x ∈ U is a term of type Ω but not Σ. Consequently, the formula defines a morphism I
Q
Q
Q
Q
from ΣR to ΩΣ ×Σ and not to ΣΣ ×Σ .
This situation is better documented for Cantor space:
Example 15.6 Richard Friedberg [Fri58] defined an effective operation on the set of total recursivefunctions N → N that is not the restriction of a recursive functional. See [Rog92, §15.3.XXXI]
for another account of this construction, which also works for the total recursive binary sequences
N → 2.
In the effective topos we can reformulate Friedberg’s example by saying that the topology ofN
2N (i.e. the object Σ2 ) is not the subspace topology induced by the inclusion 2N ⊂ 2N
⊥ . In thisN
topos, 2 is actually homeomorphic to NN , so neither of these spaces can be locally compact, andtheir topology is not the subspace topology of 2N⊥.
In the construction of 2N in ASD [L], on the other hand, the space 2N⊥ of partial functions fromN to 2 plays a role similar to that of IR in Sections 7–8, being a closed subspace of ΣN × ΣN . Then
2N ⊂ 2N⊥ is defined by a nucleus that satisfies both the ASD and localic definitions. The quantifier∀ that says that 2N is compact is obtained from this nucleus in a similar way to that for [d, u].
Escardó [Esc04] has shown how ∀ for 2N may be implemented as a program in Haskell. He
proved its correctness using relative computability (Remark 15.3), but this may also be done using
the monadic principle in ASD.
Remark 15.7 You may be left thinking that models of ASD are complicated, mysterious andhard to find. In fact, the calculus has interpretations in many kinds of classical or constructive
set, type or topos theory. It is more accurate to say that these interpretations can be based onother foundational systems, because we obtain a model of our calculus by doing a construction on
top of a system with weaker properties. In other words, whilst the direct interpretation in PER
and Eff in Example 15.5 does not work, a slightly more involved one does.
Theorem 15.8 Let (C, Σ) be a model of the axioms in Section 4, in particular with products andpowers ΣX . Suppose also that idempotents split in C. Then Aop is a model of ASD, where A isthe category of Eilenberg–Moore algebras for the monad arising from Σ(−) a Σ(−) [B].
Remark 15.9 Any category that results from this construction contains (the sober objects of) theoriginal one (and more), and the embedding preserves Σ(−) . However, many other constructions
are not preserved, important examples being, of course, Cantor space and the Dedekind reals as
we have defined them.
Whilst these objects may have had undesirable properties in the original structure, their analogues in the new one turn out to behave as the mainstream mathematician would expect. The new
objects are by definition the exponentials, equalisers, etc. for the same data in the new category,whilst (the images of) the old objects are relieved of their former duties.
This construction can be carried out for all of the well known models of computable mathematics, including Recursive Mathematics, domain-theoretic PER models and Type Two Effectivity.
For example, when we apply it to the category CL of continuous lattices and Scott-continuous
66

functions, we obtain the category LKLoc of locally compact locales. It would be interesting andfruitful to do this in detail for the other cases, and, in particular, to compare their collections ofovert objects.
On the other hand, these models have other significant properties besides those given in Section 4, which it may not be easy to reproduce in the new category. For example, CL is cartesianclosed, but LKLoc is not.
Theorem 15.10 Over the effective topos Eff there is a sheaf topos Eff A that has a model Aopof ASD as a reflective subcategory.4
Proof There is an internal category C ∈ Eff of PERs that is weakly equivalent to a reflective
subcategory C ⊂ Eff of Ω¬¬ -discrete objects [HR90]. (This situation is a peculiarity of realisability
toposes, and the weakness of the equivalence is essential: Peter Freyd observed in the 1960s that,classically, any small complete category is a lattice [Tay99, Example 7.3.2(k)], and this extends toGrothendieck toposes.)
Now let A be the internal Eilenberg–Moore category for the monad over C within Eff , and A
the external one over C (or equivalently over Eff ). Then by Theorem 15.8, both Aop and Aop aremodels of ASD.
Since Aop is an internal category, i.e. a small one in classical language, we may form thesheaf topos Eff A . But Aop and Aop are weakly equivalent to each other, and therefore to a fullsubcategory of Eff A , by the Yoneda embedding. On the other hand, Aop is also totally cocomplete(see [Kel86, Corollary 6.5] in particular, but the theory was developed in [SW78, Str80, Tho80,
Woo82]), so this full subcategory is reflective in Eff A .
Remark 15.11 Altogether, it is often very interesting (and not just for gladiatorial reasons) toinvestigate the conflicts between one view of the mathematical world and another, because theresolution of such conflicts often leads to powerful applications. It is therefore perhaps a little
disappointing that we have not managed to bring ASD into confrontation, let alone conflict, withsingular covers and similar recursive phenomena.
The explanation is simply that, as we have shown, the quantifier ∀ that encodes compactnessof the closed interval is inter-definable with the map I that we introduced classically in Proposition 2.15. The systems in which the Heine–Borel theorem is true are exactly those in which I isdefinable. In any particular system, there may be some difficult proof of the existence of ∀ and I,
but in ASD, the latter is given, essentially axiomatically, by the monadic principle.

16

Conclusion

We showed in Section 14 that Definition 1.1 is complete in the sense that it characterises R
uniquely up to unique isomorphism of its structure.
Beware that, just as in the rest of the paper, this is a theorem within the calculus, about eachmodel of ASD. In particular, our axioms isolate R within the classical model (Definition 3.1), where,of course, we intend the arithmetical operations and all other terms to be continuous. Maybe you
believe that the real line satisfies some logically more powerful properties, such as excluded middle,
the axiom of choice, the axiom-scheme of replacement, large cardinals, etc. These would justify theexistence of many more points, functions and subspaces, and also prove more equations amongst
them. Nevertheless, the uniqueness result still stands within your particular model of topology.
The additional properties are axioms that we might add to ASD’s account of topology as a whole,
not to that of the real line within it.
4 This is unpublished joint work that Giuseppe Rosolini and Paul Taylor did in 1997. However, current work by
Rosolini that uses groupoids instead of PERs may improve on these results.

67

Questions of what is “true” in the Platonist mathematical world are unanswerable, but we cansay something more definite for computation: ASD is itself a complete axiomatisation of countably
based locally compact spaces [G].
Suppose that you have a continuous function f : R → R that is defined within your Platonist
world, together with a program π taking three rational arguments such that π(q, d, u) terminates
iff d < f (q) < u. Then π may be translated into a term of type R → R in ASD, whose classicalinterpretation is the function f . Conversely, any term of ASD is a program (Remark 3.4).
It is therefore reasonable to ask whether our axioms also tell the whole story as far as analysis
is concerned. We are making the bold (essentially philosophical) claim that the exceedingly weak
computational logic of ASD is enough for “what matters”. The answer must be a utilitarian one,in which we accumulate evidence that our object and the category in which it lives have many of
the familiar properties of analysis.
The paper that follows [J] begins to answer this by studying some of the basic principles ofanalysis on the real line, such as convergence of Cauchy sequences, maxima of compact overt
subspaces and connectedness, culminating in the intermediate value theorem. With the benefit of
the Heine–Borel definition of compactness and the dual notion of overtness, we can develop theseideas in a topological style, in contrast to the metrical one that Bishop and others used.
Concentrating on general topology, one experimental test of whether we have “the real” realline is whether open subsets look like what we expect. Traditionally, any open subset of the realline is uniquely expressible as a countable union of disjoint open intervals. After some constructive
re-interpretation of this statement, we can indeed prove it in ASD, but it depends on compactnessof [0, 1].
Our claim should be seen alongside the analogous one of Errett Bishop [Bis67]. He was not only
constructive but also conservative, in the sense that his theorems are compatible with classicalanalysis (using a kind of constructive set theory [Bri99]), as well as with Brouwer’s Intuitionism
and Markov’s Recursive Mathematics. Since these settings disagree about compactness of theclosed interval, Bishop omitted it and focused on Cauchy completeness and total boundedness
instead. The decomposition of open subsets of R into disjoint open intervals also fails.
Given that ASD includes the Heine–Borel theorem, Bishop’s followers may jump to the conclusion that our theory is unacceptable in their system. Before they do so, they should firstremember that the spaces in ASD are not sets and that the ASD calculus is not the calculus oflogical predicates about points. The ASD statement “[0, 1] is compact” says nothing about theclosed interval [0, 1] from Bishop’s mathematics, because the ASD type R cannot be interpretednaı̈vely as Bishop’s set of real numbers.
One way of understanding the logical strength of ASD is as an algebraic formulation of topology(Theorem 15.8). When the “ASD algebras” are constructed in Bishop’s world, one of them will
be called [0, 1], and there will be an “ASD homomorphism” ∀[0,1] : Σ[0,1] → Σ witnessing thefact that [0, 1] behaves like a compact space within the realm of ASD algebras. The interestingquestion from the point of view of a Bishop-style constructivist is not whether ASD algebras are
acceptable per se (which they are, so far as we can tell), but how good a formulation of topology
ASD provides.
On the other hand, ASD is not presented as algebra but as topology. This has been done bytaking advantage of forty years’ study of categorical logic, type theory and the relationship between
the two. Using this, a terse piece of category theory has been transformed into a symbolic calculusthat can be used by real analysts. If, despite our advocacy of the intrinsic nature of the topologyof the real line, you still believe that sets of points are fundamental, then you will inevitably regard
these “algebraic spaces” (along with locales and formal topology) as artificial. People once said
the same thing about complex numbers.

68However, this point of view is unsustainable in computation, where everything is a mirage —our calculus has at least as good a claim to represent real analysis as does one that is based onGödel numberings of points, especially as we have presented it entirely syntactically.
Another point that might interest Bishop-style constructivists is our basic type Σ. Bishop —and he is certainly not the only one to do so — took numbers as fundamental, and proceeded toconstruct everything else from them. This is supposedly because integers are the basic objects ofcomputation.
But modern computer science (in particular domain theory) teaches us that observable properties are equally, if not more, fundamental. The space Σ is the space of observable propositions.
How might Bishop have axiomatised Σ, and, more generally, spaces of observable properties ΣX ?
Although we ourselves were brought up with domain-theoretic ideas, we had no intention of
repeating them unnecessarily when we began our investigation of analysis. We just wanted toprove some very traditional results (Heine–Borel, boundedness of a function on a closed interval,
and the intermediate value theorem), in order to show that ASD is capable of doing this.
However, we found that it was essential to define the ascending and descending reals and theinterval domain first. Maybe you are interested in some other system (even the classical one) andhave not followed any of the details of the construction in ASD. Nevertheless, a conclusion that
we hope that you will take away from this paper is that R, R and IR are more fundamental than
the familiar (“Euclidean”) real line, and not derived from it.
Interval computation, and to a lesser extent the interval domain, are now common currency
amongst those who program with real numbers in a way that is provably correct. As these people
already know very well, computing a function à la Moore with an interval [d, u] over estimates theimage of the function on this interval. In our notation, Φ[d, u] ⇒ ∀x:[d, u]. Φ(ix).
Dually, computing with the back-to-front interval [u, d] under estimates the image, or as wewould say, ∃x:[d, u]. Φ(ix) ⇒ Φ[u, d]. This is not so well known amongst interval analysts, or very
well explained where it is known. It is clearly a conceptual error to regard the interval [d, u] as
the set {x ∈ R | d ≤ x ≤ u} — both forward and reverse intervals should be seen as generalised
Dedekind cuts in the way that we described in Section 2.
Finally, we invite you to give careful consideration to our Definition 1.1 as the syntax of alanguage for analysis. We feel that this is worthy of study, both as the basis of theory and as thatof computation, and hope that it will ultimately unite these disciplines in a constructive way.

References[Bau00]Andrej Bauer. The Realizability Approach to Computable Analysis and Topology. PhD thesis,
Carnegie Mellon University, 2000. Technical report CMU-CS-00-164.

[Bau08]Andrej Bauer. Efficient computation with Dedekind reals. In Vasco Brattka, Ruth Dillhage,
Tanja Grubba, and Angela Klutch, editors, Fifth International Conference on Computability
and Complexity in Analysis, Hagen, Germany, August 2008.

[BB85]

Errett Bishop and Douglas Bridges. Constructive Analysis. Number 279 in Grundlehren dermathematischen Wissenschaften. Springer-Verlag, 1985.

[BB08a]Josef Berger and Douglas Bridges. The anti-Specker property, a Heine–Borel property, anduniform continuity. Archive for Mathematical Logic, 46:583–592, 2008.

[BB08b]Josef Berger and Douglas Bridges. The fan theorem and positive-valued uniformly continuousfunctions on compact intervals. New Zealand Journal of Mathematics, 38:129–135, 2008.

[Bis67]

Errett Bishop. Foundations of Constructive Analysis. Higher Mathematics. McGraw–Hill,
1967.

69

[BK08]Andrej Bauer and Iztok Kavkler. Implementing real numbers with RZ. Electronic Notes in
Theoretical Computer Science, 202:365–384, 2008.

[Bou66]

Nicolas Bourbaki. Topologie Générale. Hermann, 1966. English translation, General Topology,
distributed by Springer-Verlag, 1989.

[BR87]

Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics. Number 97 in
London Mathematical Society Lecture Notes. Cambridge University Press, 1987.

[Bri99]Douglas Bridges. Constructive mathematics: a foundation for computable analysis.
Theoretical Computer Science, 219:95–109, 1999.

[BS08]

Andrej Bauer and Christopher Stone. RZ: a tool for bringing constructive and computable
mathematics closer to programming practice. Journal of Logic and Computation, 19:17–43,
2008.

[Cle87]

John Cleary. Logical arithmetic. Future Computing Systems, 2(2):125–149, 1987.

[CN96]Jan Cederquist and Sara Negri. A constructive proof of the Heine–Borel covering theorem forformal reals. In Stefano Beradi and Mario Coppo, editors, Types for Proofs and Programs,
number 1158 in Lecture Notes in Computer Science. Springer-Verlag, 1996.

[Con76]

John Horton Conway. On Numbers and Games. Number 6 in London Mathematical Society
Monographs. Academic Press, 1976. Revised edition, 2001, published by A K Peters, Ltd.

[Ded72]

Richard Dedekind. Stetigkeit und irrationale Zahlen. Braunschweig, 1872. Reprinted in[Ded32], pages 315–334; English translation, Continuity and Irrational Numbers, in [Ded01].

[Ded01]

Richard Dedekind. Essays on the theory of numbers. Open Court, 1901. English translations
by Wooster Woodruff Beman; republished by Dover, 1963.

[Ded32]

Richard Dedekind. Gesammelte mathematische Werke, volume 3. Vieweg, Braunschweig,
1932. Edited by Robert Fricke, Emmy Noether and Øystein Ore; republished by Chelsea,
New York, 1969.

[ES98]

Abbas Edalat and Philipp Sünderhauf. A domain-theoretic approach to real number
computation. Theoretical Computer Science, 210:73–98, 1998.

[Esc04]

Martı́n Escardó. Synthetic topology of data types and classical spaces. Electronic Notes in
Theoretical Computer Science, 87:21–156, 2004.

[FH79]

Michael Fourman and Martin Hyland. Sheaf models for analysis. In Michael Fourman, Chris
Mulvey, and Dana Scott, editors, Applications of Sheaves, number 753 in Lecture Notes inMathematics. Springer-Verlag, 1979.

[Fri58]Richard Friedberg. Un contre-example relatif aux fonctionnelles récursives. Comptes rendus
hebdomadaires des scéances de l’Académie des Sciences (Paris), 247:852–854, 1958.

[Gen35]Gerhard Gentzen. Untersuchungen über das logische Schliessen. Mathematische Zeitschrift,
39:176–210, 405–431, 1935. English translation in [Gen69], pages 68–131.

[Gen69]Gerhard Gentzen. The Collected Papers of Gerhard Gentzen. Studies in Logic and theFoundations of Mathematics. North-Holland, 1969. Edited by Szabo, Manfred.

[GHK+ 80] Gerhard Gierz, Karl Heinrich Hoffmann, Klaus Keimel, Jimmie Lawson, Michael Mislove, andDana Scott. A Compendium of Continuous Lattices. Springer-Verlag, 1980. Second edition,
Continuous Lattices and Domains, published by Cambridge University Press, 2003.
[Hey56]

Arend Heyting. Intuitionism, an Introduction. Studies in Logic and the Foundations ofMathematics. North-Holland, 1956. Third edition, 1971.

[HLPZ]

Guillaume Hanrot, Vincent Lefèvre, Patrick Pélissier, and Paul Zimmermann. The MPFR
Library. INRIA. www.mpfr.org.

[HR90]

Martin Hyland and Giuseppe Rosolini. The discrete objects in the effective topos. Proceedingsof the London Mathematical Society, 60:1–36, 1990.

[Hyl82]

Martin Hyland. The effective topos. In Anne Troelstra and Dirk van Dalen, editors, The
L.E.J. Brouwer Centenary Symposium. North Holland, 1982.

70

[Hyl91]

Martin Hyland. First steps in synthetic domain theory. In Aurelio Carboni, Maria-Cristina
Pedicchio, and Giuseppe Rosolini, editors, Category Theory, number 1488 in Lecture Notes inMathematics. Springer Verlag, 1991.

[Joh77]

Peter Johnstone. Topos Theory. Number 10 in London Mathematical Society Monographs.
Academic Press, 1977.

[Joh82]

Peter Johnstone. Stone Spaces. Number 3 in Cambridge Studies in Advanced Mathematics.
Cambridge University Press, 1982.

[Joh84]

Peter Johnstone. Open locales and exponentiation. Contemporary Mathematics, 30:84–116,
1984.

[JR84]

William Julian and Fred Richman. A uniformly continuous function on [0,1] that is
everywhere different from its infimum. Pacific Journal of Mathematics, 111:333–340, 1984.

[JT84]

André Joyal and Myles Tierney. An Extension of the Galois Theory of Grothendieck, volume
309 of Memoirs. American Mathematical Society, 1984.

[Kau80]

Edgar Kaucher. Interval analysis in the extended interval space IR. In Götz Alefeld and Rolf
Grigorieff, editors, Fundamentals of Numerical Computation, volume 2 of Computing.
Supplementum. Springer-Verlag, 1980.

[Kea96]

Baker Kearfott. Interval computations: Introduction, uses and resources. Euromath Bulletin,
2(1):95–112, 1996.

[Kel86]

Max Kelly. A survey of totality in ordinary and enriched categories. Cahiers de Géometrie etTopologie Differentielle, 27:109–132, 1986.

[Kle45]

Stephen Kleene. On the interpretation of intuitionistic number theory. Journal of Symbolic
Logic, 10:109–124, 1945.

[KNZ96]

Vladik Kreinovich, Vyacheslav Nesterov, and Nina Zheludeva. Interval methods that are
guaranteed to underestimate (and the resulting new justification of Kaucher arithmetic).
Reliable Computing, 2(2):119–124, 1996.

[Koc06]

Anders Kock. Synthetic Differential Geometry. Number 333 in London Mathematical Society
Lecture Note Series. Cambridge University Press, second edition, 2006.

[Lak95]

Anatoly Lakeyev. Linear algebraic equations in Kaucher arithmetic. In Vladik Kreinovich,
editor, Applications of Interval Computations (APIC’95), 1995. supplement to Reliable
Computing.

[Lam07]

Branimir Lambov. RealLib: An efficient implementation of exact real arithmetic.
Mathematical Structures in Computer Science, 17(1):81–98, 2007.
www.brics.dk/∼barnie/RealLib/.

[Moo66]

Ramon Moore. Interval Analysis. Prentice Hall, 1966.

[Mül01]

Norbert Müller. The iRRAM: Exact arithmetic in C++. In Jens Blanck, Vasco Brattka, andPeter Hertling, editors, Computability and Complexity in Analysis: 4th International
Workshop, CCA 2000 Swansea, UK, September 17, 2000, Selected Papers, number 2064 in
Lecture Notes in Computer Science. Springer-Verlag, 2001.

[Pal05]

Eric Palmgren. Continuity on the real line and in formal spaces. In Laura Crosilla and Peter
Schuster, editors, From Sets and Types to Topology and Analysis: Towards Practicable
Foundations of Constructive Mathematics, Oxford Logic Guides. Oxford University Press,
2005.

[Pea97]

Giuseppe Peano. Studii di logica matematica. Atti della Reale Accademia di Torino,
32:565–583, 1897. Reprinted in Peano, Opere Scelte, Cremonese, 1953, vol. 2, pp. 201–217,
and (in English) in Kennedy, Hubert, Selected Works of Giuseppe Peano, Toronto University
Press, 1973, pp 190–205.

[Plo77]

Gordon Plotkin. LCF considered as a programming language. Theoretical Computer Science,
5:223–255, 1977.

71

[Rob66]

Abraham Robinson. Non-standard Analysis. North-Holland, 1966. Revised edition, 1996,
published by Princeton University Press.

[Rog92]Hartley Rogers. Theory of Recursive Functions and Effective Computability. MIT Press, third
edition, 1992.

[Ros86]

Giuseppe Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford,
1986.

[Ros01]Frank Rosemeier. A constructive approach to Conway’s theory of games. In Peter Schuster,
Ulrich Berger, and Horst Osswald, editors, Reuniting the Antipodes: Constructive andNonstandard Views of the Continuum. Springer-Verlag, 2001.

[Sch03]

Peter Schuster. Unique existence, approximate solutions, and countable choice. TheoreticalComputer Science, 305:433–455, 2003.

[Sch05]

Peter Schuster. What is continuity, constructively? Journal of Universal Computer Science,
11(12):2076–2085, 2005.

[Sco72a]Dana Scott. Continuous lattices. In Bill Lawvere, editor, Toposes, Algebraic Geometry and
Logic, number 274 in Lecture Notes in Mathematics. Springer-Verlag, 1972.

[Sco72b]Dana Scott. Lattice theory, data types and semantics. In Randall Rustin, editor, Formal
Semantics of Programming Languages. Prentice-Hall, 1972.

[Spi07]

Bas Spitters. Located and overt sublocales. arxiv.org/abs/math/0703561, 2007.

[Ste85]David Stevenson. Binary floating-point arithmetic. ANSI/IEEE Standard, 754, 1985.
Revised, 2008.

[Sto83]

Otto Stolz. Zur Geometrie der Alten, insbesondere über ein Axiom des Archimedes.
Mathematische Annalen, 22(4):504–519, 1883.

[Str80]Ross Street. Cosmoi of internal categories. Transactions of the American MathematicalSociety, 258:271–318, 1980.

[SW78]

Ross Street and Robert Walters. Yoneda structures on 2-categories. Journal of Algebra,
50:350–379, 1978.

[Tay91]

Paul Taylor. The fixed point property in synthetic domain theory. In Gilles Kahn, editor,
Logic in Computer Science 6. IEEE, 1991.

[Tay99]Paul Taylor. Practical Foundations of Mathematics. Number 59 in Cambridge Studies inAdvanced Mathematics. Cambridge University Press, 1999.

[Thi97]

Hayo Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, Universityof Edinburgh, 1997. ECS-LFCS-97-376.

[Tho80]Walter Tholen. A note on total categories. Bulletin of the Australian Mathematical Society,21:169–173, 1980.

[TvD88]Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in Mathematics, an Introduction.
Number 121 and 123 in Studies in Logic and the Foundations of Mathematics. North-Holland,
1988.

[Ver94]

Japie Vermeulen. Proper maps of locales. Journal of Pure and Applied Algebra, 92:79–107,
1994.

[Waa05]Frank Waaldijk. On the foundations of constructive mathematics – especially in relation to
the theory of continuous functions. Foundations of Science, 10(3):249–324, 2005.

[Wei00]Klaus Weihrauch. Computable Analysis. Springer-Verlag, Berlin, 2000.

[Woo82]

Richard Wood. Some remarks on total categories. Journal of Algebra, 75:538–545, 1982.

72

The papers on abstract Stone duality may be obtained fromwww.Paul Taylor.EU/ASD[O] Paul Taylor, Foundations for Computable Topology. in Giovanni Sommaruga (ed.), Foundational
Theories of Mathematics, Kluwer 2009.
[A] Paul Taylor, Sober spaces and continuations. Theory and Applications of Categories,
10(12):248–299, 2002.
[B] Paul Taylor, Subspaces in abstract Stone duality. Theory and Applications of Categories,
10(13):300–366, 2002.
[C] Paul Taylor, Geometric and higher order logic using abstract Stone duality. Theory and Applicationsof Categories, 7(15):284–338, 2000.
[D] Paul Taylor, Non-Artin gluing in recursion theory and lifting in abstract Stone duality. 2000.
[E] Paul Taylor, Inside every model of Abstract Stone Duality lies an Arithmetic Universe. Electronic
Notes in Theoretical Computer Science 122 (2005) 247-296, Elsevier.
[F] Paul Taylor, Scott domains in abstract Stone duality. March 2002.
[G–] Paul Taylor, Local compactness and the Baire category theorem in abstract Stone duality.
Electronic Notes in Theoretical Computer Science 69, Elsevier, 2003.
[G] Paul Taylor, Computably based locally compact spaces. Logical Methods in Computer Science, 2(2006) 1–70.
[H–] Paul Taylor, An elementary theory of the category of locally compact locales. APPSEM Workshop,
Nottingham, March 2003.
[H] Paul Taylor, An elementary theory of various categories of spaces and locales. November 2004.
[J] Paul Taylor, A λ-calculus for real analysis. Computability and Complexity in Analysis, Kyoto,
August 2005.
[K] Paul Taylor, Interval analysis without intervals. February 2006.
[L] Paul Taylor, Tychonov’s theorem in abstract Stone duality. September 2004.
[M] Paul Taylor, Cartesian closed categories with subspaces. 2009.

This paper results from a collaboration that began with Paul Taylor’s visit to Ljubljana in
November 2004. A preliminary version of this work was presented at Computability and Complexity
in Analysis in Kyoto on 28 August 2005, and we are grateful to Peter Hertling and the CCA
programme committee for the indulgence of allowing us to occupy altogether 80 pages of theirproceedings. We would also like to thank Vasco Brattka, Douglas Bridges, Thierry Coquand,
Fer-Jan de Vries, Peter Johnstone, Vladek Kreinovich, Russell O’Connor, Andrea Schalk, Peter
Schuster, Alex Simpson, Bas Spitters, Chris Stone, Maarten van Emden and Graham White for
their helpful comments, and the anonymous referee for a most professional report.
Correspondence (by email only, please):
Andrej Bauer, Department of Mathematics and Physics, University of Ljubljana.
Paul Taylor.
Andrej.Bauer@andrej.com
pt08@PaulTaylor.EU73