This paper introduces a new calculus for constructive general topology,
and in particular for analysis on the (Dedekind) real line.
When using this calculus,
there is no need to *prove* that functions are continuous,
because, from the start, the types are *intrinsically* topological spaces,
not sets with *imposed* structure,
and all terms are automatically continuous
with respect to the topology of the types.
They also have a computational interpretation, at least in principle.
Some basic facts about analysis, such as the Heine–Borel theorem
(compactness of [0,1] in the “finite open sub-cover” sense)
are also built in to the language.
It enjoys a very strong open–closed duality,
in contrast to the usual asymmetry between finite intersections and
infinite unions,
whilst avoiding the double negations that
are a conspicuous feature of Intuitionistic schools
such as those of Brouwer and Bishop.

As a first step towards testing whether our new language is suitable
for real analysis,
we prove the *intermediate value theorem*
and more generally study *connectedness*.
This in turn depends on finding the *maximum* value
in a non-empty compact subspace.
These topics relate to questions that have been studied at length
in the literature on constructive analysis,
which we review in Section 1,
but we believe that we have a new perspective on them.

As well as our new language, we also introduce a new
topological concept, namely *overt subspaces*. This
property is completely invisible in classical topology, because there
*every* subspace is overt. In Bishop’s constructive analysis, its
role is played by *locatedness* and *total boundedness*
(Remark 12.15),
but these are defined metrically,
using lots of εs and δs, which we almost entirely avoid.

By analogy with the view that the important thing
about a compact subspace is *which open sets cover it*,
rather than what points it contains,
we define overt subspaces by whether open subspaces *touch* them
(intersect them non-trivially).
In this way, compact and overt subspaces define logical operators
▫ and ◊ that satisfy the rules of modal logic.
Our motivating example of this is the collection of solutions that
interval-halving (and other) computational methods actually find for
real-valued equations.

In order to give some impression of what overtness means, and why the usual language is inadequate to describe it, Section 2 provides a translation into the usual set-theoretic language of the way in which we shall study the intermediate value theorem in our new language towards the end of this paper.

The modal operators ▫ and ◊ are continuous functions, not on the space ℝ itself, but on its topology (lattice of open subspaces). This means that we have to equip topologies with topologies. The one that we choose is due to Dana Scott and is related to local compactness. It appears in the background of analysis in the guise of semicontinuity and the ascending and descending real numbers, which will themselves play an important part in this paper. However, there seems to be no appropriate introduction to Scott continuity and continuous lattices that is intended for analysts, so Section 3 outlines the ideas from topological lattice theory and theoretical computer science that lie behind our calculus.

Even in the classical language, the ▫ and ◊ operators give
a new way of looking at the *singular* case,
*i.e*. the way in which the zeroes of a function (such as a polynomial)
vary, merge and vanish as its parameters change.
Whilst the *set* of zeroes changes discontinuously,
▫ and ◊ remain Scott-continuous across the singularity;
the only thing that breaks is one of the equations that relate them.
The abstract formulation in ASD makes the construction of
▫ and ◊ from the function an entirely symbolic one,
interprets these operators as subspaces and offers a general
(at least conceptual) structure in which to compute the zeroes.

*Sections **1**–**3**
are therefore not representative of either the paper
or the new calculus: for a “sample” please look at Sections
**10**, **13** and **14** instead*.
It is the calculus that it our main purpose, so if you are only interested
in this and not connectedness you may start with Section
3 or 4.
The underlying ideas come from foundational disciplines, not analysis;
indeed, my observations about the intermediate value theorem are made
as an outsider to even the dominant theory of constructive analysis.

In Section 4 we start to introduce the new calculus,
in a relatively informal way, developing the intuition that
*x*< *y* and *x*≠ *y* are properties of real numbers
that we can observe computationally, whereas *x*≥ *y* and *x*=*y* are not.
Section 5 sets out the restricted form of predicate logic
that we use, including the existential quantifier and an important
principle that underlies our dual treatment of open and closed subspaces.
We use this fragment of the calculus to discuss Dedekind and Cauchy
completeness in Section 6,
adopting the former as an axiom and proving the latter from it.

In topology there is a distinction between open and *general* subspaces.
Section 7 describes the λ-calculus that we
use to define the former and our quasi-set-theoretic notation
for the latter.
Recall that λ *x*. φ *x* is a notation for functions
that formalises “*x*↦ φ(*x*)”, and so makes them
first class citizens of the mathematical world.

This formalism enables us to define compact subspaces as ▫-operators in Section 8, developing the familiar results about closed or compact subspaces and direct images. The equivalence with closed and bounded subspaces of ℝ depends on further Scott- or semicontinuity properties that we formulate idiomatically as a “uniformity” principle in Section 9.

The calculus begins to look like real analysis in Section 10, where we show that every function ℝ→ℝ is continuous in the ε–δ sense, indeed uniformly so when the domain is compact. Although we do not study differential and integral calculus in this paper, we also indicate how these can be expressed in our language.

Section 11 gives the formal account of overtness
using ◊ operators,
closely following that of compactness in Section 8.
However, since we mainly consider *Hausdorff* spaces in this paper,
we only give half of the picture,
so let’s say a little bit here about overt *discrete* spaces.

Even in elementary real analysis,
there are many *combinatorial* methods,
such as integration (Remark 10.12),
where which we need at least *some* notion of a finite “collection”.
ASD rejects the claim that all mathematical objects are in the first instance
collections: it makes no recourse whatever to set theory
or to its usual categorical or type-theoretic alternatives.
It seeks to axiomatise topology *directly*
and there is nothing else in its world besides *spaces*.

We therefore have to select some of the spaces to play the role of sets. Overt discrete objects do this, because the full subcategory of them has exactly the properties that we require for doing discrete mathematics: Products, equalisers and stable disjoint sums of overt discrete spaces are again overt discrete, as are stable effective quotients by open equivalence relations [C] and finite powersets (free semilattices) [E]. Unfortunately, the relevant constructions in ASD take as much space as those for simple analysis, and are not yet available in a suitable form for the intended audience of this paper. We explain why these things are topologically non-trivial in Remark 12.16 and only rely on these methods in Section 15.

These examples illustrate the way in which overtness captures the existence of an underlying combinatorial structure, but in a topological way that is free of explicit coding. It is also related to recursive enumerability (Remark 11.15) and to other ideas that have arisen in constructive, computable and even classical analysis, such as the Bolzano–Weierstrass theorem and having a countable dense subspace.

Overtness therefore puts a common name to numerous aspects of the foundations of mathematics that have hitherto gone unremarked. Even the (currently very small number of) people who have so far encountered the idea in various constructive disciplines are well aware that it can only be appreciated very gradually, and not as a result of seeing the definition for the first time.

The combination of compactness and overtness is very powerful,
and we begin to study it in Section 12.
A feature of the lattice-dual *topological* axiomatisation
is that there is an axiom-by-axiom translation from modal logic
into the Dedekind cut for its maximum.
The idea is similar to the *constructive least upper bound principle*
(Definition 3.7).

In Section 13 this duality also leads to two definitions
of connectedness, each yielding an approximate version of the
intermediate value theorem. The overt one agrees with the definition
that is already known in constructive analysis. The *classical*
proof of connectedness of the interval and the line is valid in our calculus.
We also characterise open and compact connected subspaces of ℝ
as intervals
and show that any open subspace is a disjoint union of intervals.

Section 14 accomplishes our main goal, the intermediate value theorem.
For a function that has no tangent to the axis,
the zero-set is closed, overt and (in any bounded interval) compact.
In the singular case, the ◊ operator provides a zero-finding program,
and we present this result in a new way that takes a constructive
attitude to the classical theorem
and hints at the generalisation to ℝ^{n}.

In Section 15 we extend the traditional constructive definitions of connectedness from pairs to arbitrary families of open subsets, which is the notion that is used in category theory. We also show that the decomposition of open subspaces of ℝ into disjoint unions of intervals (Theorem 13.15) is unique and that compact intervals with non-Euclidean endpoints are compact connected. These results rely on the Heine–Borel property and so fail in Bishop’s theory. Since the central argument is combinatorial, it depends on ASD’s use of overt discrete spaces in the role of sets.

Finally, Section 16 tests the boundaries of our ideas with some counterexamples, emphasising the role of overtness.

This calculus is called Abstract Stone Duality because it was inspired
by Marshall Stone’s results on the duality of algebra and topology
[Sto37]
and his maxim that one should “always topologize” [Sto38].
The algebra that corresponds to traditional topology
is captured in the discipline of locale theory by the notion of
*frame*:
a lattice with infinite joins, over which finite meets distribute.
However, a frame is still a set with imposed algebraic structure.
ASD “topologises the topology” by saying that the carriers
for the algebra are themselves spaces of the kind being defined.
Algebras with non-set-theoretic carriers can be formulated
using the notion of *monad* in category theory.

Several lengthy papers were needed to turn this idea
into a theory of topology.
These culminated in the characterisation
of computably based locally compact spaces [G]
and the construction of the Dedekind reals [I].
As direct consequence of the monadic assumption from category theory,
we have a *recursive* model of analysis that satisfies the
Heine–Borel property.
This result is striking because it contrasts with the received wisdom
from Russian Recursive Analysis and Bishop’s theory [BR87],
as Section I 15 explains.

This paper is parallel to [I] in that they provide introductions to similar material for different audiences. This one, however, presents a slightly simplified version of ASD that relies solely on the basic intuitions and knowledge of a general mathematician, treating ℝ axiomatically instead of constructing it. The category theory has gone, and we give a “need to know” tutorial for most of the other foundational techniques that we shall use.

Since I am not an analyst, a *point–set* topologist or a homotopy
theorist, I cannot say whether ideas such as straddling intervals
have been used elsewhere to consider the intermediate value theorem.
However, these are only vehicles for the main cargo of this paper,
which is the *language* of ASD.
Since I have not come to real analysis from the usual direction,
I may well have made errors and misconceptions,
but they are not the *usual* errors.
I therefore hope that you will read what is *actually* written here,
and come to appreciate the beauty and symmetry of a logic
that reasons directly about topology and analysis.