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.
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 ℝ, ℝ 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].Φ(i x).
Dually, computing with the back-to-front interval [u,d] underestimates the image, or as we would say, ∃ x:[d,u].Φ(i x)⇒Φ[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.