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.