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*]
*over*estimates 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*]
*under*estimates 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.