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 discrete set, 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 of the closed interval. Previous theories of recursive analysis failed to do this because they were based on points; ASD succeeds because, like locale theory and formal topology, it is founded on 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 that the 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 paper that 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 pairs of real numbers.

We make a thorough study of arithmetic, in which our operations are more complicated than 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  9. Dedekind completeness  42
2. Cuts and intervals  5  10. Open, compact and overt intervals 45
3. Topology as λ-calculus  12  11. Arithmetic  49
4. The ASD λ-calculus  15  12. Multiplication  54
5. The monadic principle  22  13. Reciprocals and roots  58
6. Dedekind cuts  28  14. Axiomatic completeness  60
7. The interval domain in ASD  33  15. Recursive analysis  64
8. The real line as a space in ASD 37  16. Conclusion  67

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

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, the real 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 the rationals — being defined by division — presuppose an inequality relation that we shall come to regard as topology.

Although a great deal of mathematics has since been built over Dedekind’s construction, we still have no definition of the real numbers that is widely accepted across different foundational settings. This is in contrast to the Dedekind–Peano–Lawvere definition of the natural numbers, which has been applied within logical systems that are much weaker than the classical one, or differ substantially from it in other ways. This is a very unfortunate state of affairs at a time when a debate has at last begun amongst a number of separate disciplines that all call themselves “constructive”, ours being one of them. We need a definition so that we can agree on what we’re talking about.

So, at the risk of seeming presumptuous in the face of such a venerable object, let us first write down our own opinion of what it is that we are trying to construct. In this paper we shall use R for the object under construction, and ℝ for the real line in classical or other forms of analysis.

Definition 1.1 An object R is a Dedekind real line if

(a) it is an overt space (Theorem 9.2);

(b) it is Hausdorff, with an inequality or apartness relation, ≠ (Theorem 9.3);

(c) the closed interval [0, 1] is compact (Theorem 10.7);

(d) R has a total order, that is, (x ≠ 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 ≠ 0, in the sense of (d) (Theorem 13.4);

(g) and Archimedean (Theorem 13.6), that is, for x, y : R,

y > 0 ⇒ ∃n:ℤ. y(n − 1) < x < y(n + 1).

Our axioms are all true of the classical real line. Indeed, with the exception of the new concept of overtness, they are all headline properties in traditional analysis — just as induction had been formulated two centuries before Dedekind and Peano encapsulated it in their axioms, and used two millennia before that. These are not just peculiar order-theoretic facts that happen to lend themselves to some interesting construction.

However, some of our constructive colleagues have not adopted certain of these axioms. In particular, many formalist accounts and machine implementations use Cauchy sequences instead of Dedekind cuts. You already know our opinion on this question from the title of this paper: familiar examples such as Riemann integration give Dedekind cuts naturally, but sequences artificially. Any Cauchy sequence with a specified modulus of convergence has a limit that is defined by a Dedekind cut, but it is more difficult to translate in the other direction. We suspect that the preference for Cauchy sequences is merely a symptom of the traditional prejudice against logic. This paper shows that Dedekind cuts can be defined without using set theory, and we hope to demonstrate in future work that they also provide a natural way in which to compute with real numbers [Bau08, K].

The Heine–Borel theorem (compactness of the closed interval) is one of the most important properties that real analysts use. However, as we shall see in Section 15, this is not just a result that we prove in passing, but a hotly debated issue in the foundations of constructive analysis. For example, Errett Bishop [Bis67] reformulated a large part of the subject without it, deftly avoiding the many pathologies that arise from so doing.

In particular, he defined a function to be “continuous” if it is uniformly so when restricted to any compact domain, “compact” itself being defined as closed and totally bounded. Hence any continuous f : K → ℝ^{+} is bounded (away from ∞, if you wish), but there is no similar result to bound it away from 0. Indeed, if K is Cantor space, such a result would entail (Brouwer’s fan theorem and so) the Heine–Borel theorem. It follows that, if there is a category of partial functions on ℝ that agrees with the uniformly continuous ones on compact domains and includes λx.1/x, then the Heine–Borel theorem holds [Pal05, Sch05, Waa05, JR84, 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 numbers that are representable by programs, then the results are exceedingly unpleasant. In particular, the Heine–Borel theorem fails.

In fact, Dedekind completeness and the Heine–Borel property are both consequences of the view that open sets and not points are primary. That they hold at all in the traditional setting is the result of the heavy-handed methods of classical mathematics, which are far stronger than what is justified by computation. Brouwer’s fan theorem is, arguably, a way of legitimising part of the classical approach in a constructive setting.

The best developed formulation of topology entirely in terms of open sets (“pointless topology”, according to a now rather tired joke) is provided by locale theory. Although it does not consider computation, it does provide a way of developing general topology in foundational settings (at least, in toposes) other than the classical one. The most famous example of this is that it proves the Tychonov theorem (that the product of any family of compact objects is compact) without using the axiom of choice [Joh82, Theorem III 1.7]. Less well known, but more importantly for us, the localic interval [0, 1] is always Dedekind-complete and compact. On the other hand, when we interpret the traditional (point-based) definitions in the internal language of a sheaf topos, the object of Cauchy reals is typically smaller than the Dedekind one, and the Heine–Borel theorem fails [FH79].

Formal Topology also works with open subspaces, but is based on Martin-Löf type theory; there too [0, 1] is compact [CN96].

Abstract Stone Duality exploits the algebra of open sets as well, and so the “real line” R that we construct in this paper is Dedekind-complete and satisfies the Heine–Borel property. But ASD generalises Dedekind’s topological conception of the real line: in it, the topology is an inherent and unalienable part of a space, which is not a set of points to which open subsets have been added as an afterthought.

In locale theory, the algebra and lattice theory are all too obvious, whilst they are represented in formal topology by generators and relations. Both of these theories expect a high degree of mathematical sophistication and perseverance from the student, and only in an exceptionally well written account do the public theorems about topology stand out from the private algebraic calculations. In [Joh82] the former are marked with an asterisk, although the official meaning of that symbol is a dependence on the axiom of choice.

The lattice of open subspaces in locale theory is a set (or an object of a topos), but in ASD it is another space, with its own topology. This is formulated in the style of a type theory that makes ASD look like topology with points. The λ-notation speaks out loud and clear about continuous maps in a way that frame homomorphisms in locale theory do not. When we do some basic analysis in [J], we shall see that the language of terms, functions and open predicates actually works more smoothly than does the traditional one using set theory.

In both traditional topology and locale theory there is an asymmetry between infinite unions and finite intersections that makes it difficult to see the duality between open and closed phenomena. Intuitionistic foundations also obscure this symmetry by stating many results that naturally pertain to closed sets in a form that uses double negations. When we treat the lattice of opens of one space as another space, by contrast, the purely infinitary (directed) joins slip into the background, and the open–closed duality stands out very clearly. Indeed, it is a fruitful technique to “turn the symbols upside down” (⊤/⊥, ∧/∨, =/≠, ∀/∃), often giving a new theorem.

In this context, we shall see what the foundational roles of Dedekind completeness and the Heine–Borel theorem actually are. The former is the way in which the logical manipulation of topology has an impact on numerical computation. Again there is an analogy with the axioms for the natural numbers: for them the same role is played by definition by description, which Giuseppe Peano was also the first to formulate correctly [Pea97, §22], albeit in a different paper from the one on induction. In the ASD λ-calculus, these ideas are captured as rules that introduce numbers on the basis of logical premises.

The Heine–Borel property, meanwhile, is the result of ensuring that all algebras are included in the category. Our λ-calculus formulates this idea in an apparently point-based way by introducing higher-order terms which ensure that subspaces carry the subspace topology. We shall show that these terms are inter-definable with the “universal quantifiers” ∀ that define compactness.

The new concept of overtness is related to open subspaces in the way that compactness is to closed ones, and to logic in the shape of the existential quantifier, ∃. However, in contrast to compactness of the closed interval, no discipline would contest that the real line is overt. Indeed, the reason why you haven’t heard of overt (sub)spaces before is that classical topology makes all spaces overt — by force majeure, without providing the computational evidence.

This idea has, in fact, been identified in locale theory, but only the experts in that subject have been able to exploit it [JT84, Joh84]. In the case of overtness, formal topology shows up the idea better than locale theory does. Its role in constructive analysis is played by locatedness, though that is a metrical property, so the correspondence is not exact [Spi07]. We shall show in ASD’s account of analysis [J] that overtness explains the situations in which equations fx = 0 for f : ℝ → ℝ can or cannot be solved.

However, it is really in computation that the importance of this concept becomes clear. For example, it provides a generic way of solving equations, when this is possible.

Since ASD is formulated in a type-theoretical fashion, with absolutely no recourse to set theory, it is intrinsically a computable theory.

The familiar arithmetical operations +, − are × are, of course, computable algebraic structure on R, as are division and the (strict) relations <, > and ≠ when we introduce suitable types for their arguments and results. The topological properties of overtness and compactness are related to the logical quantifiers ∃ and ∀, which we shall come to see as additional computable structure.

Any term of the ASD calculus is in principle a program, although the details of how this might be executed have yet to be worked out [Bau08, K]. In particular, our proofs of compactness and overtness of closed intervals provide programs for computing quantifiers of the form ∀x:[d, u] and ∃x:[d, u] respectively. These are general and powerful higher-order functions from which many useful computations in real analysis can be derived.

This paper is rather long because we have to introduce the ASD calculus before we can use it for the construction. Although real arithmetic is familiar and not really related to the main issue of the Heine–Borel theorem, you would think it odd if we left it out, and of course we shall need it in order to prove completeness of the axioms, but it is a sizable task in itself. If you are impatient to see our construction of R, you may find it helpful to start with Section 6, and then bring in the introductory material as you need it.

We shall use a lot of ideas from interval analysis. However, instead of defining an interval [d, u] as the set {x ∈ ℝ | d ≤ x ≤ u} or as a pair ⟨d, u⟩ of real numbers, as is usually done, we see it as a weaker form of Dedekind cut, defined in terms of the rationals. Real numbers (genuine cuts) are special intervals. Section 2 explains the classical idea behind our construction of the Dedekind reals, presenting it from the point of view of interval analysis.

As this is the first paper in which Abstract Stone Duality has reached maturity, we give a survey of it in Sections 3–5 that will also be useful for reference in connection with other applications besides analysis. This provides a guide to the earlier papers, by no means making them redundant; for other independent introductions, see [J, O].

Sections 6–9 perform the main construction, developing cuts, the interval domain and the real line in ASD, and prove Dedekind completeness. Section 10 proves that the closed interval is compact and overt.

Sections 11–13 consider arithmetic in an entirely order-theoretic style, i.e. with Dedekind cuts rather than Cauchy sequences. We formulate an important “roundedness” property of the interval operations that is crucial to their correctness, extend the arithmetic operations to Kaucher’s 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 shows that it is unique (up to unique isomorphism), i.e. that the axioms above are complete. This means, on the one hand, that they are sufficient to develop analysis [J], and on the other that we may focus on them in order to do computation. We also show that Dedekind completeness is equivalent to abstract sobriety via some simple λ-conversions.

Finally, Section 15 compares ours with other schools of thought. In particular, we contrast compactness of the closed interval here with its pathological properties in Recursive Analysis, and comment on the status of ASD from the point of view of a constructivist in the tradition of Errett Bishop.

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 the Heine–Borel theorem to prove an abstract property of ℝ, 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 ∈ ℝ 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

D_{a} ≡ {d ∈ ℚ | d < a} and U_{a} ≡ {u ∈ ℚ | a < u}.

These are disjoint inhabited open subsets that “almost touch” in the sense that

d < 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 ℝ and extends towards ±∞ can be expressed order-theoretically, using a condition that we shall call roundedness:

d ∈ D ⟺ ∃e. d < e ∧ e ∈ D  and  u ∈ 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(ℚ) × P(ℚ), that is rounded, bounded (i.e. inhabited), disjoint and located.

Exercise 2.2 If Δ ⊂ ℝ is an open set of reals that extends downwards, show that D ≡ Δ ∩ ℚ is a rounded set of rationals with the same property, and that this defines a bijection between such subsets, where Δ ≡ {r ∈ ℝ | ∃q ∈ D. r < q}. In future we shall write D for either representation, and pass between them without comment; in particular, in “ℝ \ (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 ∈ ℝ, such a pseudo-cut corresponds classically to a closed interval [d, u] ≡ ℝ \ (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 of signs.

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 a lower bound for the maximum, but finding upper bounds is problematic using standard numerical methods, especially when the function has “spikes”.

For the sake of illustration, consider an arithmetical function f : [0, 1]^{n} → ℝ. If this is just addition or multiplication, Moore’s interval operations provide the minimum and maximum values of the function on the domain directly. For a more complicated arithmetical function, we interpret the 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 similar large 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 the resulting 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 that can 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 continuous functions to take intervals instead of real numbers as arguments. In fact, that’s exactly the point:

(a) ideally, we extend f to the operation F_{0} that takes intervals to intervals by

F_{0}[d, u] ≡ {fx | x ∈ [d, u]},

(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] = [fa, fa] and F_{0}[d, u] ⊂ F [d, u].

Whilst Moore’s interpretation may give a huge over-estimate of the image if we don’t rewrite the expression, it has an important technical property, namely that it preserves (syntactic) composition of arithmetic expressions, so it is easily performed by a compiler.

The first question that this raises is whether the ideal operation F_{0}, which (a) defines set-theo-retically, 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 F_{0}, but also for the process that extends f to F or F_{0}. However, as P(ℚ) is a complete lattice, rather than a 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 ℝ^{ℝ}.)

Definition 2.6 Let L be a complete lattice such as P(ℚ). 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 ⩽ V then V ∈ U; and

(b) “inaccessible by directed unions”, i.e. if (⋁_{i∈I} U_{i}) ∈ U then already (⋁_{i∈F} U_{i}) ∈ U for some finite subset F ⊂ I.

This Scott topology is never Hausdorff (except, that is, on the trivial lattice).

A function f : L_{1} → L_{2} 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 ⩽ y in L_{1} then fx ⩽ fy in L_{2}. 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, and K ⊂ 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 ≡ \underline{ℝ} ≡ ℝ + \{−∞, +∞\}, considered as a complete lattice in the arithmetical order, so +∞ is the top element. Equipped with the Scott topology, this space arises in real analysis because lower semicontinuous functions X → ℝ are just functions X → \underline{ℝ} that are continuous in the sense of general topology. We shall see, however, that it is a mistake to think of \underline{ℝ} as derived from ℝ in this clumsy way: it is really simpler and more fundamental than ℝ 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 ⊂ ℚ is used. The descending reals, \overline{ℝ}, are defined in the same way, but with the opposite order, and are related to upper semicontinuous functions. The words “ascending” and “descending” relate the usual temporal language about the real 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. not necessarily 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} < ⋯ < u_{2} < u_{1} < u_{0},

whose limits sup d_{n} and inf u_{n} we would like to see as the ‘ultimate result’ of the computation.

If these limits exist in ℝ, say d ≡ sup d_{n} and u ≡ inf u_{n}, then [d, u] is the (directed) intersection ⋂[d_{n}, u_{n}]. However, d and u are best seen as ascending and descending reals,

D ≡ \{d | ∃n. d < d_{n}\} ∈ \underline{ℝ}  and  U ≡ \{u | ∃n. u > u_{n}\} ∈ \overline{ℝ},

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 ℝ \ (D ∪ U), and is always a closed subspace.

Notice that the open subsets D and U represent positive information, namely the lower and upper 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 not yet excluded, which is negative information.

Definition 2.10 We can consider these generalised intervals as members of the interval domain, Iℝ [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 the order 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 ⊂ ℚ may be represented as a function ℚ → {⊤, ⊥} that says whether or not each d ∈ ℚ belongs to D. Since we believe that topology is fundamental, we give this target set the Scott topology. It then becomes the Sierpiński space, in which just one singleton {⊤} is open, making the other {⊥} closed. It therefore looks like (⊙ •), and we shall call it Σ.

Since ℚ is discrete, it doesn’t change much to require our functions ℚ → Σ to be continuous. However, for a general topological space X (such as ℝ), continuous functions ϕ : X → Σ correspond bijectively to open subspaces U ⊂ X, by U ≡ ϕ^{−1}(⊤). We shall say that ϕ classifies U.

Notation 2.12 Having passed from the (open) subset D ⊂ ℚ to a (continuous) function δ : ℚ → Σ, we also replace set-theoretic notation with the λ-calculus. A function x ↦ ϕ(x) is written as a λ-abstraction λx. ϕ(x); we use nested λ-abstractions for several variables, but write λxy. σ instead of λ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 δ, υ : Σ^{ℚ}, adopting the convention of using Greek letters for terms of this type. Many authors in computer science would write ℚ → Σ instead of Σ^{ℚ}, which is the notation in pure mathematics. Membership d ∈ D is written δd, and set-formation becomes λ-abstraction. In particular, D_{a} and U_{a} 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 the real line as a whole is a subset ℝ ⊂ Σ^{ℚ} × Σ^{ℚ}.

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 for differential and integral calculus, and ours of getting a machine to compute with real numbers. He 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 we give 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 : ℝ → ℝ 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 (δ_{fa}, υ_{fa}) that represents the value f(a) of the function at that input. In other words, the square on the left commutes:

[figure: ℝ; i; Σ^{ℚ} × Σ^{ℚ}; ℝ; i; Σ^{ℚ} × Σ^{ℚ}]

.................... Φ

[figure: ℝ; f; i; Σ^{ℚ} × Σ^{ℚ}; F; . . . . . . . . . . . . . . . .; Σ; ϕ]

Remark 2.14 We shall not attack the problem of extending functions directly. It is simpler and more in keeping with the ideas of computation, Dedekind cuts and topology to consider first how an open subset of ℝ may be extended to one of Σ^{ℚ} × Σ^{ℚ}.

Recall from Notation 2.11 that such an open subset is classified by a continuous function taking values in Σ. We expect the function ϕ from ℝ (classifying an open subset of it) to be the restriction of a function Φ from Σ^{ℚ} × Σ^{ℚ} (classifying an open subset of that), making the triangle on the right above commute. In other words, ℝ should carry the subspace topology inherited from the ambient space, Σ^{ℚ} × Σ^{ℚ}, 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 defining

F (δ, υ) ≡ (λd. Φ_{d}(δ, υ), λu. Ψ_{u}(δ, υ)),

where Φ_{d} and Ψ_{u} are the extensions of ϕ_{d} ≡ λx. (d < fx) and ψ_{u} ≡ λx. (fx < 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.

Proposition 2.15 Classically, there is a map I : Σ^{ℝ} ↣ Σ^{Σ^{ℚ}×Σ^{ℚ}}, defined by

(V ⊂ ℝ) open ↦ {(D, U) | ∃d ∈ D. ∃u ∈ U. (d < u) ∧ [d, u] ⊂ V }

in traditional notation, or

ϕ : Σ^{ℝ} ↦ λδυ. ∃du. δd ∧ υu ∧ (d < u) ∧ ∀x:[d, u]. ϕx

in our λ-calculus, that is Scott-continuous. It makes Σ^{ℝ} a retract of Σ^{Σ^{ℚ}×Σ^{ℚ}}, as it satisfies the equation

Σ^{i} · I = id_{Σ^{ℝ}}  or  x : ℝ, ϕ : Σ^{ℝ} ⊢ Iϕ(ix) ⇔ ϕx,

where ix ≡ (δ_{x}, υ_{x}) : Σ^{ℚ} × Σ^{ℚ}. This expresses local compactness of ℝ. Proof The Heine–Borel theorem, i.e. the “finite open sub-cover” definition of compactness for the closed interval [d, u], says exactly that the expression “[d, u] ⊂ V ” is a Scott-continuous predicate in the variable V : Σ^{ℝ} (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) ↦ Iϕ(ia) ≡ (∃du. a ∈ (d, u) ⊂ [d, u] ⊂ V ) ⟺ (a ∈ V).  □

The argument so far has relied on the prior existence of ℝ. The next step is to eliminate real numbers in favour of rational ones.

Lemma 2.16 Since Φ : Σ^{ℚ} × Σ^{ℚ} → Σ is a Scott-continuous function,

Φ(δ_{f}, υ_{s}) ⟺ ∃et. (e < f) ∧ (s < t) ∧ Φ(δ_{e}, υ_{t})  (a)
Φ(δ_{x}, υ_{x}) ⟺ ∃mk. (p_{k−1} < x < p_{k+1}) ∧ Φ(δ_{p_{k−1}}, υ_{p_{k+1}})  (b)

where p_{k} ≡ d + 2^{−m}k(u − d), for any chosen d < u. Although p_{k} also depends on m, d and u, we omit them to simplify the notation: they should be understood to come from the expression in which p_{k} is embedded. Proof In traditional notation, the unions

D_{f} = ⋃ ; _{e<f}D_{e} and U_{s} = ⋃ ; _{s<t}U_{t}

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 some open interval (e, t), we may find m and k so that e < p_{k−1} < x < p_{k+1} < t. □

Proposition 2.17 The idempotent E ≡ I · Σ^{i} on Σ^{Σ^{ℚ}×Σ^{ℚ}} is given by

EΦ(δ, υ) ≡ ∃n ≥ 1. ∃q_{0} < ⋯ < q_{n}. δq_{0} ∧ υq_{n} ∧ ⋀_{k=0}^{n−1} Φ(δ_{q_{k}}, υ_{q_{k+1}}).

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 ⩽ I · Σ^{i}]: Although the formula for E essentially involves abutting closed intervals,

[d, u] = [q_{0}, q_{1}] ∪ [q_{1}, q_{2}] ∪ ⋯ ∪ [q_{n−1}, q_{n}],

part (a,⇒) of Lemma 2.16 expands each of them slightly, from [q_{k}, q_{k+1}] to [e, t]. Then each x ∈ [d, u] lies inside one of the overlapping open intervals (e, t):

EΦ(δ, υ) ⇒ ∃q_{0} … q_{n}. δq_{0} ∧ υq_{n} ∧ ⋀_{k=0}^{n−1} ∃et. (e < q_{k} < q_{k+1} < t) ∧ Φ(δ_{e}, υ_{t})
⇒ ∃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 (p_{k−1}, p_{k+1}) ∋ x with dyadic endpoints, such that Φ(p_{k−1}, p_{k+1}) holds. Although some points x may â 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:ℕ. ∃k. (p_{k−1} < x < p_{k+1}) ∧ Φ(δ_{p_{k−1}}, υ_{p_{k+1}})
⇒ ∃m. ∀x:[d, u]. ∃k. (p_{k−1} < x < p_{k+1}) ∧ Φ(δ_{p_{k−1}}, υ_{p_{k+1}})
⇒ ∃m. ⋀_{k=0}^{2^{m}} Φ(δ_{p_{k−1}}, υ_{p_{k+1}}) ⇒ ∃m. ⋀_{k=0}^{2^{m}−1} Φ(δ_{p_{k}}, υ_{p_{k+1}}),

where we trim the intervals using Lemma 2.16(a,⇒) and omit the last one. Then n ≡ 2^{m}, q_{0} ≡ p_{0} ≡ d, q_{1} ≡ p_{1}, …, q_{n} ≡ p_{2^{m}} ≡ u provide a sequence to justify EΦ(δ, υ). □

Remark 2.18 Notice that this formula for E involves only rational numbers (and predicates on them) 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_{Σ^{ℝ}} and I · Σ^{i} = E.

It is the formula E — not the classically defined map I or the accompanying proof — that we shall use to construct the real line in ASD. In Section 15 we shall discuss some systems of analysis in which 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 be appropriate 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 : ℝ → ℝ be a continuous function and F be any continuous extension of f 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 < fx < t, or, equivalently, F_{0}[d, u] ⊂ (e, t),

where F_{0} gives the set-theoretic image. Then there is some finite sub-division (which could be chosen to be dyadic), d ≡ q_{0} < q_{1} < ⋯ < q_{n−1} < q_{n} ≡ u, such that

(e, t) ⊃ ⋃_{m=0}^{n−1} F [q_{k}, q_{k+1}].

Moreover, we obtain F_{0} from F in Remark 2.5 using E and Remark 2.14. □

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 we play around with the formulae. Of course, if a < b then the subsets

D ≡ D_{b} ≡ {d | d < b} and U ≡ U_{a} ≡ {u | a < u}

overlap. But we may still apply Proposition 2.15 to them, obtaining the existential quantifier,

(D_{b}, U_{a}) ∈ 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 overestimation of the range of a function in interval analysis, could this back-to-front version for ∃ yield an underestimate? It is obviously very dangerous in this case to 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 interval in 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’s arithmetic 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 Sierpiń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, ℕ and Σ are axiomatised by their 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, more basically, those of type Σ like propositions. We can form conjunctions and disjunctions of such terms, 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 properties as the quantifiers (cf. Remark 4.16). A space X is called compact when it has a ∀_{X} operator, and overt when it has ∃_{X}.

Statements in the theory are expressed as equations between terms, but we use ⩽ or ⇒ as syntactic 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 such a 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, this is not because of our asceticism, but because spaces and maps do not possess it. The justification of this claim is that, starting from the axioms of ASD, we may reconstruct the categories of computably 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 to know 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 that each 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 ⊢ fx : Y denotes a continuous function f : X → Y. All maps between spaces are continuous, simply because the calculus never introduces discontinuous functions.

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 the closed 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 a calculus that can prove theorems for itself, indeed in a computational setting. It was the subject of 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.

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 equality of two real numbers, a, b : R, using a predicate of type Σ. But since the logic of closed predicates is upside down, the (open) predicate is a ≠_{R} b, and for equality we have to write the equation (a ≠ 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 we are doing in ASD: ≠ 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–Lö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 ↣ Y using the subset-forming tools provided by the foundations of the system. For example, the real line may be constructed as the set (type, object) of those pairs (D, U) or (δ, υ) that satisfy the properties required of a Dedekind cut.

What is the topology on such a subset? We fall on the mercy of the underlying logic of sets of points to determine this, and so to prove important theorems of mathematics such as compactness of 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 the existence of certain continuous functions of higher type. We saw in Proposition 2.15 that, in the classical situation, we may use the Heine–Borel theorem to define a Scott-continuous map I that extends any open subset of X ≡ ℝ to one of Y ≡ Σ^{ℚ} × Σ^{ℚ}. The other foundational systems in which 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} (called a Σ-splitting) axiomatically whenever we define a subspace i : X ↣ Y, thereby taking account of the intended topology. It is important to understand that the types that are generated by the language 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]} that makes [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 : ℕ^{ℕ} ↣ Σ^{ℕ×ℕ} 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, ℕ^{ℕ} is not definable 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 subspace per paper. So far, it only gives a robust account of locally compact spaces, but there is work 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 theory of recursion on to the front of it. Domain theory can be developed within ASD [F], and then programming languages such as Plotkin’s PCF can be translated into this, using the denotational semantics 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”. The naï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 continuous functions [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 result of 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 this is unification, in which variables are assigned values according to the constraints imposed by the rest of the program, i.e. the values that they must have if the program is ever to terminate with a proof 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 that found 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 or something very similar, such as rationals. They cannot be real numbers, functions or predicates. Our choice principle is therefore only ℕ–ℕ for Σ_{1}^{0}-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.

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 made entirely within this calculus. We repeat that there is no underlying set theory, and that the monadic and Phoa principles are unalienable parts of the system. On the other hand, there are other 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 ℕ, 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 in particular not ℕ or ℝ), 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 ≠_{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 ⟨ , ⟩ and projections π_{0}, π_{1} for product types.

Discrete, Hausdorff, overt and compact spaces will be defined shortly. Existential quantification over ℕ or ℝ is allowed, but universal quantification is not. Universal quantification over the closed interval 𝕀 ≡ [0, 1] is justified in Section 10.

So examples of invalid logical formulae include

λn. n + 3, λx. ^{3} \sqrt{x}, π =_{ℝ} 3.14159, ∀n. ∃pq. 2n = p + q and ∀x. x^{2} ≠ −1,

but (∃npqr:ℕ. p^{n}+q^{n} = r^{n}) and (∀x:|x| ≤ 2. x^{2} < 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 ℕ → ℕ_{⊥} or ℝ → ℝ_{⊥} [D, F].

Binding, renaming, duplication, omission and substitution for variables are the same as in the λ- 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 to any depth — so long as their ranges are overt or compact spaces.

Axiom 4.3 The numerical terms of type ℕ 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 ℕ at any type X.

Definition 4.4 Judgements in the calculus are of the four forms

⊢ X type,  Γ ⊢ a : X,  Γ ⊢ a = b : X and Γ ⊢ α ⩽ β : Σ^{X},

asserting well-formedness of types and typed terms, and equality or implication of terms. We shall refer to a = b and α ⩽ β 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 Γ ⊢ α ⩽ β : Σ^{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

ϕ ⩽ ψ to mean ϕ ∧ ψ = ϕ, or equivalently ϕ ∨ ψ = ψ,

although for σ, τ : Σ we use σ ⇒ τ and σ ⇔ τ instead of σ ⩽ τ and σ = τ, since we shall also need 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 ℕ; 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 ⩽, =, ⇒ 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 ≠ 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 the form α_{2} ⇒ β_{1} ⊢ γ_{1} ⇒ δ_{0} instead. If we need another level of nesting, we use a proof rule:

{α_{3} ⇒β_{2} ⊢ γ_{2} ⇒ δ_{1} \atop ϵ_{2} ⇒ ζ_{1} ⊢ η_{1} ⇒ θ_{0}}

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 ⇒, ⇔, ⩽, = and finally ⊢. This reflects the hierarchy of 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 rules^{1}

Γ, σ ⇔ ⊤ ⊢ α ⇒ β ; = ; Γ ⊢ σ ∧ α ⇒ β  Γ, σ ⇔ ⊥ ⊢ β ⇒ α ; = ; Γ ⊢ β ⇒ σ ∨ α

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 a closed one. In symbols, for a : X,

a ∈ U (open) if ϕa ⇔ ⊤ and a ∈ C (closed) if ϕa ⇔ ⊥,

so U ⊂ U′ iff C′ ⊂ C iff ϕ ⩽ ϕ′. 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 and closed. 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 ℕ 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 of a 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 the bottom 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.

1Peter Aczel pointed out the resemblance to Gerhard Gentzen’s rules for negation in classical sequent calculus [Gen35].

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 discrete or 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 ≠_{H} k) ⇔ ⊥

Lemma 4.13 Equality has the usual properties of substitution, reflexivity, symmetry and transitivity, whilst inequality or apartness obeys their lattice duals:

\begin{aligned}ϕm ∧ (n = m) & ⇒ & ϕn & ϕh ∨ (h ≠ k) & ⇐ & ϕk \\ (n = n) & ⇔ & ⊤ & (h ≠ h) & ⇔ & ⊥ \\ (n = m) & ⇔ & (m = n) & (h ≠ k) & ⇔ & (k ≠ h) \\ (n = m) ∧ (m = k) & ⇒ & (n = k) & (h ≠ k) ∨ (k ≠ ℓ) & ⇐ & (h ≠ ℓ) \end{aligned}

(The proof of this uses Axiom 4.7.) In an overt discrete space, or a compact Hausdorff one, we have the converse of the first of the four rules:

∃m. ϕm ∧ (n = m) ⇔ ϕn ∀h. ϕh ∨ (h ≠ k) ⇔ ϕk.

When both =_{X} and ≠_{X} are defined, as they are for ℕ, they are complementary:

(n =_{X} m) ∨ (n ≠_{X} m) ⇔ ⊤  and  (n =_{X} m) ∧ (n ≠_{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 or compact 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 ℕ 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, then we 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 the Beck–Chevalley condition [Tay99, Chapter IX].

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

\begin{aligned}∃x. σ ∧ ϕx & ⇔ & σ ∧ ∃x. ϕx & (∀x. ϕx) ∧ (∃x. ψx) & ⇒ & ∃x. (ϕx ∧ ψx) \\ ∀x. σ ∨ ϕx & ⇔ & σ ∨ ∀x. ϕx & (∀x. ϕx) ∨ (∃x. ψx) & ⇐ & ∀x. (ϕx ∨ ψx) \end{aligned}

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:

⋁_{N} ≡ ∃_{N}^{X} : (Σ^{X})^{N} ≅ (Σ^{N})^{X} ⟶ Σ^{X} and ⋀_{K} ≡ ∀_{K}^{X} : (Σ^{X})^{K} ≅ (Σ^{K})^{X} ⟶ Σ^{X}.

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. ψ(fx) 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 ℕ is overt but not compact, each Σ^{X} has and each Σ^{f} preserves ℕ-indexed joins, but not ℕ-indexed meets.

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 write as Γ, 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:M} ϕ^{m} ≡ ∃n:N . α_{n} ∧ ϕ^{n} : Σ^{X}.

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 ℚ or inclusion of lists.

We shall also want to define both quantifiers over the closed interval [d, u], where d and u need not 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} ≡ ∃n. α_{n} ∧ ϕ^{n}

is called a directed join, if (a) (∃n. α_{n}) ⇔ ⊤, and (b) α_{n@m} ⇔ α_{n} ∧ α_{m} and ϕ^{n@m} ⩾ ϕ^{n} ∨ ϕ^{m} for some binary operation @ : N × N → N.

In this, α_{n} ∧ α_{m} means that both ϕ^{n} and ϕ^{m} contribute to the join, so for directedness in the informal sense, we require some ϕ^{n@m} to be above them both (contravariance), and also to count towards 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.

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 that

F (∃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 the subset M ≡ {n | α_{n}} ⊂ N. The principal use of this axiom in this paper is Proposition 7.12, where the ambient overt object N is ℚ, 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 the finitary connectives ⊤, ⊥, ∧ and ∨.

Definition 4.22 A term P of type Σ^{Σ^{X}} 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 we call 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 an inverse I, then so does i itself [Tay91].

Proof The map η : Y ↣ Σ^{Σ^{Y}} given by y ↦ λψ. ψy is mono, because focus_{Y} (λψ. ψ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 ≡ focus_{X}(λϕ. Iϕy). It satisfies

j(ix) = focus_{X} (λϕ. Iϕ(ix)) = focus_{X} (λϕ. I(Σ^{i}ϕ)x) = focus_{X}(λϕ. ϕx) = x
and λψ. ψ(i(jy)) = λψ. (Σ^{i}ψ)( focus_{X}(λϕ. Iϕy)) = λψ. I(Σ^{i}ψ)y = λψ. ψy ≡ η_{Y} y,

so i(jy) = y since η : Y ↣ Σ^{Σ^{Y}} is mono. □

For ℕ, 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 we shall see in Section 14 that Dedekind completeness expresses sobriety of ℝ.

Axiom 4.24 A predicate ϕn for n : ℕ (possibly involving other parameters) is called a description if it is “uniquely satisfiable” in the sense that

(∃n. ϕn) ⟺ ⊤ and (ϕn ∧ ϕm) ⟹ (n =_{ℕ} m)

are provable. Then we may introduce the n. ϕn : ℕ, with the same parameters, satisfying

ϕm ⟺ (m =_{ℕ} the n. ϕn).

Descriptions may be used to define general recursion (minimalisation) [A, D, O].

Proposition 4.25 All types that are definable from 1, Σ and ℕ using × and Σ^{(−)} are sober. Proof

(a) The only prime of type Σ^{Σ^{1}} is P ≡ λϕ. ϕ⋆, and focus_{1} P = ⋆.

(b) If P : Σ^{Σ^{ℕ}} is prime then ϕn ≡ P (λm. n =_{ℕ} m) is a description, and focus_{ℕ} P = the n. ϕn [A, Proposition 10.4].

(c) If X and Y are sober then so is X × Y, with

focus_{X×Y} P = ⟨ focus_{X} (λϕ. P (λp. ϕ(π_{0}p))), focus_{Y} (λψ. 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  discrete compact Hausdorff
ℕ × Σ  ✓  ×  ×  ×
ℝ, ℝ^{n}  ✓  ×  ×  ✓
Σ  ✓  ×  ✓  ×
𝕀, 2^{ℕ}  ✓  ×  ✓  ✓
free combinatory algebra  ✓  ✓  ×  ×
ℕ, ℚ  ✓  ✓  ×  ✓
Kuratowski finite  ✓  ✓  ✓  ×
finite (n)  ✓  ✓  ✓  ✓

the set of codes of

non-terminating programs  ×  ✓  ×  ✓

The axioms only provide the quantifiers ∀_{∅} ≡ ⊤, ∃_{∅} ≡ ⊥, ∀_{2} ≡ ∧, ∃_{2} ≡ ∨ and ∃_{ℕ} directly — it is the business of this paper to construct ∃_{ℝ}, ∃_{𝕀} and ∀_{𝕀}, in Sections 9 and 10. To put this the other 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 elimination in 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 of a λ-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 ⊂ Σ^{ℚ} × Σ^{ℚ} ≡ Y, where we shall construct R as the subspace of those pairs of predicates on ℚ that are 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 to introduce 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 from the 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.

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, just as 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_{Σ^{X}}  or  x : 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 be recovered (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 equaliser

[figure: X; i; Y; y ↦ λψ. ψy; y ↦ λψ. Eψy; Σ^{Σ^{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 membership of 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 parameters from Γ) 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 the surjective 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ψ) and E(ϕ ∨ ψ) = 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 the same role, namely to define subspaces, but the definitions are different. A localic nucleus, usually called j, must satisfy id ⩽ 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 is 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 this case E is a nucleus in both senses. If we view R instead as a subspace of Σ^{ℚ} × Σ^{ℚ}, but still defined by 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 in the 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 admit_{Y,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 of open 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 continuous function θ : Y → Σ. The open and closed subspaces that θ (co)classifies are the inverse images U ≡ θ^{−1}(⊤) and C ≡ θ^{−1}(⊥) of the two points of the Sierpiń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} ↓ θ ≡ {ψ | ψ ⩽ θ} 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 ⊂ Σ^{ℚ} × Σ^{ℚ} in Section 7 will involve an open subspace, a closed one and a retract.

Lemma 5.9 Let e : Y → Y be an idempotent and θ : Y → Σ any map. Then

Σ^{e},  θ ∧ (−)  and  θ ∨ (−)

are 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. Everything works if the nuclei commute, but this does not often happen. In fact, there are many situations in which E_{1} · E_{2} · E_{1} = E_{1} · E_{2}, and that is sufficient to justify forming the intersection.

Lemma 5.11 Let E_{1} and E_{2} be nuclei on a type Y such that either E_{1} · E_{2} = E_{2} · E_{1} or E_{1} · E_{2} · E_{1} = E_{1} · E_{2}. Then E_{1} · E_{2} is also a nucleus, and defines the intersection (pullback)

[figure: {Y | E_{1} · E_{2}}; {Y | E_{1}}; {Y | E_{2}}; Y]

in which all five inclusions (including the composite) are Σ-split. Regarding {Y | E_{1}} ⊂ Y as the subset of admissible elements, and Σ^{{Y |E_{1}}} as the subset {ψ : Σ^{Y} | E_{1}ψ = ψ}, we see E_{1} · E_{2} as a nucleus on {Y | E_{1}} but not necessarily on {Y | E_{2}}. □

We have already said that nuclei and Σ-splittings are intimately related to the quantifiers that define 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 Σ^{ℚ} ×Σ^{ℚ} ↓ (δ_{u}, υ_{d}) and (δ_{d}, υ_{u}) ↓ Σ^{ℚ} ×Σ^{ℚ}, 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. Then^{2}

(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 ⇒ σ  Γ, x : X ⊢ σ ⇒ ϕx
Γ, σ ⇔ ⊥ ⊢ Σ^{i}(Iϕ) ≡ ϕ = ⊥ : Σ^{X}  Γ, σ ⇔ ⊤ ⊢ ⊤ = ϕ ≡ Σ^{i}(Iϕ) : Σ^{X}
Γ, σ ⇔ ⊥ ⊢ Iϕ = ⊥ : Σ^{L}  Γ, σ ⇔ ⊤ ⊢ ⊤ = Iϕ : Σ^{L}
Γ, σ ⇔ ⊥ ⊢ ∃_{L}(Iϕ) ⇒ ⊥  Γ, σ ⇔ ⊤ ⊢ ⊤ ⇒ ∀_{L}(Iϕ)
Γ  ⊢ ∃_{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 roots of particular polynomials to a field, or set theorists construct “equiconsistent” models that have altered 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 type  y : Y, ψ : Σ^{Y} ⊢ Eψy : Σ  E is a nucleus
{Y | E} type

{}F

2This result was suggested by Alex Simpson.

Γ ⊢ a : Y Γ, ψ : Σ^{Y} ⊢ ψa ⇔ Eψa
Γ ⊢ admit_{Y,E} a : {Y | E}

{}I

x : {Y | E} ⊢ i_{Y,E}x : Y  {}E_{0}
x : {Y | E}, ψ : Σ^{Y} ⊢ ψ(i_{Y,E}x) ⇔ Eψ(i_{Y,E}x)  {}E_{1}
Γ ⊢ a : Y Γ, ψ : Σ^{Y} ⊢ ψa ⇔ Eψa
Γ ⊢ a = i_{Y,E}(admit_{Y,E} a) : Y

{}β

x : X ≡ {Y | E} ⊢ x = admit_{Y,E}(i_{Y,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 I_{Y,E} expands open subsets of the subspace to the whole space.

ϕ : Σ^{{Y |E}} ⊢ I_{Y,E}ϕ : Σ^{Y} .  Σ^{{}}E

The Σ^{{}}I rule is derived from {}E_{0}:

ψ : Σ^{Y} ⊢ Σ^{i}ψ ≡ λx:{Y | E}. ψ(i_{Y,E}x) : Σ^{{Y |E}}.  Σ^{{}}I

The β-rule says that the composite Σ^{Y} ^{Σ^{i}} [figure] Σ^{{Y |E}} ^{I} Σ^{Y} is E:

y : Y, ψ : Σ^{Y} ⊢ I_{Y,E}(λx:{Y | E}. ψ(i_{Y,E}x))y ⇔ Eψy.  Σ^{{}}β

The η-rule says that the other composite Σ^{{Y |E}} Σ^{Y} [figure] Σ^{{Y |E}} is the identity:

ϕ : Σ^{{Y |E}}, x : {Y | E} ⊢ ϕx ⇔ I_{Y,E}ϕ(i_{Y,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 is something 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 this is 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 = admit_{Y,E} ( focus_{Y} (Σ^{2}i_{Y,E}Q)).

(b) If X is also sober and has maps f : X → Y and F : Σ^{X} → Σ^{Y} with Σ^{f} · F = id_{Σ^{X}} and F · Σ^{f} = E then X ≅ {Y | E}, where

x : X  ⊢ x′ ≡ admit_{Y,E}(fx) : {Y | E}
x′ : {Y | E} ⊢ x ≡ focus_{X} (λϕ:Σ^{X} . F ϕ(ix′)) : X.

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 ℝ^{n}? Is it of any use in proving theorems in mathematics other than those that we have mentioned?

Actually, we have told the story so far in reverse historical order. The calculus above was derived from a categorical intuition, and when it was formulated [B], it was a solution in search of 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 a source 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}} | λFF . F (λx. F(λϕ. ϕx))}
{X | E_{0}} × {Y | E_{1}} ≅ {X × Y | E_{1}^{X} · E_{0}^{Y} }
Σ^{{X|E}}  ≅ {Σ^{X} | Σ^{E}}
{{X | E_{1}} | E_{2}}  ≅ {X | E_{2}}
{X | E_{0}} + {Y | E_{1}} ≅ {Σ^{Σ^{X}×Σ^{Y}} | E}
where EHH  ≡ H⟨λx. H(λϕψ. E_{0}ϕx), λy. H(λϕψ. E_{1}ψ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 the overt 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 ℕ, ℤ and ℚ;

(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 well known definitions using primitive recursion.

The infinite objects that are generated in this way are countable in the strict sense of being bijective with a decidable subset of ℕ in the calculus; since our isomorphisms are homeomorphisms, such objects inherit =, ∃, and in some cases ≠, from ℕ.

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 this subcategory is co-reflective, i.e. that the inclusion has a right adjoint, which formally assigns an overt 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 section is that we require the adjunction Σ^{(−)} ⊣ Σ^{(−)} to be monadic.

The notions of sobriety and Σ-split subspaces in ASD come from the two conditions in the theorem 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 λ-terms in [A, B].

In the presence of the other topological structure in the previous section, in particular Scott continuity, 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 ↣ Σ^{ℕ}, 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 is the part of the Phoa principle that applies to intuitionistic set theory or the subobject classifier in 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 that developed 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).

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) ⟺ (∃q. p < q < r)
(b) extrapolative (without endpoints): (∃p. p < q) ⟺ ⊤ ⟺ (∃r. q < r)
(c) linear (total or trichotomous):  (p ≠ q) ⟺ (p < q) ∨ (q < p).

The ∃q in the interpolation axiom does not necessarily mean the midpoint \frac{1}{2}(p + r). It might instead 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). This is the case when Q is countable (by which we mean strictly that Q ≅ ℕ, Remark 5.22), in which case the usual order on ℕ 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 ≠ 0, where “simpler” fractions have smaller denominators;

(b) dyadic or decimal fractions k/2^{n} and k/10^{n};

(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 for them, we shall refer to the elements of any such countable Q as rationals, but for a particular target computation any of the above structures may be chosen. We keep the dyadic rationals in mind 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 Q_{1} ≅ Q_{2} 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 Q_{1}, together with its simplest ordermatch from Q_{2}. At the next stage, we start with an absentee from Q_{2}. □

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 the Archimedean 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 that appears 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 two sides 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.

The ASD calculus does not allow negation of predicates. Nor, indeed, is there any kind of contravariant 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 predicates

for d, u : Q, δd, υu : Σ,

possibly involving parameters, such that

υu  ⇔ ∃t:Q. υt ∧ (t < u)  υ rounded upper
δd  ⇔ ∃e:Q. (d < e) ∧ δe  δ rounded lower
⊤  ⇔ ∃u:Q. υu  bounded above
⊤  ⇔ ∃d:Q. δd  bounded below
⊥  ⇔ δd ∧ (u < d) ∧ υu  disjoint
(d < u) ⇒ (δd ∨ υu)  order-located

We 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 (\underline{R}, \overline{R}, Example 2.8 and Definition 7.3). Lemma 7.5 explains why we have defined disjointness in this way, in preference to several others, and we shall discuss a stronger notion of locatedness that is needed for arithmetic in 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 a little 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:

[figure: Q; j; R; i; Σ^{Q} × Σ^{Q}; LHS; RHS; Σ^{Q} × Σ^{Q} × Σ × Σ × Σ^{Q×Q} × Σ^{Q×Q}]
[figure: (δ, υ)]
Γ^{a . . . . . . . . .}

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 a list of properties that a pair of predicates on Q may or may not have.

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 a statement (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 ↦ (δ_{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}) < (δ, υ) ⟺ δd and (δ, υ) < (δ_{u}, υ_{u}) ⟺ υu. □

We would like to show next that < is interpolative and extrapolative, but even to say that we need ∃_{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 three statements

δ ⩾ ϵ : Σ^{Q}, υ ⩽ τ : Σ^{Q} and ((δ, υ) < (ϵ, τ)) ⇔ ⊥

are equivalent. We write (ϵ, τ) ≤ (δ, υ) for any of them. Notice that the arithmetical order ≤ agrees with the logical one ⩽ 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 ϵ ⩽ δ or υ ⩽ τ, since cuts are rounded and disjoint.

Conversely, by the definition of ∃, another way of writing the statement with < is

for any q : Q, (υq ∧ ϵq) ⇒ ⊥

Then, for p : Q,

ϵp ⇔ ∃q. (p < q) ∧ ϵq  ϵ is rounded
⇒ ∃q. (δp ∨ υq) ∧ ϵq  (δ, υ) located
⇔ ∃q. (δp ∧ ϵq) ∨ (υq ∧ ϵq)  distributivity
⇒ ∃q. (δp ∨ ⊥) ≡ δp  hypothesis,

and similarly υp ⇒ τp. □

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 fact that 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 the variable length of the list, but the formal proof, of course, uses list induction. In particular, the ordering of the list is an open predicate that, like the n-fold conjunction, is easily definable by recursion 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 the other 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 q_{0} < q_{1} < ⋯ < q_{n} be a strictly ascending finite sequence of rationals, and let (δ, υ) be rounded, located and bounded, with δq_{0} and υq_{n}. Then this (pseudo-)cut belongs to at least one of the overlapping open intervals

(q_{0}, q_{2}), (q_{1}, q_{3}), …, (q_{n−2}, q_{n}),

in the sense that ⋁_{j=0}^{n−2}(δq_{j} ∧ υq_{j+2}).

Proof The hypotheses δq_{0} and υq_{n} and order-locatedness of (δ, υ) applied to each pair q_{j} < q_{j+1} give

δq_{0} ∧ (δq_{0} ∨ υq_{1}) ∧ (δq_{1} ∨ υq_{2}) ∧ ⋯ ∧ (δq_{n−1} ∨ υq_{n}) ∧ υq_{n},

which we expand using distributivity. Of the 2^{n} disjuncts, n+1 yield those in the claim, including two repetitions:

δq_{0} ∧ υq_{1} ∧ υq_{2} ∧ ⋯ ∧ υq_{n}  ⇒ δq_{0} ∧ υq_{2}
δq_{0} ∧ ⋯ ∧ δq_{j} ∧ υq_{j+2} ∧ ⋯ ∧ υq_{n} ⇒ δq_{j} ∧ υq_{j+2}
δq_{0} ∧ ⋯ ∧ δq_{n−2} ∧ δq_{n−1} ∧ υq_{n}  ⇒ δq_{n−2} ∧ υq_{n}.

Each of the remaining 2^{n} − n − 1 disjuncts consists of a conjunction of δs up to some δq_{j} and of υs starting from υq_{i}, 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

δq_{j} ∧ υq_{i} ⟹ δq_{j} ∧ υq_{j+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 ≠ 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 −∞ ≡ (⊥, ⊤). □

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 a china 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 ℝ 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, pick out 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 complicated when encoded via the bijection Q ≅ ℕ, 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 ℕ using ×, Σ^{(−)} and Σ-split subspaces, so we have to use Σ^{Q}(≅ Σ^{ℕ}) 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}.

Notation 7.1 For arbitrary δ, υ : Σ^{Q} and Φ : Σ^{Σ^{Q}×Σ^{Q}}, define

δ̂d ≡ ∃e. (d < e) ∧ δe,  υ̌u ≡ ∃t. υt ∧ (t < u),
B(δ, υ) ≡ ∃du. δd ∧ υu, ∇(δ, υ) ≡ ∃du. δd ∧ (u < d) ∧ υu

and E_{1}Φ(δ, υ) ≡ ∃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 < d in ∇!). We shall find three nuclei that define the interval domain, but E_{1} will turn out to be the most useful one.

Lemma 7.2 These operations δ ↦ δ̂ and υ ↦ υ̌ are idempotent. They fix δ and υ iff these are rounded (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

ˆ− : \underline{R} ◁ Σ^{Q} and ˇ− : \overline{R} ◁ Σ^{Q},

called the ascending and descending reals respectively. The product \underline{R} × \overline{R} is similarly a retract of Σ^{Q} × Σ^{Q}, so it is given by the nucleus

E_{r}Φ(δ, υ) ≡ Φ(δ̂, υ̌) ≡ Φ(λd. ∃e. d < e ∧ δe, λu. ∃t. υt ∧ t < u).

We may think of the lattice \underline{R} × \overline{R} as the space of “intervals” that may be infinite and even back-to-front (Remark 2.20).

Lemma 6.12 defines “inclusion” maps δ_{(−)} : Q → \underline{R} ◁ Σ^{Q} and υ_{(−)} : Q → \overline{R} ◁ Σ^{Q}. These can be extended to R → \underline{R} and R → \overline{R}, of course simply as the projections that extract δ and υ from the cut (δ, υ) : R. However, by monotonicity (Axiom 4.8), there is no map

\underline{R} → \overline{R},  \overline{R} → \underline{R},  \underline{R} → R  or  \overline{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 the one that is invariant under rounding, so that the nuclei commute, cf. Lemma 5.11.

Lemma 7.5 Let δ, υ : Σ^{Q}. Then ∇(δ, υ) ⇔ ∇(δ̂, υ̌) and E_{1}∇(δ, υ) ⇔ ⊥. Also, the statements (a,d,e,f) below are equivalent:

\begin{aligned}(a) & ∇(δ, υ) & ⇔ & ⊥ & (d) & ∇(δ̂, υ̌) & ⇔ & ⊥ \\ (b) & δd ∧ υu & ⇒ & d < u & (e) & δ̂d ∧ υ̌u & ⇒ & d < u \\ (c) & δq ∧ υq & ⇔ & ⊥ & (f) & δ̂q ∧ υ̌q & ⇔ & ⊥ \end{aligned}

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

⇔ ∃et. δe ∧ (t < e) ∧ υt ≡ ∇(δ, υ)
E_{1}∇(δ, υ) ≡ ∃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^{∞} ⊂ \underline{R} × \overline{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

E_{rd}Φ(δ, υ) ≡ ∇(δ̂, υ̌) ∨ Φ(δ̂, υ̌).

The inclusion map IR^{∞} → \underline{R} × \overline{R} provides the endpoints of any interval, but as ascending and descending 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 with specified 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(δ̂, υ̌) ⟺ E_{1}⊤(δ, υ).

Proof

B(δ̂, υ̌) ≡ ∃du. δ̂d ∧ υ̌u ⇔ ∃d < u′. δ̂d ∧ υ̌u′ ≡ E_{1}⊤(δ, υ)  u′ > d, u
≡ ∃detu. (d < e) ∧ δe ∧ υt ∧ (t < u)
⇔ ∃et. δe ∧ υt ≡ B(δ, υ).  □

Definition 7.8 The bounded interval predomain is the open subspace IR ⊂ IR^{∞} classified by B, so it consists of those (δ, υ) for which B(δ, υ) is true. By Lemma 5.9, IR ⊂ Σ^{Q} × Σ^{Q} is defined by the nucleus

E_{rdb}Φ(δ, υ) ≡ ∇(δ̂, υ̌) ∨ Φ(δ̂, υ̌) ∧ B(δ̂, υ̌),

which may be bracketed either way, since ∇ ⩽ 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 fact that [d, u] is compact, but R is not.

The following rule of inference will simplify matters a lot in the next section. Abstractly, it is just (monotonicity of) the I operator in Section 5 for the subspace IR ⊂ Σ^{Q} × Σ^{Q}.

Proposition 7.10 In proving any implication Φ ⩽ Ψ, 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 E_{1} to the result, in the sense that

{Γ, (δ, υ) : IR ⊢ Φ(δ, υ) ⇒ Ψ(δ, υ) \atop Γ, δ, υ : Σ^{Q} ⊢ E_{1}Φ(δ, υ) ⇒ E_{1}Ψ(δ, υ).}

Proof If d < u then (δ_{d}, υ_{u}) is rounded, bounded and disjoint, so

E_{1}Φ(δ, υ) ≡ ∃d < u. δ̂d ∧ υ̌u ∧ Φ(δ_{d}, υ_{u})
⇒ ∃d < u. δ̂d ∧ υ̌u ∧ Ψ(δ_{d}, υ_{u}) ≡ E_{1}Ψ(δ, υ).  □

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 E_{1}Φ ⩽ E_{1}Ψ, and indeed EΦ ⩽ EΨ, as we shall see in the next section. □

Next we invoke Scott continuity of Φ, cf. Lemma 2.16.

Proposition 7.12 If (δ, υ) are rounded and bounded then, for any Φ : Σ^{Σ^{Q}×Σ^{Q}},

Φ(δ, υ) ⟺ ∃du. δd ∧ υu ∧ Φ(δ_{d}, υ_{u}).

If (δ, υ) are also disjoint then Φ(δ, υ) ⟺ ∃d < u. δ̂d ∧ υ̌u ∧ Φ(δ_{d}, υ_{u}) ≡ E_{1}Φ(δ, υ). 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} ≡ δd and ϕ^{d} ≡ δ_{d} ≡ λx. x < d.

Then ∃d. α_{d} ⇔ ⊤ by boundedness, and the binary operation @ ≡ max satisfies

α_{d@e} ≡ δ( max(d, e)) ⟺ δd ∧ δe ≡ α_{d} ∧ α_{e}

as δ 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 the construction, 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 Proposition shows 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 to ensure that the extension exists, i.e. that we recover the given formula when we restrict back to the 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 endpoints of 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 the bounded 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 for arithmetic in Sections 11–13. Here we may complete the construction of the (bounded) interval (pre)domain in ASD:

Theorem 7.14 E_{1} is a nucleus (Definition 5.5), and (δ, υ) is admissible for it (Definition 5.7) iff it is rounded, bounded and disjoint, so IR ≅ {Σ^{Σ^{Q}×Σ^{Q}} | E_{1}}. Proof If (δ, υ) are rounded, bounded and disjoint, Φ(δ, υ) ⇔ E_{1}Φ(δ, υ) by Proposition 7.12, i.e. (δ, υ) is admissible. On the same hypothesis, therefore,

(Φ ∧ Ψ)(δ, υ) ⟺ (E_{1}Φ ∧ E_{1}Ψ)(δ, υ).

We deduce from this, using Proposition 7.10, that, for arbitrary (δ, υ),

E_{1}(Φ ∧ Ψ)(δ, υ) ⟺ E_{1}(E_{1}Φ ∧ E_{1}Ψ)(δ, υ),

which was one of the equations for a nucleus. We can prove the ∨-equation in the same way, or by observing that E_{1} is idempotent and preserves ∨.

Conversely, we have to deduce roundedness, boundedness and disjointness from instances of admissibility with respect to the new formula for E_{1}, using carefully chosen Φ, which are provided by Lemmas 7.5 and 7.7.

For disjointness, let Φ ≡ ∇, so by admissibility, ∇(δ, υ) ⇔ E_{1}∇(δ, υ) ⇔ ⊥.

For boundedness, let Φ ≡ λαβ. ⊤, so B(δ, υ) ⇔ E_{1}Φ(δ, υ) ⇔ Φ(δ, υ) ⇔ ⊤.

For roundedness, consider Φ ≡ λαβ. αc ∧ βw with c, w : Q, so

Φ(δ_{d}, υ_{u}) ⇔ δ_{d}c ∧ υ_{u}w ⇔ (c < d) ∧ (u < w).
Then  E_{1}Φ(δ, υ) ⇔ ∃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 ≡ Φ(δ, υ) ⇔ E_{1}Φ(δ, υ) ⇔ δ̂c ∧ υ̌w.  □

We conclude by looking at two other nuclei that also define IR.

Exercise 7.15 Show that

(a) E_{r} (Definition 7.3), E_{d} and E_{b} are nuclei, where

E_{r}Φ(δ, υ) ≡ Φ(δ̂, υ̌),  E_{d}Φ ≡ Φ ∨ ∇  and  E_{b}Φ ≡ Φ ∧ B;

(b) (δ, υ) is admissible for E_{r}, E_{b} or E_{d} 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) E_{r}, E_{b} and E_{d} commute pairwise (hint: use Lemmas 7.5 and 7.7);

(d) the composite E_{rb} ≡ E_{r} · E_{b} ≡ E_{b} · E_{r} is

E_{rb}Φ(δ, υ) ⟺ ∃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 E_{rdb} (Definition 7.8) is E_{rdb} = ∇ ∨ E_{1} (hint: use Axiom 4.7 with ∇(δ, υ) ⇔ ⊥ and Lemma 7.5).

We prefer E_{1} because it preserves ⊥, whereas E_{rdb}⊥ = ∇. We use this property in Theorem 9.2 to construct the existential quantifier. □

Exercise 7.16 Let E′_{1}Φ(δ, υ) ≡ ∃d < u. δd ∧ υu ∧ Φ(δ_{d}, υ_{u}) and show that

(a) E′_{1} is a nucleus;

(b) (δ, υ) is admissible for E′_{1} iff it is rounded, bounded and disjoint (hint: the only difficulty with copying the proof for E_{1} is that it only shows that admissible (δ, υ) are disjoint, bounded and satisfy δ ⩽ δ̂ and υ ⩽ υ̌, so a little more work is needed to deduce roundedness);

(c) E′_{1} also satisfies E′_{1} = E′_{1} · E_{r} = E′_{1} · E_{r} · E′_{1} ⩽ E_{1} = E_{r} · E′_{1} = E_{r} · E′_{1} · E_{r} ; but

(d) there are δ, υ : Σ^{Q} for which E_{1}⊤(δ, υ) ⇔ ⊤ and E′_{1}⊤(δ, υ) ⇔ ⊥ (hint: cf. Lemma 7.7). We prefer E_{1} because it commutes with E_{r} (cf. Lemma 5.11), so the Σ-splitting for IR ↣ Σ^{Q} × Σ^{Q} given by E_{1} restricts to IR ↣ \underline{R} × \overline{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 E_{1} on Σ^{Q} × Σ^{Q}, is the same as giving a nucleus E on the larger space for which

E · E_{1} = E = E · E = E_{1} · E.

Naturally, it will simplify the proof if we can restrict attention to (δ, υ) : IR, i.e. pseudo-cuts that are 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 ⩽ E = E^{2} and it preserves meets, so we have to prove that

Φ(δ, υ) ⇔ E_{1}Φ(δ, υ) ⇒ EΦ(δ, υ) and EΦ(δ, υ) ∧ 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 E_{1}. 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} and Σ^{Σ^{Q}×Σ^{Q}}, we may import it into the logic of ASD. However, we prefer to use

EΦ(δ, υ) ≡ ∃n ≥ 1. ∃q_{0} < ⋯ < q_{n}. δ̂q_{0} ∧ υ̌q_{n} ∧ ⋀_{k=0}^{n−1} Φ(δ_{q_{k}}, υ_{q_{k+1}}),

with δ̂ and υ̌ instead of δ and υ, and no n ≡ 0 term (which would be ∇). The reason is the same as for the choice of E_{1} in preference to E′_{1} or E_{rdb}, namely that it commutes with E_{r} and preserves ⊥ (Exercises 7.15f). Propositions 2.15 and 2.17 could be adapted to this choice by replacing I there with

IV ≡ {(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 “∃q_{0} < ⋯ < q_{n}” is existential quantification over List(Q), not just n + 1-fold quantification over Q.

Notice that E_{1} is the n ≡ 1 disjunct of E, so E_{1} ⩽ E.

We begin with some lemmas for managing the sequence.

Lemma 8.3 For any (δ, υ), suppose EΦ(δ, υ) holds by virtue of the sequence q_{0} < ⋯ < q_{n}, and that q_{0} ≤ r ≤ q_{n}. Then EΦ(δ, υ) also holds by virtue of the sequence obtained by inserting r. Proof If q_{k} < r < q_{k+1} then Φ(δ_{q_{k}}, υ_{q_{k+1}}) ⇒ Φ(δ_{q_{k}}, υ_{r}) ∧ Φ(δ_{r}, υ_{q_{k+1}}). □

Lemma 8.4 For any Φ, and understanding that q_{0} ≡ d and q_{n} ≡ u, the predicate

θ(d, u) ≡ ∃d < q_{1} < ⋯ < q_{n−1} < u. ⋀_{k=0}^{n−1} Φ(δ_{q_{k}}, υ_{q_{k+1}})

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 < q_{1} < ⋯ < q_{n−1} < u.

[⇐] If θ(d, u) holds by virtue of some sequence d = q_{0} < ⋯ < q_{n} = u, and d < e < t < u, then the same sequence with e and t in place of q_{0} and q_{n}, but omitting any q_{i} < 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).  □

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 then

EΦ(δ_{d}, υ_{u}) ⟺ ∃d < q_{1} ⋯ < q_{n−1} < u. ⋀_{k=0}^{n−1}Φ(δ_{q_{k}}, υ_{q_{k+1}}).

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})  and  EΦ(δ_{d}, υ_{u}) ⟺ ∃x:[u, d]. Φ(δ_{x}, υ_{x}).

Proof The expansion of EΦ(δ_{d}, υ_{u}) involves δ_{d}q_{0}∧υ_{u}q_{n} ≡ (q_{0} < d < u < q_{n}). So, by Lemma 8.3, we may assume that d and u occur in the given sequence, say as d ≡ q_{i}, u ≡ q_{j}. But then q_{0}, …, q_{i−2} and q_{j+2}, …, q_{n} are redundant, so without loss of generality d ≡ q_{1} and u ≡ q_{n−1}. Hence by Lemma 8.4,

EΦ(δ_{d}, υ_{u}) ⟺ ∃q_{0} < d < u < q_{n}. θ(q_{0}, q_{n}) ⟺ θ(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 E_{1}, which is IR. Notice that the expansion of E_{1}·E in the second result inherits the δ̂ and υ̌ from E_{1}, so they must also be used in the definition of E in order to obtain the equation E_{1} · E = E.

Lemma 8.6 E(E_{1}Φ)(δ, υ) ⟺ EΦ(δ, υ) and E_{1}(EΦ)(δ, υ) ⟺ EΦ(δ, υ). Proof The first part involves the conjuncts E_{1}Φ(δ_{q_{k}}, υ_{q_{k+1}}) that occur in the expansion of the formula for E(E_{1}Φ)(δ, υ). Such (δ_{q_{k}}, υ_{q_{k+1}}) are rounded, bounded and disjoint, so

E_{1}Φ(δ_{q_{k}}, υ_{q_{k+1}}) ⟺ Φ(δ_{q_{k}}, υ_{q_{k+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,

E_{1}(EΦ)(δ, υ) ≡ ∃d < u. δ̂d ∧ υ̌u ∧ EΦ(δ_{d}, υ_{u})
≡ ∃d < u. δ̂d ∧ υ̌u ∧ ∃d < q_{1} ⋯ < q_{n−1} < u. ⋀_{k=0}^{n−1}Φ(δ_{q_{k}}, υ_{q_{k+1}})
≡ EΦ(δ, υ).  □

Lemma 8.7 E^{2}Φ(δ, υ) ⟹ EΦ(δ, υ). Proof The outer E of E^{2} involves a sequence q_{0} < ⋯ < q_{n} and conjuncts EΦ(δ_{q_{k}}, υ_{q_{k+1}}) for each 0 ≤ k ≤ n − 1. By Lemma 8.5, the expansion of each of these involves a sequence

q_{k} = r_{k,0} < ⋯ < r_{k,m_{k}} = q_{k+1}

with conjuncts Φ(δ_{r_{k,j}}, υ_{r_{k,j+1}}). All of these sequences can be concatenated, to yield one that justifies 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 then

E⊤(δ, υ) ⟺ ⊤  and  EΦ(δ, υ) ∧ EΨ(δ, υ) ⟹ E(Φ ∧ Ψ)(δ, υ).

Proof As (δ, υ) are rounded and bounded, ⊤ ⇔ E_{1}⊤(δ, υ) ⇒ E⊤(δ, υ) by Lemma 7.7.

Suppose that EΦ and EΨ are justified by sequences q_{0} < ⋯ < q_{n} and r_{0} < ⋯ < r_{m} respectively. Let

d ≡ max(q_{0}, r_{0}) and u ≡ min(q_{n}, r_{m}),

so d is either q_{0} or r_{0}, which both satisfy δ, so δd holds, as similarly does υu. Since (δ, υ) are rounded and disjoint, d < u by Lemma 7.5. Now let

d ≡ s_{0} < ⋯ < s_{ℓ} ≡ u

be the union of the given sequences q_{0} < ⋯ < q_{n} and r_{0} < ⋯ < r_{m}, removing duplicates and those terms < d or > u. Such outlying points were already redundant in the expansion of EΦ(δ, υ) and of EΨ(δ, υ), whilst by Lemma 8.3 we may adjoin the members of one sequence to the other. Hence the new combined sequence serves for both EΦ(δ, υ) and EΨ(δ, υ), and therefore for E(Φ ∧ Ψ)(δ, υ) too. □

Proposition 8.9 E is a nucleus (Definition 5.5), as it satisfies, for Φ, Ψ : Σ^{Σ^{Q}×Σ^{Q}},

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

Proof For (δ, υ) : IR, Proposition 7.12 gives Φ(δ, υ) ⇔ E_{1}Φ(δ, υ) ⇒ EΦ(δ, υ), so

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

and EΦ(δ, υ) ∨ EΨ(δ, υ) ⇒ E(Φ ∨ Ψ)(δ, υ),

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

by Proposition 8.8. Then we use Proposition 7.10 to eliminate the hypothesis (δ, υ) : IR, and obtain the first inequality in each row:

E_{1}(Φ ∧ Ψ) ⩽ E_{1}(EΦ ∧ EΨ) ⩽ E(EΦ ∧ EΨ)
E_{1}(Φ ∨ Ψ) ⩽ E_{1}(EΦ ∨ EΨ) ⩽ E(EΦ ∨ EΨ)
E_{1}(EΦ ∧ EΨ) ⩽ E_{1}(E(Φ ∧ Ψ)) ⩽ E^{2}(Φ ∧ Ψ) ⩽ E(Φ ∧ Ψ)
E_{1}(EΦ ∨ EΨ) ⩽ E_{1}(E(Φ ∨ Ψ)) ⩽ E^{2}(Φ ∨ Ψ) ⩽ E(Φ ∨ Ψ).

The second inequality follows from E_{1} ⩽ E, and the third, E^{2} ⩽ E, is Lemma 8.7. Finally, from each E_{1}Θ ⩽ EΩ, we deduce EΘ = E(E_{1}Θ) ⩽ E^{2}Ω ⩽ EΩ by Lemmas 8.6 and 8.7. □

This fulfils the obligation that we have before invoking the ASD technology in Section 5, so we can now introduce the type R ≡ {Σ^{Σ^{Q}×Σ^{Q}} | 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Φ(δ, υ) ⟺ E_{1}Φ(δ, υ).

Proof [⇐] is trivial. For [⇒], we use Proposition 7.12 to widen the argument of each conjunct Φ a little towards the right, from [q_{k}, q_{k+1}] to [q_{k}, r_{k+1}], for any q_{k+1} < r_{k+1} < q_{k+2}:

EΦ(δ, υ) ≡ ∃q_{0} < ⋯ < q_{n}. δ̂q_{0} ∧ υ̌q_{n} ∧ ⋀_{k=0}^{n−1} Φ(δ_{q_{k}}, υ_{q_{k+1}})

⇒ ∃q_{0} < r_{0} < q_{1} < r_{1} < ⋯ < q_{n} < r_{n}. δ̂q_{0} ∧ υ̌r_{n} ∧ ⋀_{k=0}^{n−1} Φ(δ_{q_{k}}, υ_{r_{k+1}}),

where υ̌q_{n} ⇒ υ̌r_{n} because υ̌ is upper. As (δ̂, υ̌) is located with δ̂q_{0} and υ̌r_{n}, we may apply Lemma 6.16 to this sequence. Because of the alternation of letters, it gives

⋁_{k=0}^{n−1}(δ̂q_{k} ∧ υ̌q_{k+1}) ∨ ⋁_{k=0}^{n−1}(δ̂r_{k} ∧ υ̌r_{k+1}).

We already have the corresponding Φ(δ_{q_{k}}, υ_{q_{k+1}}) from the original abutting expansion, whilst the one with overlapping intervals provides

Φ(δ_{q_{k}}, υ_{r_{k+1}}) ⟹ Φ(δ_{r_{k}}, υ_{r_{k+1}}),

since δ_{q_{k}} ⩽ δ_{r_{k}}. Hence, with e ≡ q_{k} < t ≡ q_{k+1} or e ≡ r_{k} < t ≡ r_{k+1}, we have

EΦ(δ, υ) ⟹ ∃e < t. δ̂e ∧ υ̌t ∧ Φ(δ_{e}, υ_{t}) ≡ E_{1}Φ(δ, υ).  □

Lemma 8.11 If (δ, υ) is rounded and bounded, and EΦ(δ, υ) ⟹ E_{1}Φ(δ, υ) for all Φ, then (δ, υ) is located. Proof For any d < u, there is a sequence of rationals

q_{0} < d < q_{1} < u < q_{2} with δq_{0} and υq_{2}.

These numbers satisfy δ_{q_{0}}d ⇔ ⊥, υ_{q_{1}}u ⇔ ⊤, δ_{q_{1}}d ⇔ ⊤ and υ_{q_{2}}u ⇔ ⊥, so

∃q_{0} < q_{1} < q_{2}. δq_{0} ∧ υq_{2} ∧ (δ_{q_{0}}d ∨ υ_{q_{1}}u) ∧ (δ_{q_{1}}d ∨ υ_{q_{2}}u).

This is the n ≡ 2 disjunct of EΦ(δ, υ), where Φ(α, β) ≡ αd ∨ βu. By hypothesis, this implies E_{1}Φ(δ, υ), where

E_{1}Φ(δ, υ) ≡ ∃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 Φ(δ, υ) ⇔ E_{1}Φ(δ, υ) by Proposition 7.12. As it’s also located, EΦ(δ, υ) ⇔ E_{1}Φ(δ, υ) by Lemma 8.10, so (δ, υ) is admissible.

Conversely, admissibility of (δ, υ) for E with respect to both Φ and E_{1}Φ, give

Φ(δ, υ) ⟺ EΦ(δ, υ) ⟺ E(E_{1}Φ)(δ, υ) ⟺ E_{1}Φ(δ, υ),

where the middle implication is Lemma 8.6. Hence (δ, υ) is also admissible for E_{1}, so it is rounded, bounded and disjoint by Theorem 7.14. It is also located, by Lemma 8.11. □

Theorem 8.13 The type R ≡ {Σ^{Σ^{Q}×Σ^{Q}} | E} is the equaliser in Remark 6.9, i.e. its terms are Dedekind cuts, and the inclusion R ↣ Σ^{Σ^{Q}×Σ^{Q}} is Σ-split. □

In the following two sections, we shall show that this construction does make the real line Dedekindcomplete and the closed interval compact.

9 Dedekind completeness

In this section we shall prove Dedekind’s main result, that any cut of R corresponds to an element of 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 defined in Lemma 6.12 by q ↦ (δ_{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 true of 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} ⩽ δ_{t} and υ_{t} ⩽ υ_{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) ⇔ E_{1}Φ(⊤, ⊤) ⇔ 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 E_{1}, 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}) ≡ E_{1}Φ(⊤, ⊤)

by Proposition 7.12.

Finally, we can use Lemma 8.10 to interchange E and E_{1} in the definition of ∃, that is, EΦ(⊤, ⊤) ⇔ E_{1}Φ(⊤, ⊤), 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 by quantification 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).

Proof By Proposition 6.14, if a ≡ (δ, υ) and b ≡ (ϵ, τ) are cuts then

a = 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 to repeat 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 to show 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 ⊂ \underline{R} × \overline{R} in the same way in both versions.

Proposition 9.4 The maps Σ^{Q} ⇄ Σ^{R} given by

δ ↦ λr:R. ∃e:Q. r < je ∧ δe and λd:Q. Δ(jd) ← Δ

restrict to a bijection between rounded lower δ : Σ^{Q} and Δ : Σ^{R}. Hence the two constructions of \underline{R} agree. Those for \overline{R} do so too, with

υ ↦ λr:R. ∃t:Q. jt < r ∧ υt and λu:Q. Υ(ju) ← Υ.

Proof Recall from Lemmas 6.12f that jd <_{R} je ⇔ d <_{Q} e and (δ, υ) <_{R} ju ⇔ υu. Then

Δ ↦ δ ↦ λr. ∃e:Q. r < je ∧ Δ(je) = λr. ∃s:R. r < s ∧ Δ(s) ≡ Δ̂

by Theorem 9.2, and δ ↦ Δ ↦ λ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 (δ, υ), because

d <_{Q} u ⟺ jd <_{R} ju ⇒ Δ(jd) ∨ Υ(ju) ≡ δd ∨ υu.  □

Theorem 9.6 (R, <) is a Dedekind-complete dense linear order without endpoints, in the sense that 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 the elements 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, for example. 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. Then

R ↣ IR ↣ \underline{R} × \overline{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 the convergence 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) ⇔ max(a, b) < x  (a > x) ∧ (b > x) ⇔ min(a, b) > x
(a > x) ∨ (b > x) ⇔ max(a, b) > x  (a < x) ∨ (b < x) ⇔ min(a, b) < x
(a ≤ x), (b ≤ x) ⊣⊢ max(a, b) ≤ x  (a ≥ x), (b ≥ x) ⊣⊢ min(a, b) ≥ x. □

We have said that the two halves of a Dedekind cut play symmetrical roles. Adding an operation that 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 this has a unique fixed point (0):

⊖(δ, υ) ≡ (λd. υ(−d), λu. δ(−u)) 0 ≡ (λd. d < −d, λu. − u < u).

This agrees with Moore’s interval arithmetic, since ⊖(δ_{d}, υ_{u}) = (δ_{−u}, υ_{−d}). Since it preserves roundedness, it defines an isomorphism \underline{R} ≅ \overline{R} (Definition 7.3), but not an automorphism of either of them. Since it also preserves disjointness, boundedness and locatedness, we have ⊖ : IR ≅ IR and − : 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 ≠ 0) ≡ (δ0 ∨ υ0) ⇔ |x| ≠ 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.

10 Open, 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 à la Moore. The existential quantifier, on the other hand, is related 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 the first 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 𝕀 ≡ [0, 1], where d ≡ 0, u ≡ 1. But this is no real handicap, since (when we have some arithmetic) the general interval [d, u] with endpoints will be the direct image of [0, 1] under the function t ↦ d(1 − t) + ut. This actually generalises to all rounded bounded (δ, υ). The outcome is that the formulae that we obtain in the end 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 this section, 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 approach that 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 as the function. These operators are (Scott) continuous in the parameters, which means that we may still work with them in the vicinity of singularities of the equation, where the sets or types of zeroes are discontinuous.

Proposition 10.3 Any open subspace U ⊂ R classified by θ : Σ^{R} is overt. This applies in particular to the open intervals (d, u) and (υ, δ) in Definition 10.1. The existential quantifiers are defined 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 ⇒ σ
Γ, x : R, θx ⇔ ⊤ ⊢ ϕx ⇒ σ
Γ, x : R  ⊢ θx ∧ ϕx ⇒ σ  Axiom 4.7
Γ  ⊢ (∃x:R. θx ∧ ϕx) ⇒ σ  R overt

so ∃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 ⇔ E_{1}Φ(δ_{u}, υ_{d}) ⇔ EΦ(δ_{u}, υ_{d}) and ∀x:[d, u]. ϕx ⇔ EΦ(δ_{d}, υ_{u}),

where Lemma 8.10 allows us to interchange E with E_{1} in the existential quantifier, because the argument (δ_{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 find another 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 of Theorem 9.2. Since E_{1} preserves ⊥, this may also be seen as an application of Lemma 5.13 to the lattice \underline{R} × \overline{R} ↓ (δ_{u}, υ_{d}) of rounded pseudo-cuts with (δ, υ) ≤ (δ_{u}, υ_{d}). Recall that L ↓ α means {β : L | β ⩽ α}.

Proposition 10.5 The closed interval [d, u] is overt, with ∃x:[d, u]. Φ(ix) ≡ E_{1}Φ(δ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}) ⇒ σ.

The inequalities on the left of the ⊢ are equivalent to

d ≤ 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 ⊢ E_{1}Φ(δ_{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} ⩽ δ & υ_{u} ⩽ υ}.

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 In the upward direction, let (δ, υ) ≡ (δ_{x}, υ_{x}) ⩾ (δ_{d}, υ_{u}) be the cut corresponding to x : R. Then

Γ ⊢ σ ⇒ Iϕ(δ_{d}, υ_{u}) ⇒ Iϕ(δ, υ) ≡ Iϕ(ix) ⇔ ϕx.

For the converse, first let ψ ≡ λx. (x > u ∨ x < d) : Σ^{R} and Ψ ≡ λαβ. αu ∨ βd : Σ^{Σ^{Q}×Σ^{Q}}, 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 have

E(Φ ∨ Ψ)(δ_{d}, υ_{u}) ⇔ E⊤(δ_{d}, υ_{u}) ⇔ ⊤

by Lemma 8.5. In the expansion of E(Φ ∨ Ψ)(δ_{d}, υ_{u}), the same Lemma uses conjuncts like

(Φ ∨ Ψ)(δ_{q_{k}}, υ_{q_{k+1}}) ⇔ Φ(δ_{q_{k}}, υ_{q_{k+1}}) ∨ (u < q_{k} ∨ q_{k+1} < d) ⇔ Φ(δ_{q_{k}}, υ_{q_{k+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. ⋀_{k=0}^{n−1}Φ(δ_{q_{k}}, υ_{q_{k+1}})
⇐ Φ(δ_{d}, υ_{u})
Φ(ix) ≡ Φ(δ_{x}, υ_{x}) ⇒ ∃d < x < u. Φ(δ_{d}, υ_{u})
⇒ ∃d < x < u. ∀y:[d, u]. Φ(iy) ⇒ Φ(ix)
∃x:[d, u]. Φ(ix)  ⇔ E_{1}Φ(δ_{u}, υ_{d})
⇔ ∃et. t < u ∧ d < e ∧ Φ(δ_{t}, υ_{e})
⇒ Φ(δ_{u}, υ_{d}),

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 write

Φ : Σ^{Σ^{Q}×Σ^{Q}}, d ≤ u : R ⊢ ∃d ≤ x ≤ u. Φ(ix) ≡ EΦ(δ_{u}, υ_{d}).

This is because (∃d ≤ x ≤ u. ⊤) ⇔ ⊤ ⊣⊢ (d ≤ u) ⊣⊢ (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 meaning to ϕ(∞) ≡ lim_{x→∞}ϕ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 the cover be finite, but in what it says about the notion of covering. Recall how the statement of equality 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}) ⇔ ⊤.

Now, λϕ. ∀x:[d, u]. ϕx is a term in the ASD λ-calculus of type Σ^{Σ^{R}}, 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.

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 we have 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 other constructive systems. The computational implementation only produces ℓ or δ in the case where the predicate (is provably true and) has at worst variables of type ℕ (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 to consider are extremely well known as folklore, but we do not know of a published account that considers 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]. Even in the classical situation, the proof that the positive and negative reals form a commutative ring or field involves either an explosion of cases or considerable ingenuity. One ingenious solution is John 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 is application. 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.

There is a unique “inclusion” map ℤ ⊂ Q that preserves and reflects =, <, 0, 1, +, − and ×.

Axiom 11.2 Q obeys the Archimedean principle, for p, q : Q,

q > 0 ⟹ ∃n:ℤ. 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 ℤ (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 and multiplication 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  u + t < z  a < d × u  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 as an 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) three variables, our first task is to define the objects R^{2} and R^{3}. By R^{n} here we simply mean the product of 2, 3, … copies.

Proposition 11.5 The product spaces R^{n} exist, and they are overt, with ∃_{R^{n}} = ∃_{Q^{n}}. Proof Axiom 4.1 gives product types, and by Lemma 9.1 the quantifiers are given by

∃(x, y):R^{2}. ϕ(x, y) ≡ ∃x:R. ∃y:R. ϕ(x, y)
⇔ ∃x:Q. ∃y:Q. ϕ(x, y) ≡ ∃(x, y):Q^{2}. ϕ(x, y).  □

Remark 11.6 Now we have a diagram that combines those in Remarks 2.13 and 6.9,

[figure: Q^{2}; R^{2}; (Σ^{Q} × Σ^{Q})^{2}; Σ^{S×2}; Q; ∗; R; . . . . . . . . . . . . . . . . .; Σ^{Q} × Σ^{Q}; ⊛; Σ^{S}]

where denotes an equaliser and S ≡ Q + Q + 1 + 1 + Q × Q + Q × Q.

This means that a term of type R^{2} 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. R^{2} is, in fact, a Σ-split subspace [B], though the splitting I_{2} is not simply the square of that for R. But that does not matter, as we shall not need it anyway.

Exercise 11.7 By analogy with Proposition 2.15, find I_{2} : Σ^{R×R} ↣ Σ^{Σ^{Q}×Σ^{Q}×Σ^{Q}×Σ^{Q}}.

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 the rationals, 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 the composites R^{2} ⇉ Σ^{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 account of 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 another explosion 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 ⇔ ∃d′. (d′ < d) ∧ (a < d′ + e), for which we choose d′ with a − e < d′ < 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 [\underline{x}, \overline{x}], and

x ⋐ y ≡ [\underline{x}, \overline{x}] ⊂ (\underline{y}, \overline{y}) ≡ \underline{y} < \underline{x} ∧ \overline{x} < \overline{y}

for the strict containment relation that relates the basic compact subspace [\underline{x}, \overline{x}] to the basic open one (\underline{y}, \overline{y}), cf. [K]. (Beware that ⋐ corresponds to ≫ in the bounded interval predomain IR, which is a continuous dcpo.) Then the condition for ⊛ to be well defined is

x ⊛ y ⋐ w ⟺ ∃x′y′. x ⋐ x′ ∧ y ⋐ y′ ∧ x′ ⊛ y′ ⋐ w.

Note that ∃ here ranges over the names of the intervals, i.e. over {(d, u) | d ≤ u} ⊂ Q^{2}, which is a discrete space, not over the domain IR, since ⋐ is not defined there as an ASD predicate in the sense 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 x′ and y′ 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 α\underline{w} ∧ σ\overline{w} ≡ ∃xy. δ\underline{x} ∧ υ\overline{x} ∧ ϵ\underline{y} ∧ τ\overline{y} ∧ x ⊛ y ⋐ 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 have just given. We also get disjointness for free:

Lemma 11.12 Let α, σ : R^{n} ⇉ Σ^{Q} be “disjoint” on Q^{n}, in the sense that

a, z : Q, q⃗ : Q^{n} ⊢ αq⃗a ∧ (z < a) ∧ σq⃗z ⇒ ⊥.

Then they are also disjoint on R^{n} in the same sense, cf. Proposition 9.5. Proof By Proposition 11.5, αx⃗a ∧ (z < a) ∧ σx⃗z ⇒ ∃q⃗. αq⃗a ∧ (z < a) ∧ σq⃗z ⇒ ⊥. □

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 same d, e, u, t. It is bounded because (δ, υ) and (ϵ, τ) are bounded, and by extrapolation in (Q, <). It is disjoint 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 : ℕ.

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 any x ≡ (δ, υ) : R, there must be d, u : Q with x − \frac{1}{2}p < d < x < u < x + \frac{1}{2}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.

Proof By boundedness, δd∧υu for some d < u : Q. Then the Archimedean principle gives some k : ℕ with u − d < khp, where 0 < h + h < 1 by Lemma 11.4. So q_{j} ≡ d + jhp satisfy

q_{0} ≡ d < q_{1} < q_{2} < ⋯ < q_{k−1} < q_{k} > u,

to which we may apply Lemma 6.16, as (δ, υ) is order-located with δq_{0} and υq_{k}. This gives δe ∧ υt ∧ (t − e < p), where e ≡ q_{j}, t ≡ q_{j+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, to give 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 of the 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 Q^{n} to R^{n}.

Lemma 11.18 For f, g : R^{n} ⇉ R,

if q⃗ : Q^{n} ⊢ f(q⃗) ≤ g(q⃗) : R then x⃗ : R^{n} ⊢ f(x⃗) ≤ g(x⃗) : R.

Proof In traditional notation, since R is Hausdorff and f, g are continuous, the subspace

C ≡ {x⃗ : R^{n} | f(x⃗) ≤ g(x⃗)} ⊂ R^{n}

on which the laws actually hold is closed; on the other hand, Q^{n} ⊂ R^{n} is dense, whilst Q^{n} ⊂ C by hypothesis, so C = R^{n}. 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. □

12 Multiplication

We would like to develop multiplication in a way that follows addition as closely as possible. In that case, Example 11.9 showed that the extension of the Moore operation is well defined, and Lemma 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 ≤ 0  0 ≤ d
[d, u] ⊗ [e, t] u ≤ 0 u ≥ 0 u ≤ 0 u ≥ 0
0 ≤ t [ dt, ue] [ dt, ut] [ de, ue] [ de, ut]
0 ≤ e
t ≤ 0 [ ut, ue] [0, 0]  [q, p] [ de, dt]
0 ≤ t [ dt, de] [p, q]  [0, 0] [ ue, ut]
e ≤ 0
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, \underline{R}:

(a) constants;

(b) multiplication by q ≥ 0: δ ↦ λ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 \overline{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 \underline{R} → \underline{R} etc., by the previous lemma, and it’s enough to check this componentwise.

Alternatively, we may follow Example 11.9 directly:

a < [d, u] ⊗ [e, t] < z means a < 0, de, dt, ue, ut , min(dt, ue), max(de, ut) < z

in various cases, in each of which there is d′ < d, e′ < e, t < t′ or u < u′ with the same property.

3We computed the table ourselves with the help of Chris Stone, before we obtained a copy of [Kau80], and then checked that they agree.

Hence we have a map (\underline{R} × \overline{R}) × (\underline{R} × \overline{R}) → (\underline{R} × \overline{R}), but \underline{R} and \overline{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 widths of 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 look at 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 them to 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 and then dividing to give an integer quotient. Proposition 12.7 is the same idea in abstract form; in the 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 > 0 then 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′ : ℤ, q(k − 1) < a < q(k + 1) and q(k′ − 1) < z < q(k′ + 1).

Then 4q < z−a < q(k′+1)−q(k−1), so k < k′−2 by the previous lemma. Hence m ≡ k+1 < k′−1, where m : ℤ ⊂ Q, has the required property.

In the second case, the Archimedean principle for 8q (as p) and z − a (as q) provides k : ℤ with 8q < 2n(z − a), and then 0 < k < 2^{n} for some n : ℕ. Let h satisfy 0 < h + h < 1 (Lemma 11.4). Then

4q′ ≡ 4qh^{n} < kh^{n}(z − a) < (2h)^{n}(z − a) < (z − a),

for which the first case gives a < m′q′ = m′qh^{n} < z, so m ≡ m′h^{n} is the required approximate quotient. □

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, with any 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 a′ with 0, a ≤ max(0, a) < a′ < z, so αa′ ∨ σz by the foregoing 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. Note that we can bound a product away from zero iff we can do so for both factors, and in that case the previous result applies. The point of the fifth case below is therefore to constrain the product to 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 the definition 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 ≡ −1 < x < +1 ≡ δd ∧ υu,  where d ≡ −1, u ≡ +1
a < −|y| ≡ ∃et. ϵe ∧ τt ∧ (a < e) ∧ (a < −t)
a < xy ⇐ ∃duet. δd ∧ υu ∧ ϵe ∧ τt ∧ a < min(de, dt, ue, ut).  □

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 sets

D ≡ {d | ∃n:ℕ. d < n} and U ≡ {u | ∀n:ℕ. n < u}

form a Dedekind cut that is located only in the weaker order-theoretic sense: since every u − d is infinite, (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 use of 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 the debate at the time over the axiomatics of Euclid, but there is also a lot of extraneous discussion that 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 limit of 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 this paper.

Remark 12.13 What does this argument say about Conway’s number system? Recall that it is a proper class. Although the class D above is equivalent as a left cut to the set ℕ, 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 the other hand, U consists of infinite or non-terminating numbers, so it is the canonical example of a non-overt subspace in recursion theory. Since U is not overt, it’s not open, so it’s not defined by a 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 “real line” in ASD. This is a difficult but intriguing problem in recursion theory. Careful study of John 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 the definition 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 and arithmetic 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. □

13 Reciprocals and roots

Arithmetic, of course, provided one of the principal reasons for introducing Dedekind cuts in the first place, namely the solution of (algebraic and other) equations. Equations involving general continuous 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. This is 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 ↦ x^{5/3}, exp and log are equally simple examples. A particular problem of this kind 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 Q_{1} ↔ Q_{2} between dense linear orders without endpoints (Definition 6.1) is a pair (<, <) of binary relations that satisfy

\begin{aligned}∃b. a <_{1} b < x & ⇔ & a < x & ⇔ & ∃y. a < y <_{2} x \\ ∃b. x < b <_{1} a & ⇔ & x < a & ⇔ & ∃y. x <_{2} y < a \\ ∃x. a < x < b & ⇔ & a <_{1} b x <_{2} y & ⇔ & ∃a. x < a < y \end{aligned}

where a, b : Q_{1} and x, y : Q_{2}. These objects could, for example, consist of just positive rationals, or carry the opposite of the usual order. Let R_{1} and R_{2} 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 R_{1} ≅ R_{2} by

f(δ, υ) ≡ (λe. ∃d. e < d ∧ δd, λt. ∃u. u < t ∧ υu)
g(ϵ, τ) ≡ (λd. ∃e. d < e ∧ ϵe, λu. ∃t. t < u ∧ τt),

for which a < x ⟺ a <_{1} fx ⟺ ga <_{2} x and x < a ⟺ fx <_{1} a ⟺ x <_{2} ga. Proof The first four axioms make f(δ, υ) and g(ϵ, τ) rounded if (δ, υ) and (ϵ, τ) are. The other two 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 and reciprocals 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 Q_{1} ≡ Q_{2} ⊂ Q be its open subspace of positive elements. Then

a <_{1} b ≡ a < b,  x <_{2} y ≡ x > y,  a < x ≡ ax < 1,  x < a ≡ 1 < ax

define a strictly monotone graph Q_{1} ↔ Q_{2}. Proof Approximate division provides the six conditions

\begin{aligned}∃b. a < b ∧ bx < 1 & ⇔ & ax < 1 & ⇔ & ∃y. ay < 1 ∧ y > x \\ ∃b. 1 < bx ∧ b < a & ⇔ & 1 < ax & ⇔ & ∃y. x > y ∧ 1 < ay \\ ∃x. ax < 1 < bx & ⇔ & a < b x > y & ⇔ & ∃a. ay < 1 < ax, \end{aligned}

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 ≠ 0 by

(δ, υ)^{−1} ≡ (λd. ∃u. υu ∧ ((du < 1 ∧ δ0) ∨ (1 < du ∧ d < 0)),
λu. ∃d. δd ∧ ((du < 1 ∧ u > 0) ∨ (1 < du ∧ υ0))).

In the strictly positive or negative cases this is respectively

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

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

Proof The previous two results define an involution on {x : ℝ | x > 0}. If Q is a field then this agrees with the reciprocal on Q and with Moore’s formulae (Definition 2.3) in the legitimate case 0 < 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 the interval [−∞, +∞].

More generally, the reciprocal of a general (and possibly back-to-front) interval with endpoints is given by

\begin{matrix}[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}], \end{matrix}

illustrating the one-sided nature of Scott continuity: over d ≤ 0 for the ascending real number d and 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 − \frac{1}{2} < d < z < u < z + \frac{1}{2} for some d, 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 : ℕ,

(0 < d < u) ⇒ ∃x:Q. d < x^{2n} < u
(d < u)  ⇒ ∃x:Q. d < x^{2n+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

fe < d < u < ft ⟹ ∃x:[e, t]. d < fx < u.

The usual proof is that the non-empty open subspaces

D ≡ {x | fx < u}  and  U ≡ {x | d < fx}

cover the interval [e, t], and so must intersect. This is one of the ways of saying that the real interval is connected, which we prove for ASD in [J]. As the intersection is open, it must contain a rational.

The result is applicable to fx ≡ x^{2n} when we put

e ≡ \{ \begin{matrix}d & if 0 < d < 1 \\ \frac{1}{2} & if \frac{1}{2} < d \end{matrix} and  t ≡ \{ \begin{matrix}u & if 1 < u \\ 2 & if u < 2 \end{matrix}

and to fx ≡ x^{2n+1} when we put

e ≡ \{ \begin{matrix}d & if d < −1 \\ −2 & if − 2 < d \end{matrix}  and  t ≡ \{ \begin{matrix}u & if 1 < u \\ 2 & if u < 2. \end{matrix}  □

Proposition 13.8 R has (2n + 1)st roots and [0, ∞) has 2nth roots, where

\sqrt[2n+1]{(δ, υ)} ≡ (λd. δ(d^{2n+1}), λu. υ(u^{2n+1}))
+ ^{2n} \sqrt{(δ, υ)} ≡ (λd. (d < 0) ∨ δ(d^{2n}), λu. (u > 0) ∧ υ(u^{2n})).

In the illegitimate case, \sqrt{−1} = 0. Proof The strictly monotone graph is given by the relations (a < x^{m}) and (x^{m} < a), where m ≡ 2n or 2n + 1. If a < x^{m} and 0 < x then, by m-fold application of roundedness of division,

∃0 < y_{1}, y_{2}, …, y_{m} < x. max(0, a) < y_{1}y_{2} ⋯ y_{m} < ⋯ < y_{1}y_{2}x^{m−2} < y_{1}x^{m−1} < x^{m},

so a < y^{m}, where 0 < y ≡ max(y_{1}, …, y_{m}) < x. Similarly if 0 < x and x^{m} < a then ∃y > x. y^{m} < a, whilst if m ≡ 2n + 1 and x < 0 then we switch the signs. Approximate roots provide the fifth interpolation property, and also the case x ≡ 0, since Q has decidable equality. The other conditions are trivial. □

Finally, we leave the interested reader to use this method to develop the exponential and logarithm functions ℝ ⇄ (0, ∞) with base b, using 0 < d < b^{k·2^{−n}}< u.

14 Axiomatic completeness

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

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

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

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

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

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

Lemma 14.2 If d < u in an Archimedean ordered field R then there is some q : ℚ with d < q < u, and we may choose it to be dyadic, i.e. of the form q ≡ k · 2^{−n} with k, n : ℤ. Proof First apply the Archimedean axiom to q ≡ u − d > 0 and p ≡ 2, giving m, n : ℤ with

(m − 1)(u − d) < 2 < (m + 1)(u − d) < 2^{n}(u − d).

Then use it again with q′ ≡ 2^{−n}, giving k : ℕ with

d < u − 2 · 2^{−n} < k · 2^{−n} < u < (k + 2) · 2^{−n}.  □

Proposition 14.3 Let R be an Archimedean ordered field. Then there is a mono ℓ : R ↣ ℝ that fixes ℚ, and preserves and reflects <. Proof For x : R, consider δ_{x}, υ_{x} : Σ^{ℚ}, defined by δ_{x}d ≡ (d <_{R} x) and υ_{x}u ≡ (x <_{R} u). Since ℚ → R preserves and reflects order, for x : ℚ, these formulae agree with Lemma 6.12.

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

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

x <_{R} y ⟺ ∃q:ℚ. x <_{R} q <_{R} y ≡ ∃q:ℚ. δ_{x}q ∧ υ_{x}q ≡ ℓx <_{ℝ} ℓy,

so the order relations <_{R} and <_{ℝ} agree, and (as they are total) the map ℓ is mono. □

Theorem 14.4 If R is a Dedekind-complete Archimedean ordered field then the map ℓ in the previous result is an isomorphism. Definition 1.1 therefore characterises ℝ uniquely up to unique isomorphism. Proof Members of ℝ are by definition Dedekind cuts of ℚ, which extend to cuts of R as in Proposition 9.5. These define members of R since it is Dedekind-complete. Since all of the orders agree, this process is inverse to the construction of ℓ. □

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

Proposition 14.5 For x : R and ϕ : Σ^{R}, ϕx ⟺ ∃du. (d < x < u) ∧ ∀y:[d, u]. ϕy. Proof Whilst Corollary 10.8 has already shown that the Dedekind reals ℝ (as we have constructed them) satisfy this property, we claim here that it also follows from Definition 1.1. This is proved in detail in [J]. The key point is that, since [−1, +1] ⊂ R is compact, Hausdorff and totally ordered,

ϕx ⟹ ∀h:[−1, +1]. ∃δ > 0. (|h| > δ ∨ ϕ(x + h)),

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

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

Proof By Proposition 14.5 and Lemma 14.2,

∃x:R. ϕx ⇒ ∃dux:R. (d < x < u) ∧ ∀y:[d, u]. ϕy ⇒ ∃q:Q. ϕ(jq) ⇒ ∃x:R. ϕx.  □

Proposition 14.7 Σ^{ℓ} : Σ^{ℝ} ≅ Σ^{R}. Proof As in Proposition 2.15, we define, for ϕ : Σ^{R},

Iϕ ≡ λδυ:Σ^{ℚ}. ∃d < u:ℚ. δd ∧ υu ∧ ∀y:[d, u]. ϕy : Σ^{Σ^{ℚ}×Σ^{ℚ}},

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

Iϕ(ℓx) ≡ Iϕ(δ_{x}, υ_{x}) ≡ ∃du. (d <_{R} x <_{R} u) ∧ ∀y:[d, u]. ϕy ⇔ ϕx,

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

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

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

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

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

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

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

(a) ℝ-introduction: given a cut (δ, υ) : Σ^{ℚ} × Σ^{ℚ}, we introduce a real number cut(δ, υ) : ℝ;

(b) ℝ-elimination: given a real number a : ℝ and rationals d, u : ℚ, we eliminate a in favour of (d < a), (a < u) : Σ, along with the other rules concerning the order <;

(c) ℝ-beta: δd ⇔ (d < cut(δ, υ)) and υu ⇔ ( cut(δ, υ) < u);

(d) ℝ-eta: a = cut(λd. d < a, λu. a < u).

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

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

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

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

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

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

[cut(δ, υ)/x]^{∗}σ ⟺ (λx. σ) cut(δ, υ) ⟺ ∃d < u:ℚ. δd ∧ υu ∧ ∀x:[d, u]. σ.

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

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

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

(δ, υ) ≡ (λd. P (λx. d < x), λu. P (λx. x < u))

is a Dedekind cut, with cut(δ, υ) = 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 bounded because

P (λ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). □

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

⊥ ⟺ ∀x:[0, 1]. ωx  and  x ≠ y ⟹ ωx ∨ ωy.

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

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

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

ω ≡ δ ∨ υ  and  P ϕ ≡ ∃d < u. δd ∧ υu ∧ ∀x:[d, u]. ϕx.

Expressing any co-description ω as a Dedekind cut is a special case of the characterisation of connected subspaces of ℝ in [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 such an important property for a topological space to have, and partly because there are several schools of 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 computable maps between computably based locally compact spaces. On the other, Section 10 proved that the closed interval is compact. If all functions are computable, then surely we should be able to use 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 \frac{1}{2}. It can be shown that no finite sub-cover of a singular cover 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 CT_{0} [TvD88, §3.3.2], which states that every function ℕ → ℕ has a Gödel code. (With hindsight, it would have been more natural to enumerate ℕ → ℕ_{⊥}, but this is the way in which CT_{0} is usually stated.) It follows that every real number has a Gödel code, too. In classical recursion theory, a singular cover is described as a computable 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 Σ^{ℕ}, as in Section 4. An example is the category Dcpo of posets with directed joins and Scott-continuous functions. Here the equaliser carries the discrete (“specialisation”) order, but in this 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 in 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 computable ones. Each space is also equipped with a “computability” structure, such as an enumeration of basic open sets, that is used to specify which continuous maps are computable. Examples are (one variant of) Type Two Effectivity [Wei00], and computable equilogical spaces [Bau00]. Another is Martín Escardó’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 classical one. In particular, Escardó 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, but will 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, by following the usual construction, we could define a sequence of intervals with rational endpoints, (a_{n}, b_{n}), whose total length is bounded by \frac{1}{2}, and prove the meta-theorem that

“if ⊢ t : [0, 1] then ⊢ ∃n:ℕ. a_{n} < t < b_{n}”.

However, it does not follow that (a_{n}, b_{n}) covers [0, 1], by which we mean

x : [0, 1] ⊢ ∃n:ℕ. a_{n} < x < b_{n},

because that would be to confuse a family of theorems about all definable closed terms t with a single 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 CT_{0} 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 of ℕ, products, equalisers and exponentials. For Σ we take the object of semidecidable propositions.

This yields a valid interpretation of the language and construction of Sections 4 and 6, so that the equaliser 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 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 recursive functions ℕ → ℕ 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 ℕ → 2.

In the effective topos we can reformulate Friedberg’s example by saying that the topology of 2^{ℕ} (i.e. the object Σ^{2^{ℕ}}) is not the subspace topology induced by the inclusion 2^{ℕ} ⊂ 2_{⊥}^{ℕ}. In this topos, 2^{ℕ} is actually homeomorphic to ℕ^{ℕ}, so neither of these spaces can be locally compact, and their topology is not the subspace topology of 2_{⊥}^{ℕ}.

In the construction of 2^{ℕ} in ASD [L], on the other hand, the space 2_{⊥}^{ℕ} of partial functions from ℕ to 2 plays a role similar to that of IR in Sections 7–8, being a closed subspace of Σ^{ℕ} ×Σ^{ℕ}. Then 2^{ℕ} ⊂ 2_{⊥}^{ℕ} is defined by a nucleus that satisfies both the ASD and localic definitions. The quantifier ∀ that says that 2^{ℕ} is compact is obtained from this nucleus in a similar way to that for [d, u].

Escardó [Esc04] has shown how ∀ for 2^{ℕ} 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 and hard 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 on other 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 and powers Σ^{X}. Suppose also that idempotents split in C. Then A^{op} is a model of ASD, where A is the category of Eilenberg–Moore algebras for the monad arising from Σ^{(−)} ⊣ Σ^{(−)} [B]. □

Remark 15.9 Any category that results from this construction contains (the sober objects of) the original 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 functions, we obtain the category LKLoc of locally compact locales. It would be interesting and fruitful to do this in detail for the other cases, and, in particular, to compare their collections of overt 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 cartesian closed, but LKLoc is not.

Theorem 15.10 Over the effective topos Eff there is a sheaf topos Eff^{A} that has a model A^{op} of 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 to Grothendieck 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 A^{op} and A^{op} are models of ASD.

Since A^{op} is an internal category, i.e. a small one in classical language, we may form the sheaf topos Eff^{A}. But A^{op} and A^{op} are weakly equivalent to each other, and therefore to a full subcategory of Eff^{A}, by the Yoneda embedding. On the other hand, A^{op} 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) to investigate the conflicts between one view of the mathematical world and another, because the resolution 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, with singular covers and similar recursive phenomena.

The explanation is simply that, as we have shown, the quantifier ∀ that encodes compactness of 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 is definable. 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 ℝ 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 each model of ASD. In particular, our axioms isolate ℝ 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 the existence 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.

4This 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.

Questions of what is “true” in the Platonist mathematical world are unanswerable, but we can say 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 : ℝ → ℝ 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 ℝ → ℝ in ASD, whose classical interpretation 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 of analysis 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 these ideas 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” real line is whether open subsets look like what we expect. Traditionally, any open subset of the real line 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 compactness of [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 classical analysis (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 the closed interval, Bishop omitted it and focused on Cauchy completeness and total boundedness instead. The decomposition of open subsets of ℝ 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 first remember that the spaces in ASD are not sets and that the ASD calculus is not the calculus of logical predicates about points. The ASD statement “[0, 1] is compact” says nothing about the closed interval [0, 1] from Bishop’s mathematics, because the ASD type R cannot be interpreted naï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 the fact that [0, 1] behaves like a compact space within the realm of ASD algebras. The interesting question 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 by taking 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 calculus that can be used by real analysts. If, despite our advocacy of the intrinsic nature of the topology of 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.

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 on Gö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 to construct everything else from them. This is supposedly because integers are the basic objects of computation.

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 to prove 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 the interval domain first. Maybe you are interested in some other system (even the classical one) and have 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 \underline{ℝ}, \overline{ℝ} and Iℝ 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 à la Moore with an interval [d, u] overestimates the image 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] underestimates the image, or as we would 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 ∈ ℝ | 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 a language for analysis. We feel that this is worthy of study, both as the basis of theory and as that of 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 der mathematischen Wissenschaften. Springer-Verlag, 1985.

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

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

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

[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 Géné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 for formal 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 Sünderhauf. A domain-theoretic approach to real number computation. Theoretical Computer Science, 210:73–98, 1998.

[Esc04] Martín Escardó. 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 in Mathematics. Springer-Verlag, 1979.

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

[Gen35] Gerhard Gentzen. Untersuchungen ü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 the Foundations of Mathematics. North-Holland, 1969. Edited by Szabo, Manfred.

[GHK^{+}80] Gerhard Gierz, Karl Heinrich Hoffmann, Klaus Keimel, Jimmie Lawson, Michael Mislove, and Dana 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 of Mathematics. North-Holland, 1956. Third edition, 1971.

[HLPZ] Guillaume Hanrot, Vincent Lefèvre, Patrick Pélissier, and Paul Zimmermann. The MPFR Library. INRIA. www.mpfr.org.

[HR90] Martin Hyland and Giuseppe Rosolini. The discrete objects in the effective topos. Proceedings of 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.

[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 in Mathematics. 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] André 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 Gö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 Géometrie et Topologie 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.

[Mül01] Norbert Müller. The iRRAM: Exact arithmetic in C++. In Jens Blanck, Vasco Brattka, and Peter 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.

[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 and Nonstandard Views of the Continuum. Springer-Verlag, 2001.

[Sch03] Peter Schuster. Unique existence, approximate solutions, and countable choice. Theoretical Computer 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 über ein Axiom des Archimedes. Mathematische Annalen, 22(4):504–519, 1883.

[Str80] Ross Street. Cosmoi of internal categories. Transactions of the American Mathematical Society, 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 in Advanced Mathematics. Cambridge University Press, 1999.

[Thi97] Hayo Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, University of 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.

The papers on abstract Stone duality may be obtained from

                                  www.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 Applications of 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 their proceedings. 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.EU