A Lambda Calculus for Real Analysis

Paul Taylor

19 August 2010

Abstract

Abstract Stone Duality is a revolutionary paradigm for general topology that describes computable continuous functions directly, without using set theory, infinitary lattice theory or a prior theory of discrete computation. Every expression in the calculus denotes both a continuous function and a program, and the reasoning looks remarkably like a sanitised form of that in classical topology. This is an introduction to ASD for the general mathematician, with application to elementary real analysis.

This language is applied to the Intermediate Value Theorem: the solution of equations for continuous functions on the real line. As is well known from both numerical and constructive considerations, the equation cannot be solved if the function “hovers” near 0, whilst tangential solutions will never be found.

In ASD, both of these failures and the general method of finding solutions of the equation when they exist are explained by the new concept of overtness. The zeroes are captured, not as a set, but by higher-type modal operators. Unlike the Brouwer degree, these are defined and (Scott) continuous across singularities of a parametric equation.

Expressing topology in terms of continuous functions rather than sets of points leads to treatments of open and closed concepts that are very closely lattice- (or de Morgan-) dual, without the double negations that are found in intuitionistic approaches. In this, the dual of compactness is overtness. Whereas meets and joins in locale theory are asymmetrically finite and infinite, they have overt and compact indices in ASD.

Overtness replaces metrical properties such as total boundedness, and cardinality conditions such as having a countable dense subset. It is also related to locatedness in constructive analysis and recursive enumerability in recursion theory.

Contents

1. The intermediate value theorem  5  9. Compactness and uniformity  44
2. Stable zeroes and straddling intervals 8  10. Continuity on the real line  48
3. The Scott topology  13  11. Overt subspaces  53
4. Introducing the calculus  20  12. Compact overt subspaces  58
5. Formal reasoning  23  13. Connectedness  63
6. Numbers from logic  27  14. The intermediate value theorem 68
7. Open and general subspaces  32  15. Local connectedness  74
8. Abstract compact subspaces  38  16. Some counterexamples  79

This paper appeared in the Journal of Logic and Analysis 2(5) 1–115 on 18 August 2010.

Introduction

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 Scottcontinuous 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 [I, Section 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.

1 The constructive intermediate value theorem

When we have described our new λ-calculus for general topology, we shall apply it to the intermediate value theorem, which solves equations that involve continuous functions ℝ → ℝ.

The usual constructive form of this result puts an additional condition on the continuous function, where the classical one has greater generality. Also, the constructive argument is based on an interval-halving method that apparently gives just one extra bit of the solution for each iteration, whereas the well known Newton algorithm doubles the precision (number of bits) each time.

Whilst it is widely appreciated that constructivism emphasises similar issues to those that arise in computational practice [Dav05], classical analysts sometimes feel that their constructive colleagues want to rob them of their theorems, without replacing them with algorithms that are any better than those that numerical analysts already know.

When we look more closely into these complaints, we find that the two sides are talking at cross-purposes and even the traditionalists are conflating two different theorems of their own. Some mathematicians consider the “generality” of classical results to be more important than their applications. On the other hand, anyone who is genuinely interested in solving an equation, i.e. in finding a number, will probably already have some algorithm (such as Newton’s) in mind, and will be willing to accept the pre-conditions that this imposes. We find, on examination, that these imply the extra property that constructivists require, which is in fact very mild: it is satisfied by any example in which you might reasonably expect to be able to compute a zero. Topologically, these conditions are weaker forms of openness, whilst the “general” theorem is about continuous functions.

Turning to the classical Newton algorithm, it is not always as good as it claims: on the large scale it can run away from a nearby zero and sometimes behaves chaotically. In fact, it only exhibits its rapid convergence after we have first separated the zeroes, which we must do by some discrete method such as interval-division. Ramon Moore’s interval Newton method [Moo66, Chapter 7], which exploits Lipschitz conditions instead of differentiability (cf. Definition 10.9), behaves at small scales like its traditional form, but at larger ones like interval halving, so it finds the initial approximation to the zero in a systematic way. Andrej Bauer has begun to demonstrate that computation may indeed be performed efficiently in the ASD calculus using these methods [Bau08].

Constructive mathematics is about proving theorems just as much as classical analysis is. What we gain from looking at the intermediate value theorem constructively is a more subtle understanding of the space of solutions in the singular and non-singular situations. In this paper, this will take the form of a new topological property of the space S_{f} of “stable” zeroes, which are essentially those that can be found computationally. Nevertheless, the space Z_{f} of all zeroes (stable or otherwise) still plays an equally important role: we shall study the two together, in a way that is an example of the open–closed duality in topology.

Let us begin, therefore, with the form in which the (classical) intermediate value theorem is taught to mathematics undergraduates:

Theorem 1.1 Let f : 𝕀 ≡ [0, 1] → ℝ be a continuous function with f(0) ≤ 0 ≤ f(1). Then there is some x ∈ 𝕀 for which f(x) = 0. Proof There are two well known proofs of this.

(a) Put x ≡ sup {y ∈ 𝕀 | fy ≤ 0} and suppose that 0 < ε < f(x), so since f(0) ≤ 0 we have x > 0. Then, by ε–δ-continuity, there is some interval (x ± δ) ≡ (x − δ, x + δ) on which f(y) > 0, so x was not, after all, the least upper bound of its defining set. A similar argument excludes f(x) < 0, which leaves f(x) = 0. This proof was given by Bernhard Bolzano in [Bol17, §15.3].

(b) The other proof uses interval halving. Let d_{0} ≡ 0 and u_{0} ≡ 1. By recursion, consider

x_{n} ≡ \frac{1}{2}(d_{n} + u_{n}), and put d_{n+1}, u_{n+1} ≡ \{ \begin{matrix}d_{n}, x_{n} & if f(x_{n}) > 0 \\ x_{n}, u_{n} & if f(x_{n}) ≤ 0, \end{matrix}

so by induction f(d_{n}) ≤ 0 ≤ f(u_{n}). But d_{n} and u_{n} are respectively (non-strictly) increasing and decreasing sequences, whose differences tend to 0, so they converge to a common value x. Using ε–δ-continuity in the last step again, f(x) = 0. Augustin-Louis Cauchy gave this proof in [Cau21, Note III]. □

These methods are not suitable as they stand for numerical solution of equations:

Example 1.2 Consider this parametric function, which hovers around 0:

for − 1 ≤ s ≤ +1 and 0 ≤ x ≤ 3, let f_{s}(x) ≡ min (x − 1, max (s, x − 2)).

The graph of f_{s}(x) against x for s ≈ 0 is shown on the left. The diagram on the right shows how f_{s}(x) depends qualitatively on s and x, where the two regions are open, and the thick lines denote f_{s}x = 0. In particular, f(1) = 0 iff s ≥ 0, f(2) = 0 iff s ≤ 0 and f(\frac{3}{2}) = 0 iff s = 0.

+1 f_{s}x  +1 s
[figure]
..................... −ve positive
.......
[figure: x; x]
[figure: .......]
..................... negative +ve
[figure: −1; 0; −1; 0]
0  1  2  3  0  1  2  3

Neither the classical theorem nor any numerical algorithm has much to say about analysis in this example. However, if any of them does yield a zero of f_{s}, as a side-effect it will decide a question of logic, namely how s stands in relation to 0.

Remark 1.3 As L.E.J. Brouwer observed in his revolutionary work in 1907 [Bro75, Hey56], for an arbitrary numerical expression s, we may not know whether s < 0, s = 0 or s > 0. There are many different ways in which such indeterminate values may arise, depending on whether your reasons for using analysis come from experimental science, engineering, numerical computation or logic. So s may be

(a) a parameter that we intend to vary;

(b) an experimental measurement that we can make only to a certain precision;

(c) the result of a numerical computation of which we have (so far) only found so many digits;

(d) a constant defined in terms of some mathematical question that has (so far) resisted solution, such as the Riemann Hypothesis or the Goldbach Conjecture (Brouwer used patterns in the digits of π ≡ 3.14159 ⋯ for this); or

(e) a constant defined in terms of some logical question that is provably unanswerable, such as s ≡ ∑_{n=0}^{∞} 2^{−n} · g_{n}, where g_{n} is the primitive recursive sequence

g_{n} ≡ \{ \begin{matrix}1 & if n encodes a proof that (⊢ 0 = 1) \\ 0 & otherwise, \end{matrix}

so s = 0 iff the calculus is consistent, which, as Kurt Gödel demonstrated [Göd31], it is unable to prove for itself.

We see that the issue is one of logic rather than geometry and the definitive answer only came in the 1930s. Whether Bolzano, Cauchy or the other 19th century analysts and geometers would have intended the intermediate value theorem to apply to Brouwer’s example is a question that needs extremely careful historical investigation. Other errors were made because the notion of uniformity was lacking (Remark 10.11), for example, so the fair conclusion is that those who believed the general result were relying on decidable equality of real numbers, and as such were mistaken in this too.

Since the Example is a monster from logic and not analysis, we bar it [Lak63]. It is also sometimes more convenient to suppose that the function is defined on the whole line.

Definition 1.4 We say that f : ℝ → ℝ doesn’t hover if,

for any e < t, ∃x. (e < x < t) ∧ (fx ≠ 0),

so the open non-zero set W_{f} ≡ {x | fx ≠ 0} is dense. A similar property, that f is “locally non-constant”, is used in other constructive accounts such as [BR87].

Example 1.5 Any non-zero polynomial of degree n doesn’t hover, x being one of any given n + 1 distinct points in the interval (d, u). □

Remark 1.6 For Newton’s algorithm to be applicable to solving the equation f(x) = 0, we must assume that the derivative f′ exists, and preferably that it is continuous. Also, since we intend to divide by f′(x), this should be non-zero, although it is enough that f′ doesn’t hover. So let d < x′ < u with f′(x′) ≠ 0. Then, by manipulating the inequalities in the ε–δ definition of f′(x′), cf. Definition 10.9, there must be some d < x < u with f(x) ≠ 0. This argument may be adapted to exploit any higher derivative that is non-zero instead. □

So this condition is very mild when taken in the context of its practical applications. Using it, here is the usual (exact) constructive intermediate value theorem (there is also an “approximate” one, cf. Proposition 13.4).

Theorem 1.7 Suppose that f : ℝ → ℝ is continuous, has f(0) < 0 < f(1) and doesn’t hover. Then it has a zero. Proof In the interval-halving algorithm (Theorem 1.1(b)), we may have f(x_{n}) = 0. This can be avoided by relaxing the choice of x_{n} to the x provided by Definition 1.4, to which we supply, say, e ≡ \frac{1}{3}(2d_{n} + u_{n}) and t ≡ \frac{1}{3}(d_{n} + 2u_{n}). Then we only have to test whether f(x_{n}) < 0 or > 0, which is allowed, both constructively and numerically [TvD88, Theorem 6.1.5]. □

This proof is better computationally than the previous one, in that it doesn’t involve a test for equality. But it introduces a new problem: the meaning of ∃, to which we shall return many times. Here we characterise the solutions that this algorithm actually finds.

Definition 1.8 We call x ∈ ℝ a stable zero of f if, for any d < x < u,

∃et. (d < e < t < u) ∧ (fe < 0 < ft ∨ fe > 0 > ft),

leaving you to check that a stable zero of a continuous function really is a zero. Stable zeroes are elsewhere called transversal.

On the other hand, even in such a nice situation as solving a polynomial equation, not all zeroes need be stable — in particular, double ones (where the graph of f touches the axis without crossing it) are unstable. As Example 1.2 shows, if f hovers, there need not be any stable zeroes.

Example 1.9 Consider f_{s}x ≡ sx^{2} − sx + 1 for s > 0 and 0 ≤ x ≤ 1, so f_{s}0 = f_{s}1 = 1. There are two stable zeroes when s > 4, a single unstable one at \frac{1}{2} when s ≡ 4, but no zeroes at all when s < 4. □

This discussion may perhaps suggest that unstable zeroes are a bad thing. However, the computational results are only one side of what we have to say in this paper: our treatment of topology will consider both stable and arbitrary (i.e. either stable or unstable) zeroes. In fact, it is also possible to compute unstable zeroes, if they are isolated and we know that they’re there, but this is a distraction from our story.

We conclude this section with a couple of remarks concerning the choice of name and formulation of stable zeroes.

Remark 1.10 Earlier drafts of this paper required e < x < t in Definition 1.8. Suppose we have e < t < x, where fe and ft have opposite signs, and f doesn’t hover in the interval (x, u). Then fy < 0 or fy > 0 for some x < y < u, so we may replace either e or t with y to obtain the stronger property. Similarly, if there are stable zeroes arbitrarily close on both sides of a point then it is a stable zero in the stronger sense.

Example 1.11 The hovering function f(x) ≡ sin(π/x) if x > 0 and 0 if x ≤ 0 has stable zeroes in the stronger sense at \frac{1}{n} but only in the weaker one at 0. □

Remark 1.12 (Andrej Bauer) We call such zeroes stable because, classically, x is a stable zero iff every nearby function (in the sup or ℓ_{∞} norm) has a nearby zero:

∀δ > 0. ∃ε > 0. ∀g. (|f − g| ≤ ε ⟹ ∃y. gy = 0 ∧ |y − x| < δ).

However, the ∀δ, ∀g and = in this formula mean that it is not a well formed predicate in the calculus that we shall introduce in this paper, although the ∀g may be allowed in a later version.

2 Stable zeroes and straddling intervals

In this section we look at the topological properties of the subspaces S_{f} ⊂ Z_{f} ⊂ ℝ of stable and arbitrary zeroes of a function f : ℝ → ℝ.

Remark 2.1 We know, of course, that Z_{f} is closed, and therefore compact if we choose to bound the domain of the function, with f : 𝕀 → ℝ.

We have S_{f} = Z_{f} for non-singular values of the parameters (which may, for example, be the coefficients of a polynomial), but in certain singular situations, S_{f} is smaller than Z_{f}. The set S_{f} is G_{δ} (a countable intersection of open subsets).

But the interesting thing for us is that S_{f} is overt. As we shall see, it is not possible to define overtness in terms of classical sets of points: we use logic instead. In this section we show how the notions of zero and stable zero for a function give rise to “modal” predicates □ and ♢ that may or may not be satisfied by open subspaces. Since such subspaces are themselves predicates on points, the result of this discussion will be to represent compact and overt subspaces as predicates on predicates.

Proposition 2.2 If an open subspace U ⊂ ℝ touches S_{f}, that is, it contains a stable zero x ∈ U ∩ S_{f}, then U contains (the whole of) a straddling interval,

[e, t] ⊂ U with fe < 0 < ft or fe > 0 > ft,

and conversely if f doesn’t hover. Proof By Definition 1.8, a point is a stable zero iff every open neighbourhood of it contains a straddling interval. [⇒] Since the point x itself is in the interior of U, some interval d < x < u is also contained in U. By Definition 1.8, this interval contains one that straddles. [⇐] The straddling interval is an intermediate value problem in miniature, for which Theorem 1.7 finds a stable zero. □

Remark 2.3 If an interval [e, t] straddles with respect to f then it also does so with respect to any nearby function g, i.e. with |f − g| < ε, where ε ≡ min(|fe|, |ft|), cf. Remark 1.12. Since the definition only refers to the endpoints, it is also invariant with respect to homotopies that fix the values there, in contrast to Example 1.9. □

Notation 2.4 We write ♢ U if the open subspace U contains a straddling interval.

The hypothesis of the intermediate value theorem makes ♢ U_{0} true when U_{0} ⊃ 𝕀, whilst ♢ ∅ is obviously false. Since ♢ requires the whole of the interval [e, t] to be contained in the open set, not just its endpoints, ♢ W_{f} is also false, where W_{f} ≡ {x | fx ≠ 0}. This relies on connectedness of [e, t].

Theorem 2.5 If f doesn’t hover then the ♢ operator preserves joins in the sense that

♢ ( ⋃_{j∈J} U_{j}) ⟺ ∃j ∈ J. ♢ U_{j}.

In particular, ♢(U_{1} ∪ U_{2}) ⟹ ♢ U_{1} ∨ ♢ U_{2}.

The hovering Example 1.2 fails this property for U_{1} ≡ (0, 1\frac{2}{3}) and U_{2} ≡ (1\frac{1}{3}, 3). Proof Suppose that 𝕀 ≡ [d, u] ⊂ ⋃_{j∈J} U_{j} with fd < 0 < fu, and consider the open subspaces (with > for V^{+} and < for V^{−})

V^{±} ≡ \{x : ℝ | ∃j:J. ∃y:ℝ. (x < y) ∧ (fy {> \atop <} 0) ∧ [x, y] ⊂ U_{j}\}.

For each x ∈ 𝕀, there are j ∈ J and e, t ∈ 𝕀 such that x ∈ (e, t) ⊂ [e, t] ⊂ U_{j}, but since f doesn’t hover in (x, t) there’s some x < y < t with fy ≠ 0 and [x, y] ⊂ U_{j}. Then x ∈ V^{+} or x ∈ V^{−}, according to the sign of fy. Hence 𝕀 ⊂ V^{+} ∪ V^{−}, whilst d ∈ V^{−} and u ∈ V^{+} by hypothesis.

Now, since 𝕀 is connected, V^{+} ∩ V^{−} is non-empty, so it contains some open interval, in which f doesn’t hover, so fx ≠ 0 for some x ∈ V^{+} ∩ V^{−}. If fx < 0 then (since x ∈ V^{+}) there is a straddling interval [x, y] ⊂ U_{j} with fy > 0; similarly if fx > 0 we have x ∈ V^{−} and fy < 0. See Theorem 14.12 for another proof of this. □

Remark 2.6 Some extra condition is necessary to prove this Theorem in ℝ^{1}, but Example 1.11 satisfies it despite hovering. Also, the classical mathematician may appreciate the improved constructive proof, whilst objecting that its pre-condition is unnecessary, because either 1 or 2 is a zero in Example 1.2. Besides, the constantly zero function hovers.

In higher dimensions, it is customary to study fixed points (f(x) = x) instead of zeroes (f(x) = 0). In his alter ego as a (non-constructive) geometric topologist, Brouwer showed that any continuous endofunction of the cube 𝕀^{n} has a fixed point. In this case, the disagreement between the classical and constructive situations cannot be brushed under the carpet: There is a computable function f : 𝕀^{2} → 𝕀^{2} with no computable fixed points, in the strong sense that none of the classical fixed points can be defined by a program [Bai85, Pot07].

Remark 2.7 If we want to apply Newton’s method, the derivative of the function has to be continuous and non-zero near the required solution. A similar pre-condition is needed for the usual definition of the Brouwer degree, which is a numerical analogue of our logical operator ♢ that takes disjoint unions to sums of integers [DG03, Llo78, Mil97]. In these non-singular settings, all zeroes are stable, so the space of them is overt and closed, and we shall see that many classical arguments remain constructively valid.

In these cases, locally, we have an open map, i.e. one for which the direct image of any open subspace is open. Open maps also arise if we look for the zeroes of an analytic function in ℂ instead of ℝ, whilst our notion of overtness came from asking when the map X → {⋆} is open [Joh84, JT84]. For any open map f : X → Y and element 0 ∈ Y, it is easy to see that the operator defined by ♢ U ≡ (0 ∈ fU) has the property of Theorem 2.5.

If we look more closely at how this property is achieved, we can extend it to the singular case, using overtness of the stable zeroes even when there are unstable zeroes around. When X is locally compact (Definition 3.18), 0 ∈ fU iff there is a compact subspace K ⊂ U with 0 ∈ V ⊂ fK, where V is open. Specialising further to f : ℝ^{n} → ℝ^{m}, we may take K to be an enclosing polyhedron: one for which f is non-zero on the faces but zero somewhere inside, cf. Remark 14.17.

However, it is not the purpose of this paper to consider this interesting geometrical problem, but instead to study the logical consequences of the join-preserving property, which will become the definition of overtness. We will only consider the non-hovering condition again when we return to the intermediate value theorem in ASD in Section 14.

We do, however, note a theme in this discussion that will recur in both the abstract development of the paper and the intermediate value theorem. There are two essentially different theorems, for the non-singular and singular cases. The former includes Bolzano’s argument and the Brouwer degree, requiring that f be (locally) open, whilst the latter uses interval bisection and only assumes the non-hovering condition or something similar.

We might imagine an overt subspace or the Brouwer degree as like radioactivity, or lions in the Sahara Desert (!) [Pét53], which cannot be seen themselves, but their presence in any region, however small, can be detected. Using the bisection argument yet again, such properties have a computational interpretation:

Theorem 2.8 Let ♢ be a property of open subspaces of ℝ that takes unions to disjunctions and satisfies ♢(0, 1). Then ♢ has an accumulation point x ∈ (0, 1), by which we mean one of which every open neighbourhood x ∈ U ⊂ ℝ satisfies ♢ U. If ♢ arises from the intermediate value problem for a non-hovering function, any such x is a stable zero. Proof Let d_{0} ≡ 0, u_{0} ≡ 1 and, by recursion, e ≡ \frac{1}{3}(2d_{n} + u_{n}) and t ≡ \frac{1}{3}(d_{n} + 2u_{n}), so

⊤ ⟺ ♢(d_{n}, u_{n}) ≡ ♢ ((d_{n}, t) ∪ (e, u_{n})) ⟺ ♢(d_{n}, t) ∨ ♢(e, u_{n});

then at least one of the disjuncts is true, so let (d_{n+1}, u_{n+1}) be either (d_{n}, t) or (e, u_{n}).

Since the property ♢(d, u) is only semi-decidable, this argument uses dependent choice. Computationally, we may interleave the execution of the tests, and choose whichever of them terminates first [N]: since this choice is made on contingent practical grounds rather than mathematical ones, it is said to be non-deterministic.

The sequences d_{n} and u_{n} converge to a common limit x, respectively from below and above. If x ∈ U then x ∈ (d_{n}, u_{n}) ⊂ (x±ε) ⊂ U for some ε > 0 and n, but ♢(d_{n}, u_{n}) is true by construction, so ♢ U also holds, since ♢ takes ⊂ to ⇒. □

Remark 2.9 Although we describe the interval-division algorithm on paper in a way that suggests precise bi- or tri-section, when we come to implement it we may find much better ways of calculating the division point. This could be far from the middle, and based on other information about the situation, possibly using some approximation to the derivative or Lipschitz condition. Then if we know that ♢(U ∪ V) but ¬ ♢ U (e.g. if f ≠ 0 on U), where U is a large part of the union, we are left with a small part that still satisfies ♢ V.

The operator ♢ therefore seems to capture these algorithms, albeit as parallel non-deterministic processes. Let’s see whether classical point-set topology has anything to say about it.

Exercise 2.10 Classically, let ♢ U ≡ (U ∩ S ≠ ∅) ≡ ∃x ∈ S. (x ∈ U), for any subset S ⊂ ℝ whatever. Show that the operator ♢ has the property in Theorem 2.5. □

Examples 2.11

(a) The existential quantifier to which we drew attention following the proof of Theorem 1.7 is defined by ♢ U ≡ ∃x ∈ S. (x ∈ U), where S is the open subspace {x | fx ≠ 0}.

(b) The accumulation points (in the traditional sense) of any sequence or net S are those of ♢ in the sense of Theorem 2.8. Apparently, ♢ is merely a roundabout way of defining a closed subspace, or the closure of an

arbitrary subspace:

Proposition 2.12 Let ♢ be an operator for which ♢ ⋃_{i∈I} U_{i} iff ∃i. ♢ U_{i}, and define

S ≡ {x ∈ ℝ | for all open U ⊂ ℝ, x ∈ U ⇒ ♢ U}.

Then W ≡ ℝ \ S = ⋃ {U open | ¬ ♢ U}

is open (making S closed) and has ¬ ♢ W by preservation of unions. Since ♢ takes ⊂ to ⇒, ♢ U holds iff U ⊄ W iff U ∩S ≠ ∅. If ♢ had been derived from some S′ as in Exercise 2.10 then S = \overline{S′}, its closure, since ♢ U ⟺ (U ∩ S′ ≠ ∅). □

Remark 2.13 We learn from this that

(a) since ♢-like properties are defined, like compactness (which we are about to consider), in terms of unions of open subspaces, they deserve to be called general topology, and we shall see that the analogy goes much deeper than this;

(b) the proof of Theorem 2.5, that the subspace of stable zeroes has such a ♢ in a useful way, uses an idea from geometric topology (connectedness) in the case of ℝ^{1};

(c) the operator ♢ is the bounded existential quantifier: ♢ U ≡ ∃x ∈ S. (x ∈ U);

(d) there are long-standing arguments in analysis and

(e) general algorithms that use these operators (abstracted from the original question) to solve many kinds of problem in a uniform way; so

(f) ♢-like properties stand exactly at the gateway between the mathematical and computational aspects of topology; but

(g) classical point–set topology is too clumsy to take advantage of this. When we come to study overtness in ASD, in Section 11, we shall find that the problem lies more with the sets of points than with classical logic.

Whereas stable zeroes are characterised by ♢, there is another operator □ that describes the subspace Z_{f} ⊂ 𝕀 of all zeroes. (The symbol □ is read “necessarily” and ♢ is called “possibly”.)

Notation 2.14 Let Z be any compact subspace. For any open subspace U, we write □ U if U contains or covers Z (where ♢ was about touching). If Z is the complement of an open subspace W ⊂ X of a compact Hausdorff space then

□ U iff (U ∪ W) = X.

The “finite open sub-cover” definition of compactness says exactly that □ ⋃_{i∈I} U_{i} iff □ ⋃_{i∈F} U_{i} for some finite F ⊂ I. This is similar to the defining property of ♢, except that in that case F consisted of a single index {i} ⊂ I.

We shall consider this common infinitary lattice-theoretic property of □ and ♢ in the next section. Here we look at their contrasting finitary properties:

Proposition 2.15 Let W ⊂ X be an open subspace of a Hausdorff space X, and let □ and ♢ be operators defined as above, i.e.

□ U ≡ (U ∪ W = X) and ♢ V ≡ (V ⊄ W)

for any open subspaces U, V ⊂ X. Then

(a) the operator □ preserves finite intersections,

□ X is true and □ U ∧ □ V ⟹ □(U ∩ V),

(b) whereas ♢ preserve finite unions (Theorem 2.5),

♢ ∅ is false and ♢(U ∪ V) ⟹ ♢ U ∨ ♢ V.

(c) The corresponding closed subspace X \ W is non-empty iff □ ∅ is false iff ♢ X is true,

(d) and it is a singleton iff □ preserves unions, iff ♢ preserves intersections.

(e) Both operators are Scott-continuous, as we shall explain in the next section. □

Now recall the situation in which □ was defined in terms of the compact subspace Z_{f} of all zeroes, and ♢ using the overt subspace S_{f} of stable zeroes of a non-hovering continuous function ℝ → ℝ. In the non-singular situation these coincide, but for singular cases of the parameters, S_{f} is properly contained in Z_{f}.

Proposition 2.16 If □ and ♢ arise from subspaces S ⊂ Z of a Hausdorff space X, with Z ≡ (X \ W) compact, then they satisfy the modal laws: for all open U, V ⊂ X,

□ U ∧ ♢ V ⟹ ♢(U ∩ V), □ U ⟺ (U ∪ W = X) and ¬ ♢ W,

whilst □(U ∪ V) ⟹ □ U ∨ ♢ V and ♢ V ⟸ (V ⊄ W)

hold iff S is dense in Z. □

Example 2.17 If fx ≡ (x − 1)^{2}(x + 2) ≡ x^{3} − 3x + 2 then Z_{f} = {1, −2} and S_{f} = {−2}. The last two laws fail for the intervals U ≡ (−3, −1) and V ≡ (0, 2). □

Remark 2.18 Therefore, whilst the subsets S_{f} and Z_{f} agree in the non-singular situation, they provide a rather unsatisfactory description of the way in which the zeroes of a function (or even of a polynomial) depend on its parameters, because they change abruptly at singularities. Notice also that they do so on opposite sides of the singularity and that the Brouwer degree is not defined there at all.

Whatever description or algorithm we use to solve equations, something has to break at singularities. Nevertheless, our operators ♢ and □ are defined from the function in a uniform way throughout the parameter space, indeed, even when it hovers. The only things that go wrong are (some of) the modal laws that relate them.

Although we shall not discuss computation explicitly in this paper, Theorem 2.8 and Remark 6.6 indicate what the computational meaning of the calculus is intended to be. They provide a general method of finding stable zeroes, even in the singular case, but this is necessarily non-deterministic.

We intend to introduce an abstract calculus in which all operations are regarded as continuous functions. Since ♢ and □ are applied to open subspaces of ℝ, and not to its points, we first have to explain in a concrete way how the topology (lattice of open subspaces) of a space carries its own topology.

3 The Scott topology

The topology that we shall impose on the topology of a space exploits the fact that the operators □ and ♢ preserve directed joins. It is now well known in theoretical computer science and topological lattice theory, so, if you are already familiar with either of these subjects, you may safely omit this section, as it just collects the basic facts of which you should be aware in order to follow the rest of the paper. Indeed, it serves as background and not an introduction, as our calculus will abstract from these ideas, rather than assume them.

In more traditional mathematical disciplines, on the other hand, the Scott topology is not as well known as it deserves, especially considering that it appears in real analysis in the guise of semicontinuity. The reason why it is absent from the curriculum is probably that it is not Hausdorff. Whilst there is a compact Hausdorff topology (the Lawson topology) that one can put on lattices of open sets, this does not have the properties that we require. The canonical textbook about these topologies and the continuous lattices on which they are particularly well behaved is [GHK^{+}80]; its six authors represent the various disciplines in which these ideas arose.

Definition 3.1 Let L be any complete lattice. A subset U ⊂ L is called Scott-open if

(a) it is upper: if V ⩾ U ∈ U then V ∈ U; and

(b) any subset S ⊂ L for which ⋁ S ∈ U already has some finite F ⊂ S with ⋁ F ∈ U. The Scott-open subsets form a topology on L. That is, ∅, L ⊂ L are Scott-open, if U, V ⊂ L are Scott-open then so is U ∩ V ⊂ L, and any union of Scott-open subsets is Scott-open.

It is crucial that you grasp the following point:

Exercise 3.2 Let L be the lattice of open subspaces of a locally compact space X. Re-stating the usual “finite open sub-cover” definition (Notation 2.14), show that a subset K ⊂ X is compact iff the family U_{K} ≡ {U ∈ L | K ⊂ U} of open neighbourhoods of K is a Scott-open subset of L. □

The compact–open topology on the set of continuous functions X → Y was introduced by Ralph Fox in 1945 [Fox45]. Our topology is the much simpler special case in which Y is the Sierpiński space (Definition 3.8), but Dana Scott identified it as the crucial one in the study of topologies on function spaces [Sco72]. It had already become clear by then that the neighbourhoods of a compact subspace (which our □ and U_{K} capture) are more important than its points [Wil70].

There are some other examples of the Scott topology that are useful in analysis and will play a major role in this paper. (In fact, they too can be seen as special cases of the topology on a topology on a space.)

Definition 3.3 The space \underline{ℝ} of ascending reals consists,

(a) classically, of ℝ together with ±∞, ordered arithmetically; or,

(b) constructively, of the rounded lower subsets D ⊂ ℚ, i.e. for those which

d ∈ D ⟺ ∃e:ℚ. d < e ∈ D,

ordered by inclusion (we get an isomorphic result if we replace ℚ by ℝ in this); and is endowed with the Scott topology that is defined by this order. The descending reals \overline{ℝ} are defined in a similar way, but using the reverse arithmetical order, so U ⊂ ℚ is rounded upper if u ∈ U ⇔ ∃t:ℚ. u > t ∈ D. Arithmetic negation (−) takes descending reals to ascending ones and vice versa, indeed making \underline{ℝ} ≅ \overline{ℝ}, but it is not continuous as an endofunction of either space.

The significance of (this topology on) the space \underline{ℝ} in traditional analysis is

Proposition 3.4 A function f : X → \underline{ℝ} is lower semicontinuous by definition if the inverse image of any open upper interval (d, +∞] is open in X. This happens iff f is continuous with respect to the Scott topology. □

So, when we say that all functions are continuous in our calculus, we are not precluding the consideration of semicontinuous functions: they just have to be seen as valued in \underline{ℝ} or \overline{ℝ} instead of in ℝ.

Example 3.5 The lower-semicontinuous step function f : ℝ → \underline{ℝ} ⊂ P(ℚ)

3

2  •
1 •  •
0  •  •
0  1  2  3  4

may be defined by

fx ≡ \{d | \begin{matrix}(d < 1 ∧ x < 1\frac{1}{2}) ∨ (d < 2 ∧ 1 < x < 2\frac{1}{2}) \\ ∨ (d < 3 ∧ 2 < x < 3) ∨ (d < 0) \end{matrix} \} .

Notice that it takes the lower value at the steps.

Remark 3.6 Constructively, the spaces \underline{ℝ} and \overline{ℝ} are not obtained by re-topologising the extended set of reals. On the contrary, an ordinary Euclidean real number is defined by a pair (called a Dedekind cut, cf. Definition 6.7) consisting of an ascending real (the set of its rational lower bounds) and a descending one (the upper bounds) that are compatible. In the computable setting, there are descending reals that have no ascending partner, and vice versa (Example 16.6).

The analysis of the ascending reals is very simple. In particular, any set of ascending reals has a supremum, given by union, and this is the limit of the set, so there is no difficulty with interchanging ascending limits, unlike two-sided ones.

These spaces offer two ways of forming the supremum of any set of Euclidean reals:

(a) as the intersection of their upper bounds, yielding a descending real; or

(b) as the union of their lower bounds, the result of this being an ascending real. In our calculus, we will be able to form these two suprema when the set is compact or overt, respectively (Propositions 9.13 and 11.18).

Why should these two suprema be the same? Constructively, we need an additional condition on the set in order to ensure that the two parts define a Dedekind cut:

Definition 3.7 A subset K ⊂ ℝ obeys the constructive least upper bound principle if

(a) it is inhabited and bounded above, and

(b) for any two real numbers x, z with x < z, either z is an upper bound for all of K, or there is some k ∈ K with x < k.

This condition, which is probably due to L.E.J. Brouwer, is necessary to form y ≡ sup K because of the locatedness property (Axiom 4.9) of y with respect to (x < z), that is, it must satisfy either x < y or y < z. We shall find in Section 12 that this follows from the mixed modal laws (cf. Proposition 2.16) and is sufficient to define a Dedekind cut, and therefore a Euclidean real number.

You may perhaps think that this “constructive” situation is rather complicated, and could be simplified by adding some extra axioms. However, it is not difficult to adapt the arguments of Sections 1 and 16 to show that any such axiom would provide an oracle that could solve unreasonable computational and logical problems like those in Remark 1.3. We shall come to see that these anomalous situations are just as natural as singularities in polynomial equations, and are indeed closely related to them. When we recognise that ascending and descending reals occasionally lead their own separate lives, we come to appreciate the symmetries that real analysis enjoys, instead of its pathological counterexamples.

Definition 3.8 Our last example of the Scott topology is the Sierpiński space, which we call Σ. We define it as the lattice of open subspaces of the singleton. Classically, therefore,

Σ looks like (⊙ •), not like 2 ≡ ( ⊙ ⊙ ),

having two points and three open sets. We shall call these points ⊤ and ⊥, the former being open and the latter closed. Since Σ is a lattice, it also has ∧ and ∨.

The space 2 is both discrete and Hausdorff, but Σ is neither. Whilst there is a continuous function that takes the two points of 2 to those of Σ, any continuous function Σ → 2 is constant. Hence Σ is connected, at least in the classical sense, and indeed in the constructive ones that we shall consider in Section 13. The map [0, 1] → Σ by x ↦ (x > 0) even makes it path-connected.

This means that Σ has “more than” two points — there is something in between ⊥ and ⊤ that “connects” them. From a constructive point of view, this is because we defined the points of Σ as the open subsets of the singleton. There are more of these than just the decidable or complemented ones ⊥ ≡ ∅ and ⊤ ≡ {⋆}.

The Sierpiński space was treated with derision in classical topology, but it is the spider in the middle of the web in our subject, being even more important than Proposition 3.4 for the ascending reals.

Proposition 3.9 For any space X, there is a bijective correspondence amongst

(a) open subspaces U ⊂ X,

(b) continuous functions ϕ : X → Σ and

(c) closed subspaces C ⊂ X, where we shall say that ϕ classifies U ≡ ϕ^{−1}(⊤) and co-classifies C ≡ ϕ^{−1}(⊥).

In particular, either U or C uniquely determines ϕ. □

Notice, therefore, that the correspondence between U and C is given by their common relationship to ϕ and not by set-theoretic complementation. This is how we avoid the double negations that appear frequently in work in the Brouwer and Bishop schools. Nevertheless, it is convenient to retain the word complementary for this relationship.

Remark 3.10 In the case where X ≡ Σ, continuous functions Σ → Σ correspond to open subsets of Σ. Three of these are definable: the identity and the constant functions with values ⊥ and ⊤, corresponding to the singleton, empty and entire open subspaces respectively. Just as there was no arithmetical negation for the ascending reals (Definition 3.3), there is no continuous function (“logical negation”, ¬) that interchanges ⊥ and ⊤.

More generally, Scott-continuous functions respect the order on the lattice. Indeed, any topological space X has a specialisation order, defined by

x ⩽ y if every neighbourhood of x also contains y.

This is antisymmetric iff the space is T_{0}, discrete iff it is T_{1} and (classically) it agrees with the order on the underlying lattice when that is given the Scott topology. Notice that we distinguish this order relation ⩽ from ≤ in real and integer arithmetic; they agree in the case of the ascending reals, but ⩽ is ≥ or = for the descending or Euclidean reals respectively. The key difference is that the order ⩽ is intrinsic, i.e. every continuous function f : X → Y preserves it, whilst ≤ is imposed on ℕ, ℚ and ℝ, in the sense that continuous functions may in general preserve, reverse or ignore it.

Scott continuity is stronger than just preserving order, but instead of talking about arbitrary joins and finite sub-joins, it is convenient to introduce a new definition.

Definition 3.11 A poset (partially ordered set) (I, ≤) is directed if it is inhabited (has an element) and, for any i, j ∈ I, there is some k ∈ I with i ≤ k ≥ j. When we form a join or union indexed by I (taking ≤ to ⩽), we use an arrow to indicate that it is directed: ⋁ ; or ⋃ ; .

Examples 3.12 The following ordered sets are directed:

(a) any total order (or chain); in particular

(b) ℕ, ℚ or {q : ℚ | q < a} with the arithmetical order, where a is any (ascending) real number; and

(c) ℚ or {q : ℚ | q > a} with the reverse arithmetical order, if a is a (descending) real number; also,

(d) the set of finite subsets of any set, with the inclusion order.

The Scott topology may be reformulated using directedness: U ⊂ L is open iff it is upper and, whenever ⋁ ; x_{i} ∈ U, already x_{i} ∈ U for some i ∈ I. Hence this topology may be defined on any dcpo (directed-complete partial order), i.e. a poset in which every directed subset but not necessarily every finite subset has a join.

Proposition 3.13 A function F : L_{1} → L_{2} between complete lattices (or dcpos) is Scottcontinuous, i.e. F^{−1}(V) is Scott-open in L_{1} whenever V ⊂ L_{2} is Scott-open in L_{2}, iff F preserves directed joins, i.e.

F ( ⋁ ; _{i∈I}x_{i}) = ⋁ ; _{i∈I}F (x_{i})

for all directed (x_{i})_{i∈I} ⊂ L_{1}. Hence a function that is Scott-continuous in each of several variables is jointly continuous in them [Sco72, Props. 2.5&6]. □

Examples 3.14 Our operators □ and ♢ are Scott-continuous functions from the lattice of open subspaces of X to Σ, since they preserve directed joins (Notation 2.14).

Moreover, if they are defined in terms of some (function f with) parameters, they are jointly continuous with respect to both those parameters and to open subspaces of X, throughout the parameter space. By contrast, the Brouwer degree cannot be continuous at singularities, because of the fact that it takes values in ℤ.

Remark 3.15 The use of directed covers of compact spaces instead of general ones simplifies the idioms of analysis, because covers are often naturally indexed by the rationals or reals.

Suppose, for example, that we want to find an upper bound for a function f : K → ℝ. The subsets U_{u} ≡ {k ∈ K | fk < u} indexed by candidate bounds u ∈ ℚ are open and cover K, so only finitely many of them are needed. Now, u ranges over a (totally ordered and so) directed poset ℚ, and we have u ≤ v ⇒ U_{u} ⊂ U_{v}. Therefore the finite open sub-cover need only have one member, named by the greatest u in the finite set, and we have K ⊂ U_{u} for a single u. In other words, there is a uniform bound.

More abstractly, a directed family (U_{u}) that respects the order on u ∈ ℚ corresponds to an upper semicontinuous function f : K → \overline{ℝ}, and to a directed relation θ, by

(k ∈ U_{u}) ≡ θ(k, u) ≡ (fk < u).

When we need to state Scott continuity in our abstract calculus, in Section 9, it will be most convenient to formulate it using θ, which must satisfy

(u ≤ v) ∧ θ(k, u) ⟹ θ(k, v).

This situation also arises with the opposite order. For example, in the definitions of continuity and differentiability (Section 10) we require δ > 0 with a certain property. Underlying this is a lower semicontinuous function, a directed family of subsets with δ ≤ ε ⇒ U_{δ} ⊃ U_{ε}, or a relation θ that satisfies

(δ ≤ ε) ∧ θ(k, ε) ⟹ θ(k, δ).

Now let’s think about Proposition 3.9 again.

Notation 3.16 Since open sets U ⊂ X correspond to continuous maps X → Σ, we write Σ^{X} for the lattice of them, equipped with the Scott topology. This correspondence also gives rise to the notation

ϕa  or  ϕa ⇔ ⊤  for  a ∈ U

for membership of this subspace.

Implicit in the expression “ϕa” is a binary higher-type function, called evaluation or application, so ev(ϕ, a) ≡ ϕa. We want this, like everything else, to be continuous, but this requirement places a severe restriction on the compatibility of the ideas in this paper with those of traditional topology:

Proposition 3.17 The function ev : Σ^{X} × X → Σ is jointly continuous (with respect to the Tychonov product topology defined from the given topology on X and the Scott topology on Σ^{X} and Σ) iff X is locally compact [GHK^{+}80, Thm. II 4.10], [Joh82, §VII 4]. □

As we are dealing with non-Hausdorff spaces (in particular Σ^{X}) here, we need to adjust the traditional definition of local compactness [HM81]:

Definition 3.18 A (not necessarily Hausdorff) space X is locally compact if, whenever x ∈ U ⊂ X with U open, there are compact K and open V with x ∈ V ⊂ K ⊂ U.

This relation between open subsets, written V ≪ U and called way below, may be characterised without mentioning the compact subspace K between them: if U ⊂ ⋃ ; W_{i} then already V ⊂ W_{i} for some i. This is the point from which the theory of continuous lattices begins [GHK^{+}80], but we shall not need to make much use of it, beyond observing the ubiquitous alternating inclusions of open and compact intervals in real analysis (Remark 10.1).

The result that justifies calling Σ^{X} a function-space is then

Theorem 3.19 Let X be locally compact and Γ any space. Then Σ^{X} is also locally compact and there is a bijection between continuous functions

Γ × X ⟶ Σ  and  Γ ⟶ Σ^{X}

that is given in the backward direction by composition with ev : Σ^{X} ×X → Σ. This correspondence is natural in the space Γ, i.e. it respects pre-composition with any continuous function Δ → Γ [Sco72, Section 3]. □

Remark 3.20 Dana Scott’s work grew into the two disciplines of domain theory and denotational semantics in theoretical computer science, giving topological meanings to programs as continuous functions. These ideas are particularly useful for functional programming languages, i.e. those in which functions may be defined as first class objects, e.g. [Plo77]. Functions are interpreted using λ-abstraction, whilst recursive definitions that need not necessarily terminate or be well founded are given a meaning in terms of directed joins.

Denotational semantics was founded on an intuition of the analogy between continuity and computation that had earlier roots in recursion theory such as the Rice–Shapiro theorem [Ric56]. In particular, the recursively enumerable subsets of ℕ provide something like a topology, in so far as they admit all finite intersections and some infinite unions.

The connection can be put more simply than this, in terms of computation with real numbers. We cannot make a positive (terminating) test for equality (cf. Remark 1.3), but we can do so for ≠, > or <. More generally, we may observe membership of an open subspace, since that is determined by some finite approximation to (essentially, finitely many decimal places of) the number. Like open subsets, (parallel) observations admit finite intersections and (some) infinite unions. Another basic intuition of Scott continuity is that the result of a computation depends on only a finite part of the data.

We shall begin the axiomatisation of our calculus in the next section from these remarks, but first we need to make some more foundational observations about general topology.

Remark 3.21 The Sierpiński space is particularly familiar in computation, because it provides the type of values of a program that may terminate (⊤) or diverge (⊥) but generates no numerical output or other side-effect. This type is called void in C and Java. An input of this type is a signal that may or may not ever arrive.

Then a program F of type Σ → Σ, i.e. which takes a signal as input and then may terminate (output another signal) or diverge, may behave in one of three ways:

(a) it may always diverge (⊥), whether it obtains an input signal or not;

(b) it may transmit the signal (id), i.e. wait for its input, do some internal processing and then terminate; or

(c) it may always terminate (⊤), without waiting for the input.

The one thing that it cannot do is to negate its input (¬), i.e. terminate iff its signal never arrives; this is called the Halting problem [Tur35]. The type Σ is therefore quite different from a two-element or Boolean type.

This situation is the same as that in Remark 3.10, except that we are now able to see computationally something that was perhaps a little ambiguous in constructive topology, namely the general behaviour of any program F : Σ → Σ is determined by the specific cases F ⊤ and F ⊥ in which it definitely does or does not receive the signal.

As in topology, we must have F ⊥ ⩽ F ⊤, i.e. if the program terminates without receiving the input signal, it must also terminate if it does receive it (for example, the signal might arrive just after F has terminated).

Using the lattice structure on Σ, we may use “linear interpolation” to define a function F : Σ → Σ, from F ⊤ and F ⊥. Because of the previous remark, this recovers the original F:

Definition 3.22 The Phoa principle (pronounced “Pwah”) [Hyl91] says that

for any F : Σ → Σ and x : Σ, F x ⟺ F ⊥ ∨ x ∧ F ⊤.

It would be wise to pause for a moment’s reflection on the ways in which we have motivated the Phoa principle in topology (Remark 3.10) and computation. This is the key step in the abstraction that we shall make in ASD, because it is exactly the condition that is required to ensure the extensional correspondence amongst open and closed subspaces and terms of type Σ^{X} in Proposition 3.9 [C].

It will also provide the glue that gives our proofs their coherence. However, the rules of inference in topology to which it leads (Axiom 5.6) may appear to be classical, so we emphasise that it was discovered as a result of investigations in several constructive disciplines.

One of these is locale theory, which is a formulation of general topology purely in terms of lattices, without mentioning points; Peter Johnstone’s book [Joh82] is an outstanding account of this and its relationship to many areas of mathematics, in particular analysis. The validity of our principle for locales is shown in [O, §7.5], but it had been noticed independently as the so-called Frobenius laws for open [JT84] and proper [Ver94] maps, cf. Propositions 11.2 and 8.2 respectively.

As for its connection with real analysis, the Phoa principle is similar to Markov’s principle, but the historical links involve too many unrelated ideas along the way to give the bibliographical trail.

Remark 3.23 There is a certain imprecision about the analogy between topology and recursion theory, since the former traditionally requires arbitrary unions, but the latter only recursive ones. In fact, the translation from programs to continuous functions is perfectly rigorous and has been used very successfully to develop methods of demonstrating correctness of programs. One may also try to reformulate topology using σ-frames, i.e. lattices with countable unions, over which meets distribute (the σ follows the usage of probability theory, but it is confusing in our notation). However, countability is just a mutilated form of set theory that does not get to grips with computation and actually makes no difference for objects such as ℕ and ℝ.

These issues may be addressed by considering topology and computation in parallel, i.e. by requiring the morphisms to be pairs consisting of a continuous function and a program that “agree” in a suitable sense. There are two such techniques that are well established. One uses logical relations and can show that, if the topological denotation of a program is ⊤ then its computation terminates [Plo77], cf. Remark 6.6. The other, called type two effectivity, develops computational representations of many ideas in classical general topology and real analysis [Wei00].

We have already seen in Proposition 2.12 that our possibility operator ♢ and the new notion of overtness are badly represented by the arbitrary unions of subsets that are used in traditional general topology. We want to replace these arbitrary unions by recursive ones, thereby legitimising the idea that the RE subsets of ℕ form a topology (Remark 3.20). However, when we consider how complicated both topology and recursion theory are on their own, it seems to be a recipe for a dog’s breakfast to try to combine them into a new theory.

So that’s not what we are going to do: the revolutionary approach that we shall follow in this paper is quite different from any of these things. We begin by abandoning traditional topology and recursion theory altogether, and returning to some extremely basic intuitions about the things that we can calculate about real numbers. We find that, without ever introducing set theory, we can recover the main results about continuity on the real line, including the issues regarding connectedness and solutions of equations that we introduced in the first two sections. On the other hand, it has been well known since the time of Alonzo Church, Stephen Kleene and Alan Turing that more or less anything that looks like computation is equivalent to the standard forms (at least as far as partial functions from ℕ to ℕ are concerned). In particular, there are already enough ingredients amongst our topological ideas to do general computation.

Overtness plays a key role underlying all of this. In the previous section, we saw manifestations of it in open maps, the existential quantifier and the join-preserving property of ♢. It is also related to recursive enumerability, and specifies which joins exist in open set lattices and the ascending reals. However, despite the fact that it does so many jobs, we don’t have to do anything to encode this behaviour into the system: it will all just fall out naturally.

In this section we have introduced some ideas from non-Hausdorff general topology because they underlie four decades’ work in the theory of computation but are largely unknown to those mathematicians who do not work in computer science departments. In particular, they provide the background for our new calculus. However, I now ask you to forget them again, along with all of the other textbook accounts of general topology, and begin the next section with a fresh mind. Our new calculus will “stand on its own feet”. It has a concrete representation that we have just sketched, but is not defined by it, just as groups may be represented by permutations or matrices, and integers by sheep or pebbles. Progress in mathematics is made by abstraction from such things, leaving the old concrete form behind.

4 Introducing the calculus

Now we start to present our new calculus, which is called Abstract Stone Duality, in a relatively informal way. For a more formal treatment that is better suited to logicians please see [I] instead. Indeed, readers of both kinds should be aware that the notation in this paper is the result of carefully chosen de-formalisation of the earlier and more foundational work in the ASD programme, in order to make it look more like the usual idioms of mathematics.

The first few axioms are very familiar facts about the real line and other spaces.

Axiom 4.1 In this paper, we take ∅, 1, 2, 3,..., ℕ, ℤ, ℚ, ℝ, 𝕀 ≅ [0, 1] ⊂ ℝ and the Sierpiński space Σ as base types. If X and Y are types then so are their product X × Y and sum (disjoint union) X + Y. The open and closed subspaces of X that are defined by a continuous function ϕ : X → Σ are also types, as is the function-space Σ^{X}. However, we stress that these do not use set theory.

Every variable x or expression a has a type; we write x : X or a : X to say what it is.

Along with X ×Y, X +Y and Σ^{X} come projections, pairing, inclusions, case-analysis, functionapplication and abstraction operations. These are explained in any account of simple type theory, such as [Tay99, §2.3].

You may substitute the phrase “locally compact topological space” for “type” if you wish, just as you understood elements of a group as matrices, and numbers as collections of beads, earlier in your mathematical education. However, our language is intended to be complete in the sense that we can reason in it using just the rules that we state, and not by forever referring back to the model in traditional topology. These rules extend those of arithmetic, and the role of types is to stop us from doing silly things like applying logical operators to numbers or vice versa.

The fundamental place of ℝ in science surely justifies introducing and axiomatising it independently, as we do in this paper. On the other hand, [I] constructed it using two-sided Dedekind cuts of ℚ in the ASD calculus. So you may say that the Axioms about ℝ here were Theorems there, or that that paper implements the ideas of this one, or again that it shows that these axioms provide a conservative extension. However, giving some implementation is not an exclusive action: there may be better ones.

Axiom 4.2 Terms of any type may be defined by recursion over ℕ, for example ℕ itself has addition and multiplication. The objects ℤ, ℚ and ℝ carry the structure of commutative rings, with the usual notation, inclusions and algebraic laws. We shall consider division and general recursion shortly.

Axiom 4.3 The types ℕ, ℤ and ℚ all carry the usual six binary relations

x = y, x ≠ y, x < y, x ≤ y, x > y and x ≥ y,

but ℝ and 𝕀 only have x ≠ y, x < y and x > y.

Notice again that we distinguish ≤ in arithmetic from ⩽ in logic and topology.

Axiom 4.4 These nine expressions are propositions, as are

⊤ (true), ⊥ (false), σ ∧ τ, σ ∨ τ, ∃x:S. ϕ(x) and ∀x:K. ϕ(x),

whenever σ, τ and ϕ(x) are, except that the quantifiers may only be formed when S is overt and K compact, as we shall explain later. Propositions are the same as terms of type Σ. Therefore, for the topological and computational reasons that we gave in the previous section, we cannot use ¬ or ⇒ to form them.

However, such a logic would be too weak to be useful. An important difference between set theory and topology is that one has just a single notion of subset, whilst the other has many different kinds of subspace: open, closed, compact, overt, connected and so on (Section 7). We therefore need to make analogous distinctions in the terminology that we use for the corresponding logical properties.

Definition 4.5 If σ and τ are propositional expressions and a, b : X are any two expressions of the same (but any) type then

σ ⇒ τ,  σ ⇔ τ  and  a = b : X

are called statements. The intended meaning of the first is that the open subspace represented by σ is contained in that represented by τ, or that if the program σ terminates then so does τ, whilst the containment between corresponding closed subspaces is the other way round. The second says that they coincide. Since σ ⇒ τ iff σ ∧ τ ⇔ τ, all three can be seen as equations between terms of type Σ or X, but they are not terms themselves.

We write & instead of ∧ for the conjunction of statements; note that ∃, ∀, ⇒ and ⇔ cannot be used to combine statements into more complicated things (in this version of the calculus, but cf. [M]). We shall, however, write

α ⇒ β ⇔ γ ⇒ δ  for  (α ⇒ β) & (β ⇒ γ) & (γ ⇒ β) & (γ ⇒ δ),

just as we do with equations and inequalities of numbers. We shall see how statements can be used to define subspaces, in particular compact ones, in Sections 7 and 8.

A propositional expression ϕx that contains a parameter (free variable) x : X defines a function X → Σ, which is automatically continuous, and so (cf. Proposition 3.9) both an open subspace U and a closed one C, where

ϕx ⇔ ⊤ means x ∈ U  and  ϕx ⇔ ⊥ means x ∈ C.

These are statements, although we sometimes write them more briefly as ϕx and ¬ϕx respectively. Since we are not allowed to write ¬¬ϕx or ϕx ∨ ¬ϕx, the subspaces U and C are not “complementary” in anything like the set-theoretic sense.

We may use statements as axioms, assumptions or conclusions, as we shall explain in the next section.

Now consider the meaning of statements that are formed directly from the propositional arithmetical relations on ℕ and ℝ that we introduced in Axiom 4.3. Recall that we said that ℝ didn’t have =, ≤ or ≥ as propositions, because the subspaces of ℝ × ℝ that these define are not open.

Examples 4.6 For x, y : ℝ, the statements

(x ≠ y) ⟹ ⊥,  (x > y) ⟹ ⊥  and  (x < y) ⟹ ⊥

mean x = y, x ≤ y and x ≥ y respectively. We augment our notation for statements with these three familiar symbols, but now equality has become overloaded:

Definition 4.7 We call a type N (such as ℕ or ℚ but not ℝ) discrete if the two statements in the rule on the left below are interchangeable. The top one is the statement of equality of two terms (n, m) that we could make for any type, and the bottom one is a statement of equality of two propositions, (n =_{N} m) and ⊤. A discrete space is special in that the proposition (n =_{N} m) of equality is meaningful for it (as it is for ℕ and ℚ but not ℝ) and makes this rule valid.

n = m : N ; = ; (n =_{N} m) ⇔ ⊤  h = k : H ; = ; (h ≠_{H} k) ⇔ ⊥

Definition 4.8 Similarly, we call a type H (such as ℕ, ℚ or ℝ) Hausdorff if the statement of equality of terms (h, k) on the top right is interchangeable with the statement of equality of propositions below it, one of which is the proposition (h ≠_{H} k) of inequality. In other constructive accounts of analysis, ≠ is sometimes called apartness and written h # k.

Since propositions provide a logical way of describing open subspaces, these two properties say that the diagonal subspace X ⊂ X × X is respectively open or closed. In traditional topology, which has arbitrary unions, every discrete space is Hausdorff, but this is not so in ASD: =_{N} may be defined whilst ≠_{N} isn’t (Example 16.5). When they are both defined, as they are for ℕ, they are complementary (Definition 6.4). Lemma 5.9 collects some of the properties of equality and inequality.

We can now formulate some of the basic properties of ℝ as axiomatic statements:

Axiom 4.9 The types ℚ and ℝ are totally ordered Hausdorff fields, i.e.

(x ≠ y) ⟺ (x < y) ∨ (y < x)  and  x^{−1} is defined iff x ≠ 0.

The order relation < is also transitive and located,

(x < y) ∧ (y < z) ⟹ (x < z) ⟹ (x < y) ∨ (y < z).

Beware that the word “located” has several meanings in constructive analysis, which are related but not directly so.

5 Formal reasoning

In our new calculus, we will be able to reason about continuous, computable functions in ways that are quite similar to those with which you are already familiar for giving proofs based on set theory. So the situation is like that of learning Italian when your native language is Spanish: it’s possible to communicate quite effectively, but in order to learn the new language properly, you have to begin by defining the grammar of your own language in a more formal way. You may perhaps wish to hear the language being spoken (in the course of this paper) before learning it yourself, but this section is by no means optional.

Remark 5.1 Hermann Weyl (quoted in [EJ92]) said that “logic is the hygiene the mathematician practices to keep his ideas healthy and strong”. This precisely sums up what ASD provides, if we take “health and strength” to mean that any function that we define will be continuous automatically, according to the right topologies on the object concerned.

We achieve this by enforcing “hygiene” precautions that take the form of restrictions on the applicability of the usual logical connectives. In other words, to gain the benefit of our calculus you need to learn the rules according to which these may be used in topology, and unlearn those that come from mathematics based on set theory, which yield non-continuous functions. As we shall see, these restrictions are topologically natural, for example the universal quantifier, ∀, may only range over compact spaces (Sections 2 and 8).

Our approach is in contrast to the traditional one that begins by allowing set-theoretic reasoning in its widest generality, and afterwards tries to restore sanity by imposing topological and computational structure. Our thesis is that this unwieldy structure is unnecessary, because the same things can be achieved more naturally by introducing a weaker logic that is in tune with topology and computation in the first place.

The style in which we shall set out our predicate calculus belongs to a tradition begun by Gerhard Gentzen [Gen35], where our restrictions take the form of additional side-conditions on the applicability of the rules. A textbook introduction that includes all of the predicate and λcalculus that we assume here and in Section 7 is provided (but in its standard form) by [GLT89].

Definition 5.2 A mathematical argument consists of a sequence (or tree) of

(a) acts of formation of well defined terms, a : X, and assigning types to them (Axiom 4.1); and (b) assertions of statements, σ ⇒ τ, σ ⇔ τ or a = b : X (Definition 4.5). However, each term or statement may contain parameters, so these steps are made in the context of these parameters, which also have type-assignments and are subject to assumptions in the form of statements. Some proofs proceed directly from fixed assumptions by developing successive conclusions. Others are indirect: assumptions and variables need to be introduced and discharged, in particular when using the quantifiers, so the context may vary from one statement to the next.

In proof theory, where contexts are manipulated heavily, it is customary to use the Greek letters, Γ, Δ,... for them. We, on the other hand, only need the occasional reminder that parameters and assumptions may be present, so we shall usually write “⋯” instead of Γ for an unspecified context, or omit it if it doesn’t change.

One formal way of showing the relevant context is to write it on the left of a turnstile, ⊢. (This symbol was first used by Gottlob Frege, but has done many different jobs since his time.) Then a statement-in-context is called a judgement. For example,

…, x : ℝ, d ≤ x ≤ u, ϕx ⇔ ⊤, ψx ⇔ ⊥ ⊢ θx ∧ (x < u) ⇒ ∃t:𝕀. ϕt ∧ ψt,

where the various expressions (d, u, ϕ, ...) must themselves have been introduced in previous judgements, is written informally as “let x : ℝ and suppose that d ≤ x ≤ u, ...” in the text, followed by its conclusion as a display,

θx ∧ (x < u) ⟹ ∃t:𝕀. ϕt ∧ ψt.

Even if we do not mention free variables explicitly, any (symbol for a) term in this paper denotes an expression that may contain parameters. That is, except for a small number of occasions where we specifically say otherwise.

On the other hand, our types are fixed, without parameters, at least in the present version of the calculus.

Definition 5.3 In keeping with the need to allow parameters to pass all the way through an argument, when we talk about a function f : X → Y, we mean an expression

…, x : X ⊢ f(x) : Y

of type Y, in which we draw attention to the variable x : X as one amongst many that may occur in it, although it does not have to do so.

Exercise 5.4 Fill in the contexts (“Γ ⊢”) in all of the formal assertions that we make in this paper. (Print out a fresh copy!)

Definition 5.5 This discussion may sound like mere symbol-pushing, but it has a direct topological meaning or denotation. The context Γ denotes a big space (universe of discourse), sometimes written [[Γ]], that is a subspace of the product of the types of the parameters, carved out by the assumptions.

Terms and functions also have denotations, which are continuous functions between the denotations of the corresponding types or contexts. We have to construct these continuous functions by recursion over the language, with a scheme of recursion steps for each of the connectives. We explain in Section 7 how Theorem 3.19 handles abstraction and application of functions, and also how to define subspaces.

By “denotation” we mean the same as we did in Remark 3.20: a structure-preserving translation of a symbolic language into point-set topology. In fact, the denotational semantics of programming languages “factors through” the denotation of ASD, in the sense that it can be rewritten to use our syntactic language for topology.

Whilst the denotation helps us to understand what the calculus is doing, the syntax stands on its own feet, and we shall develop proofs directly in it. These are well formed if their successive judgements obey one of a number of patterns called rules of inference. When we state these, a single line indicates deduction downwards, and a double one equivalence (upwards too).

Axiom 5.6 The Phoa principle (Definition 3.22) may be formulated as a pair of rules that transfer statements across the ⊢, between the assumptions and the conclusion. One of these is the same as the rule for ⇒ in intuitionistic sequent calculus, but the other is like Gentzen’s rule for classical negation:

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

By Definition 5.5, “Γ, σ ⇔ ⊤” denotes an open subspace of the universe, and “α ⇒ β” means that one relative open subspace of this is contained in another. Then both lines of the rule on the left say that the intersection of the open subspaces of Γ classified by σ and α is contained in that classified by β.

Because of Definition 4.5, the rule on the right is valid constructively, because it says exactly the same thing as that on the left, except that it concerns the intersection of closed subspaces, cf. the discussion following Definition 3.22.

However, to distinguish our theory of topology from (classical) set theory, we need

Axiom 5.7 Every F : Σ^{Σ} is monotone: if σ ⇒ τ then F σ ⇒ F τ, cf. Remarks 3.10 and 3.21. From this we can recover the Phoa principle (Definition 3.22):

Proposition 5.8  F σ ⟺ F ⊥ ∨ σ ∧ F ⊤.  □

The Phoa principle will be as important to our logic for topology as the distributive law is to arithmetic. For example, whereas the traditional constructive proof of the intermediate value theorem (Theorem 1.7) requires Dependent Choice, we avoid it in ASD by relying on the Phoa principle (Section 13). More mundanely, we first use it to show that equality in a discrete space obeys the usual properties of substitution, reflexivity, symmetry and transitivity, whilst inequality obeys their lattice duals.

Lemma 5.9 Let N and M be discrete spaces and H and K Hausdorff ones, let f : N → M and g : H → K be functions (Definition 5.3) and let ϕx and ψx be predicates on N and H respectively. Then

\begin{aligned}ϕm ∧ (n =_{N} m) & ⇒ & ϕn & ψh ∨ (h ≠_{H} k) & ⇐ & ψk \\ (n =_{N} m) & ⇒ & fn =_{M} fm & (h ≠_{H} k) & ⇐ & gh ≠_{K} gk \\ (n =_{N} n) & ⇔ & ⊤ & (h ≠_{H} h) & ⇔ & ⊥ \\ (n =_{N} m) & ⇔ & (m =_{N} n) & (h ≠_{H} k) & ⇔ & (k ≠_{H} h) \\ (n =_{N} m) ∧ (m =_{N} k) & ⇒ & (n =_{N} k) & (h ≠_{H} k) ∨ (k ≠_{H} ℓ) & ⇐ & (h ≠_{H} ℓ). \end{aligned}

Proof Starting from the basic rule of substitution,

…, n = m : N ⊢ ϕn ⟺ ϕm,

discreteness (Definition 4.7) allows us to replace the statement of equality of terms on the left above by the equality proposition:

…, (n =_{N} m) ⇔ ⊤ ⊢ ϕn ⟺ ϕm,

and then the first rule in Axiom 5.6 transfers this across the ⊢,

… ⊢ (n =_{N} m) ∧ ϕm ⟹ ϕn.

The other results in the left-hand column follow from this.

If you think you understand the results for =, which apply to open subspaces of a discrete space, then you also understand those for ≠, since they say the same thing in the upside-down notation for closed subspaces of a Hausdorff space. Formally,

…, h = k : H  ⊢ ψh ⇔ ψk
…, (h ≠_{H} k) ⇔ ⊥ ⊢ ψh ⇔ ψk
…  ⊢ ψh ⇒ ψk ∨ (h ≠_{H} k)

using Definition 4.8 and the second rule in Axiom 5.6. □

Whereas the Gentzen rules in topology (together with those for ⇒ in set theory) move propositions across the ⊢, the rules for the quantifiers move a variable. The latter is said to be free in one line of the rule and bound in the other.

Axiom 5.10 The rule for the existential quantifier is

…, x : X ⊢ ϕx ⟹ σ = … ⊢ ∃x. ϕx ⟹ σ

in which the propositional expression ϕx may contain the variable, but σ must not. The upward direction of this rule is equivalent to existential instantiation,

ϕa ⟹ ∃x. ϕx.

The downward direction justifies the mathematical idiom there exists, in which, when given ∃x. ϕx, we may temporarily assume that we have an x that satisfies ϕx, in order to deduce any conclusion σ, so long as σ doesn’t depend on what x is. However, no choice is involved in doing this, because the formal rule may be shown to agree precisely with the informal idiom [Tay99, §1.6]. On the other hand, we must not export the value of the witness from the argument.

Remark 5.11 Quantification is the logical form of the infinitary unions in topology, but arbitrary unions were the reason why Proposition 2.12 missed the point of Theorem 2.5, and more generally of computation (Remark 3.23). The rule above is therefore not asserted in general in ASD: the type X of the quantified variable x must be overt.

As far as the familiar spaces in topology are concerned, this is not a severe handicap, since ℕ, ℚ, ℝ and the other base types that we listed in Axiom 4.1 are all overt. The one significant exception that will arise in this paper is that closed subspaces need not in general be overt (Section 16).

Besides the topological properties that we discuss in this paper, the existential quantifier is also employed for combinatorial purposes, even in analysis. For example, we shall want to say that there exists a step function that approximates an integral sufficiently accurately (Remark 10.12). Since this means that there exists a number of steps, as well as that there exist values for each of them, we are quantifying over a more complicated space, to which we shall return in Remark 12.16.

We study overt (sub)spaces more fully in Section 11: the reason for introducing the quantifier here is that we need it to state some of the basic properties of ℕ and ℝ.

Lemma 5.12 The quantifier ∃ is related to ∧ by the Frobenius law,

τ ∧ ∃x. ϕx ⟺ ∃x. (τ ∧ ϕx).

Proof Each side of this law is related to the judgement …, x : X, τ ⇔ ⊤ ⊢ ϕx ⇒ σ by Axioms 5.6 and 5.10. The name is due to Bill Lawvere. □

Lemma 5.13 The order < on ℝ admits interpolation and extrapolation:

(x < z) ⟺ ∃y. (x < y) ∧ (y < z) and ⊤ ⟺ ∃xz. (x < y) ∧ (y < z).

Proof [⇒] by existential instantiation, with y ≡ \frac{1}{2}(x + z), x ≡ y − 1 and z ≡ y + 1. [⇐] by the other direction of Axiom 5.10. □

In the same way, from Lemma 5.9, we deduce

Lemma 5.14 For any propositional expression ϕx on an overt discrete space N,

ϕn ⟺ ∃m:N . ϕm ∧ (n =_{N} m).  □

Theorem 8.13 gives the dual rules for the universal quantifier ∀, which ranges over a compact space, and Lemma 8.14 is the dual of Lemma 5.14.

6 Numbers from logic

The axioms that we have given so far generate numbers from numbers using the arithmetic operations, logic from numbers using relations, and logic from logic using the connectives and quantifiers. However, for the logic to be of any practical use, we must complete the circle by recovering numbers from it. The idea is to define an integer or a real number by giving some propositional expression that fixes it uniquely. We shall see that the various “limiting” operations in analysis can be derived from this, and that all computation is done in the arena of logic.

In the case of ℕ, we characterise those propositions that ought to be of the form ϕn ≡ (n =_{ℕ} a), where a : ℕ is the number to be defined. This is a rule of logic that is easily overlooked; it was first stated correctly (including our Lemma 6.3) by Giuseppe Peano, who wrote \overline{ι} for our “the” [Pea97, §22].

Definition 6.1 A description is a propositional expression ϕn containing a variable of overt discrete type N (such as ℕ or ℚ but not ℝ) such that

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

For example, for any given a : ℕ, the proposition ϕn ≡ (n =_{N} a) is a description.

Axiom 6.2 For any description ϕ, there is term, written a ≡ the n. ϕn, of type N, for which ϕn ⇔ (n =_{N} a). For example, the n. (n^{3} =_{ℕ} 8) is 2.

The following is a syntactical result about this new symbol:

Lemma 6.3 Any expression of type ℕ or ℚ is provably equivalent to one of the form the n. ϕn, in which the description operator is not used in the syntax of ϕ, whilst any real or logical term be rewritten without using it at all. Proof Any term of type ℕ or ℚ may be wrapped in a description operator,

a = the n. (n =_{N} a),

so we just have to show how to eliminate it from within propositional sub-expressions. From Lemma 5.14 and the Axiom we have

θ(the n. ϕn) ⟺ ∃m. θm ∧ (m =_{N} the n. ϕn) ⟺ ∃m. θm ∧ ϕm

and we may use this to rewrite each description operator within the expression. □

Lemma 6.4 A predicate αx is called decidable or complemented if there is another predicate ωx such that

αx ∧ ωx ⟺ ⊥  and  αx ∨ ωx ⟺ ⊤.

They define a unique function f : X → 2 for which αx ≡ (fx = 0) and ωx ≡ (fx = 1). Proof The expression θnx ≡ (n = 0 ∧ αx) ∨ (n = 1 ∧ ωx) satisfies

(∃n. θnx) ⟺ (αx ∨ ωx) ⟺ ⊤

and θnx ∧ θmx ⟹ (αx ∧ ωx) ∨ (m = n = 0) ∨ (m = n = 1) ⟹ (m = n).

Hence θ is a description (of n, parametrically in x) and defines a map f : X → 2 ⊂ ℕ. Since (fx = 0) ⇔ θ0x ⇔ αx and (fx = 1) ⇔ θ1x ⇔ ωx, the correspondence is bijective (see also [B, §11]). □

In particular, ℕ has decidable equality, because both = and ≠ are defined for it.

Remark 6.5 Propositional expressions that have parameters may be used to embed computation in our calculus. First consider a function f : N → 2 such that ∃n. fn = 1, so there are predicates αn ≡ (fn = 1) and ωn ≡ (fn = 0) with

…, n : ℕ ⊢ αn ∧ ωn ⇔ ⊥, αn ∨ ωn ⇔ ⊤ and … ⊢ ∃n. αn ⇔ ⊤.

Then there is a third predicate ϕn, defined by

…, n : ℕ ⊢ ϕn ≡ αn ∧ ∀m < n. ωm,

that has the uniqueness property too, so it is a description, and the n. ϕn is the least n such that αn.

This way of obtaining a number n from a function f is called general recursion or minimalisation. It is known that there are general recursive functions that grow faster than any that can be defined using primitive recursion (Axiom 4.2) alone, so Lemma 6.3 cannot eliminate all descriptions: they properly extend the calculus. Minimalisation over partial functions may be formulated using pairs of predicates α and ω that need only satisfy the first of the three conditions above; [D] interprets them in ASD.

These results are proved as constructions within the ASD calculus and so hold in any model of it. However, the converse operation, which you may think of as a very limited choice principle, depends on syntactical analysis, so it is a property of the free model:

Remark 6.6 The calculus obeys the existence property:

if ⊢ ∃n. ϕn ⇔ ⊤ is provable then so is ⊢ ϕm ⇔ ⊤, for some numeral ⊢ m : ℕ,

where ⊢ with nothing on the left means that no parameters are allowed. This may be shown by methods of proof theory that go outside the calculus (e.g. logical relations, cf. Remark 3.23): the proof of ⊢ ϕn ⇔ ⊤ can be manipulated to derive the numeral ⊢ m : ℕ.

The meaning of ∃ was the battleground between classical and intuitionistic mathematics in the 1920s. Brouwer’s philosophy that in order to say that something exists we must be able to construct it was later justified by this property when intuitionism became formalised. However, our version is weaker because it only applies to integer expressions without parameters.

The search for a witness m can be made by a machine, using logic programming, and it doesn’t even require the proof as an input: the search terminates (possibly after a very long time) if it exists, but diverges or aborts if it doesn’t. However, the details of the computation depend on a careful syntactic analysis of the whole calculus, which is way beyond the scope of this paper [N].

Beware, also, that there is no lattice dual of this result: there is a propositional expression ϕn that is not equivalent to ⊤, but such that ⊢ ϕm ⇔ ⊤ for each numeral ⊢ m : ℕ.

Turning to real numbers, we cannot define them by descriptions because equality of real numbers is not a proposition (Definition 4.7). We could use inequality instead [I, Exercise 14.14], but it is more natural to characterise the propositional expressions that are of the form δd ⇔ (d < a) and υu ⇔ (a < u).

Definition 6.7 A Dedekind cut (δ, υ) is a pair of propositional expressions δd and υu, with real or rational arguments d and u, such that

\begin{aligned}∃e. (d < e) ∧ δe & ⇔ & δd & ∃t. υt ∧ (t < u) & ⇔ & υu \\ ∃d. δd & ⇔ & ⊤ & ∃u. υu & ⇔ & ⊤ \\ δd ∧ υu & ⇒ & (d < u) & (δd ∨ υu) & ⇐ & (d < u). \end{aligned}

The top two statements say that δ and υ are respectively ascending and descending reals, cf. Definition 3.3; we call such a pair (δ, υ) a pseudo-cut. The middle two say that they are bounded; and the bottom ones that they are disjoint and located, cf. Axiom 4.9. The real line itself is constructed from Dedekind cuts of ℚ in [I].

Analogously to Axiom 6.2 for ℕ, we assert

Axiom 6.8 The type ℝ is Dedekind complete in the sense that every cut is of the form

δd ⇔ (d < a) and υu ⇔ (a < u) for some unique a : ℝ.

Just as we introduced the n. ϕn as a new piece of syntax for the integer defined by a description, we sometimes also write cut (δ, υ) for this new real number a. However, the analogue of Lemma 6.3 for cuts relies on additional axioms, and will be given in Corollary 10.3.

In order to print the result of a real-valued expression in the traditional decimal or binary notation, we first need another axiom to say that it is equivalent to a Dedekind cut of the (decimal or dyadic) rationals, and not infinite or infinitesimal:

Axiom 6.9 The Archimedean principle says that, for x, ε : ℚ or ℝ:

ε > 0 ⟹ ∃k:ℤ. ε(k − 1) < x < ε(k + 1).

We often use ε ≡ 2^{−n} in this, cf. [I, Prop. 11.15 & Lemma 14.2]:

Lemma 6.10 Between any two real numbers lies a dyadic rational:

x < y ⟹ ∃n, k:ℤ. x < k · 2^{−n} < y.

On either side of any real number there are arbitrarily close dyadic rationals,

x : ℝ, n : ℤ ⊢ ∃k:ℤ. (k − 1) · 2^{−n} < x < (k + 1) · 2^{−n}.  □

Remark 6.11 Applying the existence property (Remark 6.6) to k, we may therefore evaluate any real-valued expression ⊢ a : ℝ (without parameters) to any prescribed number ⊢ n : ℤ of binary digits: a ≈ k · 2^{−n}. More generally, given any possibility operator ⊢ ♢ : Σ^{ℝ} → Σ (without parameters) that is true on some interval, so ⊢ ♢(a, b) ⇔ ⊤, we may find k : ℤ such that

⊢ ♢ ((k − 1) · 2^{−n}, (k + 1) · 2^{−n}) ⇔ ⊤,

cf. Theorem 2.8. The query that we raised about the existential quantifier ∃x_{n} in Theorem 1.7 may also be settled in this way.

We stress that this proof-theoretic computation operates on an entire expression, and that it needs to be given the required precision n explicitly (say, 1000). Our sketchy mathematical discussion does not claim to say anything about how to implement these ideas practically on a computer, so you cannot judge from what we have said here how fast or slow it is. There is a syntactic translation that eliminates real numbers from our calculus in favour of dyadic intervals [K]. These can then be manipulated using constraint logic programming [Cle87], which can solve equations as rapidly as Newton’s algorithm does so. For some preliminary work on real computation within our calculus, see [Bau08, N].

Also, even in the case of a single real number a, it is subject to the usual caveat that there may be an error of as much as one unit (not just a half) in the last place, essentially because of Remark 1.3 again. In other words, the result k is non-determinate. This helps to explain how the computation can jump from one solution to another when we vary the coefficients of, for example, a cubic equation.

Nevertheless, returning from computation to analysis, we may abstract from this result by replacing the fixed numeral n with a (variable) parameter, and k·2^{−n} with a real-valued expression a_{n} that depends in a definite way on n. (Bolzano [Bol17, §§7,12] did this before Cauchy [Cau21, Chapître VI].)

Definition 6.12 A Cauchy sequence is an expression a_{n} : ℝ containing a variable n (albeit subscripted) of type ℕ and maybe other parameters such that

…, n, m : ℕ ⊢ n ≤ m ⟹ |a_{n} − a_{m}| < 2^{−n}.

This sequence converges to a limit a : ℝ if

…, n : ℕ ⊢ ⊤ ⟺ (|a_{n} − a| < 2^{1−n}) ≡ (a_{n} − 2^{1−n} < a < a_{n} + 2^{1−n}).

Remark 6.13 Here 2^{−n} is called the modulus of convergence, and may be replaced by another function μ(n), for example Bishop used μ(n) ≡ \frac{1}{n+1}. Specifying the modulus makes the difference between

(a) the classical definition, where any finite number of terms may be altered or deleted without affecting the limit, which we only find out retrospectively; and

(b) our constructive one, for which the limit is determined to any prescribed accuracy (2^{−n}) by finitely many (n) terms, where n is known in advance.

The constructive definition is consistent with the fact that the result of any computation can only depend on a finite part of the data (Remark 3.20), but the classical definition conflicts with this.

Addition, multiplication and substitution of sequences incur an administrative overhead, because they need to be re-parametrised in order to satisfy the modulus of convergence. Commonly occurring sequences such as the sums of power series do not march obediently towards their limits at the exponential pace that we have ordered. But analysts who regularly deal with series are skilled in re-bracketing and re-arranging them: there is no reason why the nth member of the sequence need be the sum of exactly n terms of the series.

Now we shall find the limit of any Cauchy sequence. Given that we are about to prove our first Theorem of analysis in ASD, we adopt a more formal style, to illustrate the way in which the rules of the previous section are used. Nevertheless, plenty of logical details have been abbreviated, so it would be a very good exercise to make them explicit, in particular formalising the idiomatic use of “there exists” using Axiom 5.10 and [Tay99, §1.6].

Theorem 6.14 Every Cauchy sequence in ℝ converges to a unique limit.

Proof The limit a will be defined as a Dedekind cut (δ, υ), where

δd ≡ ∃n:ℕ. (d < a_{n} − 2^{−n}) and υu ≡ ∃n:ℕ. (a_{n} + 2^{−n} < u).

These are easily seen to be lower and upper respectively (using transitivity of < and the Frobenius law, Lemma 5.12) and rounded (using interpolation). They are bounded by any d < a_{0} − 1 < a_{0} + 1 < u. For disjointness, given d, u, we have

δd ∧ υu ≡ ∃nn′:ℕ. (d < a_{n} − 2^{−n}) ∧ (a_{n′} + 2^{−n′} < u),

so let m ≡ min(n, n′), whence |a_{n} − a_{n′}| < 2^{−m} < 2^{−n} + 2^{−n′} and u − d > 0.

Locatedness is usually the most difficult thing to prove, as we found when constructing ℝ itself and defining addition and multiplication on it [I]. We need the Archimedean principle (Axiom 6.9), in the form that

(d < u) ⟹ ∃n:ℕ. (u − d > 2^{2−n}).

Besides expanding the definitions of δ, υ and ≤ (Example 4.6), the proof relies on the meaning of ∃ (Axiom 5.10) and the Phoa principle (Axioms 5.6):

…, (δd ∨ υu) ⇔ ⊥  ⊢ (∃n. d < a_{n} − 2^{−n} ∨ a_{n} + 2^{−n} < u) ⇒ ⊥
…, (δd ∨ υu) ⇔ ⊥, n : ℕ ⊢  (d < a_{n} − 2^{−n} ∨ a_{n} + 2^{−n} < u) ⇒ ⊥
…, (δd ∨ υu) ⇔ ⊥, n : ℕ ⊢ d ≥ a_{n} − 2^{−n} and a_{n} + 2^{−n} ≥ u
…, (δd ∨ υu) ⇔ ⊥, n : ℕ ⊢ u − d ≤ (a_{n} + 2^{−n}) − (a_{n} − 2^{−n}) < 2^{2−n}
…, (δd ∨ υu) ⇔ ⊥, n : ℕ ⊢  (u − d > 2^{2−n}) ⇒ ⊥
…, (δd ∨ υu) ⇔ ⊥  ⊢ (d < u) ⇒ (∃n. u − d > 2^{2−n}) ⇒ ⊥
…  ⊢ (d < u) ⇒ (δd ∨ υu).

Hence, by Dedekind completeness, δd ⇔ (d < a) and υu ⇔ (a < u) for some unique a : ℝ. This is a limit because

…, n, m : ℕ ⊢ n < m ⟹ a_{n} − a_{m} < 2^{−n} < 2^{1−n} − 2^{−m} ⟹ a_{n} − 2^{1−n} < a_{m} − 2^{−m},

so, putting m ≡ n + 1,

…, n : ℕ ⊢ ⊤ ⇔ (∃m. a_{n} − 2^{1−n} < a_{m} − 2^{−m}) ≡ δ(a_{n} − 2^{1−n}) ≡ (a_{n} − 2^{1−n} < a),

and similarly a < a_{n} + 2^{1−n}. Finally, it is unique because, if … ⊢ a, b : ℝ satisfy

…, n : ℕ ⊢ ⊤ ⇔ a_{n} − 2^{1−n} < a, b < a_{n} + 2^{1−n} ⇒ |a − b| < 2^{2−n},

then … ⊢ (∃n. |a − b| > 2^{2−n}) ⇔ ⊥,

so a = b by the Archimedean principle and Definition 4.6. □

Remark 6.15 Other accounts of constructive analysis, most notably Errett Bishop’s [BB85], define real numbers as Cauchy sequences of rationals, but this approach leads to a heavily metrical treatment of analysis. By contrast, in ASD we can do things topologically, as we shall see. Indeed, in the drafting of this paper and [I], I had developed the analysis as far as the intermediate value theorem using the order on ℚ and ℝ before considering their arithmetic at all [I, Sections 11-13].

We can also take a more topological view than Remark 6.11 of the translation from Dedekind cuts to Cauchy sequences. Bearing in mind the unavoidable non-determinacy, one popular representation, called signed binary, is ∑_{n} d_{n}2^{−n}, where d_{n} ∈ {−1, 0, +1} ≡ 3. We want the evaluation map 3^{ℕ} → [−2, +2] to be surjective, rather than an isomorphism. In fact, it is a proper surjection, i.e. the inverse image of any a : [−2, +2] is an occupied compact subspace (Definition 8.6 and Theorem 8.9) of 3^{ℕ}. But the calculus does not provide function-spaces like this (essentially, Cantor space) for free, so we have first to construct it [L].

Returning to computation,

Theorem 6.16 Any computable continuous function f : ℝ → ℝ in the classical world can be represented in ASD. Proof (Sketch) Since it is continuous, f is uniquely determined by the open subset of rational triplets (d, q, u) such that d < fq < u. On the other hand, we have a program that approximates f, which it may do in any of the senses that we have discussed in this section. The point is that this program can be adapted to one that

terminates on input (d, q, u) iff d < fq < u.

General recursion, and indeed the denotational semantics of any modern programming language, can be formulated in ASD, so this modified program can also be represented. Finally, since it yields Dedekind cuts, it defines a term x : ℝ ⊢ gx : ℝ in our calculus, whose denotation back in the classical world is the given function f. □

The other two limiting operations of elementary analysis, derivatives and integrals, are also naturally defined as Dedekind cuts, and will be considered briefly in Section 10. Section 12 shows that ℝ is complete in an order-theoretic sense by constructing the maximum of a non-empty compact overt subspace. Definition by description and Dedekind completeness may be seen as examples of a more general categorical idea called sobriety: see [I, Section 14] and [A].

7 Open and general subspaces

Whereas there is only one notion of “subset” in set theory, in topology we need to distinguish between open and other kinds of subspaces. Besides this, open subspaces are used in two different ways in our arguments: not only as particular spaces that are included in larger ones, but also as generic tests that are used in the definition of compactness. This section introduces our notation for these two roles: we use the λ-calculus for open subspaces considered as tests, and adopt {} from set theory for inclusions of general subspaces.

We will set out the λ-calculus in a relatively formal way because, as we said in Remark 5.1, logic thereby undertakes the burden of proof of continuity. Because of the methods that we sketched in Section 3, any well formed expression in our language denotes a function that is automatically continuous in traditional general topology. Our purpose in this paper is to show that it is possible to do some things in elementary real analysis entirely within this language. Traditional set-based topology is then redundant, because we (or a machine) may compute directly with our language, so we have made the first step towards using computation instead of set theory as the foundations for analysis.

Remark 7.1 Recall from Section 3 that open subspaces of X correspond uniquely to continuous functions X → Σ, so the topology on X is the collection of such functions. However, we do not consider this as a set but as another space, which we call Σ^{X}; in traditional terms, it carries the Scott topology. The meaning of Σ^{X} is captured by Theorem 3.19: there is a bijection between continuous functions

Γ × X ⟶ Σ  and  Γ ⟶ Σ^{X}.

This is the recursion step in the proof that every well formed expression denotes a continuous function in traditional topology. We may re-state it as

Proposition 7.2 If the denotation (in the sense of Definition 5.5) of

Γ, x_{1} : X_{1}, …, x_{n} : X_{n} ⊢ σ is a continuous function [[Γ]] × [[X_{1}]] × ⋯ × [[X_{n}]] ⟶ Σ

then the denotation of

Γ ⊢ λx_{1} … x_{n}. σ is a continuous function [[Γ]] ⟶ Σ^{[[X_{1}]]×···×[[X_{n}]]},

where the products are given the usual Tychonov topology and Σ^{[[X_{1}]]×···×[[X_{n}]]} the Scott topology [Sco72, Section 3]. □

Remark 7.3 The typed λ (lambda)-calculus, which gives a name to the forward correspondence, may seem to be little more than a change of symbols, especially when it is used for sets. In topology, on the other hand, Theorem 3.19 depends crucially on the correct definitions of local compactness and of the Scott topology, so these ideas are built in to the syntax. Whenever we use this syntax, we therefore implicitly invoke that Theorem.

We intend to use these ideas to define compactness and overtness. We saw in Section 2 that these are captured by operations □ and ♢ that preserve directed unions, so are continuous functions Σ^{X} → Σ with respect to the Scott topology. We therefore handle them in our language as terms of this type. Any well formed expression F such as □ or ♢ of this type denotes such a continuous function, and so F ϕ is of type Σ and denotes a member of the Sierpiński space.

However, in order to discuss terms of higher types like these, we need to be able to treat a function ϕ : X → Σ as a thing in itself (of type Σ^{X}). This is why we need the typed λ-calculus, instead of the informal ways in which mathematicians usually talk about functions, and which we too have been using so far. There are numerous textbook accounts of λ-calculi and the way in which they, and the β-rule in particular, relate to computation. Beware, however, that they usually talk about arbitrary function-types Y^{X} (also written X → Y), whereas we only allow Σ^{X} and (Σ^{Y})^{X} ≅ Σ^{(Y ×X)}. This corresponds to only allowing λ to bind logical expressions. See [I, Section 4] for how these general treatments are specialised to ASD.

In order to distinguish our own λ-calculus from the generic ones, we need to define its types, its terms and the rules that say when two terms of the same type are to be interchangeable (regarded as equal). Axiom 4.1 listed the base types and the ways of forming new ones that we use in this paper. We have already introduced the terms for the arithmetic of ℕ, ℚ and ℝ and for the logic in Σ, so we need to say how the λ-calculus provides other ways of forming terms.

Axiom 7.4 For any proposition (term of type Σ)

…, x_{1} : X_{1}, …, x_{n} : X_{n} ⊢ σ,

possibly containing variables x_{1}, …, x_{n} of any type and maybe some other variables (or “parameters”) from the list …, we may form the predicate

… ⊢ λx_{1}, …, x_{n}. σ,

in which x_{1}, …, x_{n} are bound by lambda abstraction, but the other variables in the list ⋯ remain free. The type of λx_{1}, …, x_{n}. σ is X_{1} → ⋯ → X_{n} → Σ or Σ^{X_{1}×···×X_{n}}, where the convention is that X → Y → Σ means X → (Y → Σ).

Axiom 7.5 Conversely, given any predicate ϕ of type Σ^{X_{1}×···×X_{n}} and expressions (“arguments”) a_{1} : X_{1}, ..., a_{n} : X_{n} of the corresponding types, any of which may contain parameters, we may apply the predicate to the arguments, yielding the proposition ϕ⟨a_{1}, a_{2}, …, a_{n}⟩.

Application is given by the map ev : Σ^{X} × X → Σ, whose denotation is jointly continuous by Proposition 3.17. Hence, in the backward direction of Theorem 3.19, if the denotations of ϕ, a_{1}, ..., a_{n} are continuous functions then so is that of ϕ⟨a_{1}, a_{2}, …, a_{n}⟩. This and Proposition 7.2 are the steps in the proof by recursion that every term denotes a continuous function.

Finally, there are rules to say that the two directions of the correspondence are mutually inverse. We need these in order to be able to reason entirely within the calculus itself, without referring back to the model.

Axiom 7.6 When a lambda-abstraction ϕ ≡ λx⃗. σ is applied to arguments, the result is equivalent to substitution of those arguments for the abstracted variables:

(λx_{1}:X_{1}, …, x_{n}. σ)⟨a_{1}, a_{2}, …, a_{n}⟩ ⟺ [a_{1}/x_{1}, …, a_{n}/x_{n}]^{∗}σ.

This is called the β-rule. Its converse is the η-rule: we recover the given function or predicate if we apply it to fresh variables and then abstract them:

(λx_{1}, …, x_{n}. ϕx_{1} … x_{n}) = ϕ,

this being an equational statement (Definition 4.5) between terms of type Σ^{X_{1}×···×X_{n}}. The βand η-rules are equivalent to saying that the correspondence in Theorem 3.19 is bijective.

Naturality (in the categorical sense) is captured by

Axiom 7.7 We may substitute a term for a free variable:

[a/x]^{∗}λy. σ = λy. [a/x]^{∗}σ and [a/x]^{∗}(ϕb) ⟺ ([a/x]^{∗}ϕ)([a/x]^{∗}b),

so long as x and y are distinct variables and y is not a free variable in a.

Besides equalities of λ-terms such as these, the lattice structure of Σ gives rise to an order relation:

Notation 7.8 If the propositions σ, τ : Σ with parameters x⃗ : X⃗ are related by σ ⇒ τ or σ ⇔ τ then (as we have just done) we write λx⃗. σ ⩽ λx⃗. τ or λx⃗. σ = λx⃗. τ for the corresponding relationships between the predicates. So ⩽ is really the same as ⇒: we just use two symbols for clarity, distinguishing between propositions (type Σ) and predicates (type Σ^{X}).

Now we turn to subspaces in the sense of inclusions, starting with two familiar cases.

Axiom 7.9 The predicates ⊢ α, ω : Σ^{X} (without parameters) give rise to

(a) the open subspace U ≡ {x : X | αx ⇔ ⊤} and

(b) the closed subspace C ≡ {x : X | ωx ⇔ ⊥}. Plainly we need some notation to distinguish between these two subspaces that arise from the same predicate. The curly brackets are no more than convenient symbols and are in no way intended to be a re-introduction of set theory. As with other parts of the language, we must give the rules according to which we may manipulate these symbols.

In particular, any type X in our language is to be regarded, not just as a set of points or terms, but as a space, whose topology is another space, the exponential Σ^{X}. In order to introduce U and C as types, we therefore have to construct Σ^{U} and Σ^{C} too.

Axiom 7.10 The exponentials Σ^{U} and Σ^{C} are obtained as retracts of Σ^{X} by splitting the idempotents α∧(−) and ω ∨(−) respectively. Hence the open subsubspaces of U and C are canonically represented as those open subspaces ϕ of X that lie between the least and greatest ones:

for U: ⊥_{U} ≡ ⊥_{X} ⩽ ϕ ⩽ ⊤_{U} ≡ α and for C: ⊥_{C} ≡ ω ⩽ ϕ ⩽ ⊤_{C} ≡ ⊤_{X}.

The intersection of an open subspace with a closed one is written {x | αx & ¬ωx} and called locally closed. It is the result of composing the constructions above (which commute) and its open subsubspaces are represented by ϕ : Σ^{X} with ω ∧ α ⩽ ϕ ⩽ α.

On the other hand, if α and ω are complementary (Lemma 6.4) then each of them defines a clopen (both closed and open) subspace.

Remark 7.11 These idempotents arise from the canonical ways of converting open subspaces of X into those of U and C and conversely. For an open subsubspace V ⊂ U ⊂ X, this is easy: V is already an open subspace of X, classified by ϕ with ϕ ⩽ α, so

Σ^{U} ≅ \{ϕ : Σ^{X} | ϕ ⩽ α\}[figure: \underline{α ∧ (−)}] Σ^{X}.

In the closed case, given W ⊂ C ⊂ X, the union V ≡ W ∪ U ⊂ X is open, where V (not W) is classified by ϕ : Σ^{X} with ω ⩽ ϕ. Hence we have the representation

Σ^{C} ≅ \{ϕ : Σ^{X} | ω ⩽ ϕ\}[figure: \underline{ω ∨ (−)}] Σ^{X}.

It is then necessary to show that these retracts of Σ^{X} obey the bijective correspondences

Γ × U ⟶ Σ ; = ; Γ ⟶ Σ^{U}  and  Γ × C ⟶ Σ ; = ; Γ ⟶ Σ^{C}

using the fact that any map on the top row extends to one Γ × X → Σ. The argument within the abstract ASD calculus depends on Axiom 5.6 and is given in [C].

Remark 7.12 This suggests a more general situation, in which the inclusion i : Y ↣ X is Σ-split by a map I : Σ^{Y} ↣ Σ^{X} for which Σ^{i} · I = id. In fact, any computably based locally compact space Y can be represented in this way with X ≡ Σ^{ℕ} [G].

The language for Σ-split subspaces is described in [B] and more briefly in [I, Section 5]. Axioms 7.9 and 7.10 above are special cases of Axioms 5.14 and 5.15 in [I]. Another example (the main subject of [I]) is the Dedekind-cut representation ℝ ↣ Σ^{ℚ} × Σ^{ℚ}, for which the existence of the Σsplitting is equivalent to the Heine–Borel theorem. However, in this paper we have avoided using the general construction by taking ℝ as a base type and the Heine–Borel theorem as Axiom 9.5.

Besides being complicated to work with, Σ-split subspaces are not really appropriate for the concepts that we wish to discuss here. Any Σ-split subspace of a locally compact space is locally compact, but this need not be true of a compact subspace of a non-Hausdorff locally compact space (or of an overt subspace of a non-discrete one).

The system of types including the constructor Σ^{(−)} cannot be generalised to allow such subspaces if we want to retain an interpretation within traditional general topology, because the exponential Σ^{X} only exists in that category when X is locally compact (Proposition 3.17).

Now, the goal of ASD is to re-axiomatise topology, not the objects that have usurped the name “topological spaces” in the textbooks — larger categories are known in which all exponentials exist. However, the process of adapting these to the principles of ASD is ongoing research that is by no means straightforward and is certainly well beyond the scope of this paper [M].

All that we really need in the rest of this paper is a way of giving names to open, closed, compact and overt subspaces. We shall do this by generalising Axiom 7.9 without 7.10.

Remark 7.13 We shall see that a term Γ ⊢ a : X belongs to one of these kinds of subspaces if it satisfies a certain equation f(a) = g(a) between terms of some type Z. For example, open and closed subspaces are defined by the equations αx ⇔ ⊤ and ωx ⇔ ⊥ with Z ≡ Σ, and we will use Z ≡ Σ^{Σ^{X}} for compact subspaces. Thus membership means that the composites

[figure: Γ; a; X; f; g; Z]

are equal. The subspace that we require is therefore the equaliser of this parallel pair, which is tested by any context Γ, i.e. by terms with parameters and satisfying equational hypotheses. This is general categorical language that in no way depends on either set theory or traditional topology.

The problem with the textbook categories of topological spaces is that locally compact spaces admit the exponentials Σ^{(−)} that we require, but not equalisers, whilst the usual category of “all” spaces has equalisers but not exponentials. In a future, more general, formulation of ASD, we would expect to have both of these, abandoning the traditional categories, but for now we want to retain compatibility.

Definition 7.14 We therefore distinguish between

(a) a type X, belonging to the smaller category, for which Σ^{X} exists and the denotation is locally compact; and

(b) a subspace, belonging to the larger category, for which we may form equalisers but not necessarily exponentials.

In Definition 4.5 we introduced the word statement for any equation between terms, whereas we called the terms themselves propositions or predicates if they are of type Σ or Σ^{X} respectively. The inequality ϕ ⩽ ψ in Notation 7.8 is also a statement, because it is equivalent to the equation ϕ ∧ ψ = ϕ and also to ϕ ∨ ψ = ψ.

Axiom 7.15 A subspace of a space X is defined by putting a statement 𝔭(x) (with no parameters besides x) on the right of the divider in the notation

{x : X | 𝔭(x)},

where 𝔭(x) may be ϕx ⇔ ψx, ϕx ⇒ ψx, ϕx ⩽ ψx, fx = gx or a conjunction of these.

Then any term a of type X (which may now contain parameters) is called a member or element of the subspace,

… ⊢ a ∈ {x : X | 𝔭(x)}, if it satisfies the statement … ⊢ 𝔭(a).

We therefore use this notation according to the familiar idiom of comprehension, but its axiomatic force is exactly that the map denoted by a has equal composites with the parallel pair whose equaliser defines the subspace in Remark 7.13.

The denotation of a subspace is the equaliser computed in the traditional category of topological spaces.

Membership or elementhood of a general subspace is therefore another species of statement, whereas that of an open subspace is a proposition. As we intended, the distinction between propositions and statements in logic matches that between open and general subspaces in topology.

Once again we stress that our “comprehension” is not set theory: we have just given the symbolic rules that allow us to introduce and eliminate the symbols {} and ∈, as we did earlier for relations, connectives, quantifiers, descriptions, Dedekind cuts and the λ-calculus. Indeed, for general subspaces, the only situation in which the curly brackets are meaningful is together with the ∈ symbol.

Remark 7.16 In the next section we want to use the subspace notation to prove that any compact subspace of a Hausdorff spaces is closed.

However, instead of an a priori set-theoretic notion of general subspace that can be closed or compact as a secondary property, Axiom 7.15 provides one construction of a subspace based on the data for compactness, and another based on the idea that it is closed, both by means of equalisers. In other words, we are given the compact and closed subspaces separately, and need to show that they are isomorphic.

However, instead of defining mutually inverse maps between the two objects, there is a categorical technique (with its origins in sheaf theory) known as using generalised elements. These are incoming maps from an arbitrary object Γ of the category. By considering the two objects in each of the roles, this establishes the isomorphism: we just have to show that these incoming maps are in bijection.

The beauty of this method is that it requires exactly the same piece of reasoning as (both the set-theoretic language and also) the symbolic one in our new calculus. By Definition 5.3, an incoming continuous function is a term possibly containing parameters, and the generic such term is a variable.

However, along with the parameters come assumptions (Definition 5.2), so we have

Definition 7.17 For statements 𝔭(x) and 𝔮(x) involving only the variable x : X, we write

{x : X | 𝔭(x)} ⊂ {x : X | 𝔮(x)} ⊂ X  if  x : X, 𝔭(x) ⊢ 𝔮(x)

and say that one subspace is contained in or a subspace of the other. If both of the containments hold then we say that these subspaces are equal. Similarly, we write

{x : X | 𝔭(x)} ∩ {x : X | 𝔮(x)} ≡ {x : X | 𝔭(x) & 𝔮(x)}

for their intersection, where & is the conjunction of statements that we mentioned in Definition 4.5. (The union is a more delicate issue.)

These rules agree with our definition of membership. Hence the subspaces are syntactic sugar: they actually not needed at all, because we can just reason with the language of terms and statements.

In the next section we will begin to use this notation for compact subspaces, but first we apply it to open and closed ones, beginning with an example of Axiom 7.15:

Examples 7.18 For any term a : X, we then have, as in Definition 4.5,

a ∈ U ≡ {x : X | αx ⇔ ⊤} iff αa ⇔ ⊤
a ∈ C ≡ {x : X | ωx ⇔ ⊥} iff ωa ⇔ ⊥.  □

We can also show that any function (Definition 5.3) is continuous in the sense that the inverse image of any open or closed subspace is again open or closed respectively.

Definition 7.19 The inverse image of a predicate ϕ : Σ^{Y} along a function f : X → Y is given by composition. There are several notations for this, coming from different disciplines:

f^{∗}ϕ ≡ f^{−1}ϕ ≡ Σ^{f}ϕ ≡ (f ; ϕ) ≡ (ϕ · f) ≡ λx. ϕ(fx) : Σ^{X}.

The corresponding open and closed subspaces of X are

f^{−1}{y : Y | αy} ≡ {x : X | α(fx)} and f^{−1}{y : Y | ¬ωy} ≡ {x : X | ¬ω(fx)}.

Lemma 7.20 These are indeed the inverse images in a sense that is consistent with our definitions of membership for a : X:

a ∈ f^{−1}{y : Y | αy} ; = ; fa ∈ {y : Y | αy}  and  a ∈ f^{−1}{y : Y | ¬ωy} ; = ; fa ∈ {y : Y | ¬ωy}  □

Whilst open and closed subspaces have inverse but not direct images under general continuous functions, we shall see in Theorem 8.9 and Notation 11.13 respectively that it is the other way round for compact and overt ones.

Since the traditional categories do not admit all of the structure that we would like, the question of what is the appropriate general notion of topological space remains a matter of debate. We shall therefore only use the subspace notation in a suggestive way, restricting our attention to those compact or overt subspaces that are also (either given or may be shown to be) open or closed.

Since ℝ is Hausdorff, this presents no problem for the compact subspaces that primarily interest us, and the next section unashamedly exploits that simplification. On the other hand, there are overt subspaces that are neither open nor closed, arising from singular ♢-operators (Section 2). However, the worst example that I have been able to find (Remark 16.14) is locally closed and therefore still locally compact.

8 Abstract compact subspaces

Although our abstract re-axiomatisation is not quite complete (there are still two axioms to come, in the next section), we now have enough tools to fashion an account of the usual properties of compact subspaces based on the modal operator □ from Section 2. As in the traditional way in which compactness is taught, it seems to be easier to begin with compact subspaces of a Hausdorff space, and then consider compact spaces as a special case.

In Section 6 it was enough to refer to the open subsets such as δ and υ as propositional formulae. However, following Notation 2.14, we shall now need to use a “general” or “arbitrary” open subspace ϕ in a test of the form □ ϕ to examine compact subspaces. This is why we needed to introduce λ-abstraction in the previous section.

In Section 2 we wrote □ U for the property that a compact subspace K is contained in an open one U. Now we shall allow □ to stand for an expression that may quite naturally contain variable parameters. This will enable us to treat abstract compact subspaces as intermediate expressions in the course of calculations that have real-valued inputs and outputs, such as the solution of polynomial equations. Working with higher-type expressions is much simpler, both notationally and conceptually, than trying to understand what it means for a compact set K to depend continuously on parameters.

Definition 8.1 An abstract compact subspace of a Hausdorff space H is defined by its necessity modal operator. This is an expression □, possibly containing parameters, that yields a proposition (term of type Σ) when applied to an open subset (term of type Σ^{H}), so by Axiom 7.4 its own type is Σ^{Σ^{H}}.

As in Notation 2.14, □ must satisfy, for any predicate-expression ϕ : Σ^{H},

□ ϕ ⇔ ⊤ ⊣⊢ ϕ ∨ ω = ⊤  where  ωx ≡ □(λy. x ≠_{H} y).

If we want to name the subspace, we write [K]ϕ instead of □ ϕ. The intended meaning is that the compact subspace K represented by □ is contained in (or covered by) the open subspace classified by ϕ.

In English, the formula ωx ≡ □(λy. x ≠ y) reads: “x belongs to the complementary open subspace (called W in Section 2) iff, necessarily for any y in the subspace, x is separated from y”. The symbol □ says “necessarily, in the compact subspace”, whilst ≠ denotes separation in a Hausdorff space (Definition 4.8).

Proposition 8.2 For a : H, σ : Σ, ϕ, ψ : Σ^{H} and θ : Σ^{H_{1}×H_{2}}, □ operators obey

(a) uniqueness: if □ and □′ both satisfy the definition for the same ω then □ = □′;

(b) preservation of meets: □ ⊤ ⟺ ⊤ and □(ϕ ∧ ψ) ⟺ □ ϕ ∧ □ ψ;

(c) the (dual) Frobenius law: □(λx. σ ∨ ϕx) ⟺ σ ∨ □ ϕ;

(d) relative instantiation: □ ϕ ⟹ ϕa ∨ ωa;

(e) substitution into any expression to which □ is applied; and

(f) commutativity: [K_{1}](λx. [K_{2}](λy. θxy)) ⟺ [K_{2}](λy. [K_{1}](λx. θxy)). Proof [a] For any ϕ, by hypothesis □ ϕ ⇔ ⊤ ⊣⊢ ϕ ∨ ω ⇔ ⊤ ⊣⊢ □′ ϕ ⇔ ⊤, so □ ϕ ⇔ □′ ϕ by Axiom 5.6. [b] ⊤ ∨ ω = ⊤, whilst

ϕ ∨ ω = ψ ∨ ω = ⊤ ⊣⊢ (ϕ ∨ ω) ∧ (ψ ∨ ω) = ⊤ ⊣⊢ (ϕ ∧ ψ) ∨ ω = ⊤

by distributivity. [c] Putting F σ ≡ □(λx. σ ∨ ϕx) in Proposition 5.8, we have

F ⊤ ≡ □(λx. ⊤ ∨ ϕx) ⇔ □(λx. ⊤) ≡ □ ⊤ ⇔ ⊤

and F ⊥ ≡ □(λx. ⊥ ∨ ϕx) ⇔ □(λx. ϕx) ≡ □ ϕ,

so □(λx. σ ∨ ϕx) ≡ F σ ⇔ F ⊥ ∨ σ ∧ F ⊤ ⇔ □ ϕ ∨ σ ∧ ⊤ ⇔ □ ϕ ∨ σ.

[d] Relative instantiation is the forward direction of the defining rule (using Axiom 5.6 and λ-application) and [e] the substitution property is simply that for λ-application (Axiom 7.7).

[f] Using the Definition and Axiom 5.6, (equality with ⊤ of) the left hand side of the commutative law is equivalent to

…, x : H  ⊢ ω_{1}x ∨ [K_{2}](λy. θxy) ⇔ ⊤
…, x : H, ω_{1}x ⇔ ⊥  ⊢ [K_{2}](λy. θxy) ⇔ ⊤
…, x, y : H, ω_{1}x ⇔ ⊥  ⊢ ω_{2}y ∨ θxy ⇔ ⊤
…, x, y : H, ω_{1}x ⇔ ω_{2}y ⇔ ⊥ ⊢ θxy ⇔ ⊤
…, x, y : H  ⊢ ω_{1}x ∨ ω_{2}y ∨ θxy ⇔ ⊤,

which is symmetric, so agrees with the other side. □

Definition 8.3 If □ is covered by ϕ then ϕ is called a neighbourhood of □. A point a : H (by which we mean an expression that may contain parameters) belongs to all such neighbourhoods ϕ if

□ ϕ ⟹ ϕa, or □ ⩽ λϕ. ϕa : Σ^{Σ^{H}}

using Notation 7.8. This agrees with

a ∈ K,  where  K ≡ {x : H | □ ⩽ λϕ. ϕx}

is defined using Notation 7.15, so we say that a is a member of □.

Warning 8.4 Without the Hausdorffness assumption (and interpreting it in traditional topology), this definition need not recover membership of a given compact subspace, but may give a larger one, called the saturation [HM81].

Example 8.5 Any point of a Hausdorff space defines a compact subspace K ≡ {a}, with [K]ϕ ≡ ϕa and ωx ≡ (x ≠ a), by Lemma 5.9. Then [K] preserves meets and joins, cf. Proposition 2.15(d).

□

Definition 8.6 We say that a compact subspace K is occupied if [K]⊥ ⇔ ⊥, whereas [K]⊥ ⇔ ⊤ iff K ≅ ∅, cf. Proposition 2.15(c).

Any compact subspace that has a definable point is occupied, but not conversely. For example, we shall see that any function 𝕀 → ℝ attains its bounds (or any particular intermediate value) on an occupied subspace (Corollaries 12.13 and 13.11), but not necessarily at any point of it (Example 16.15). To appreciate why the word was chosen, imagine going into a hotel room to find someone else’s luggage already there, but not the actual person. The more familiar notion of inhabitedness says that a point exists, so it will be related to ∃ and ♢ for overt subspaces in Definition 11.5. When we return to the intermediate value theorem in Section 14, we shall see that the fact that occupied subspaces need not have points exactly explains the difference between the classical and constructive views of the result (Corollary 14.16).

Proposition 8.7 Any compact subspace of a Hausdorff space is closed. Proof As we explained in Remark 7.16, we have to show that the two subspaces that are defined from the data for compactness and closedness are isomorphic. We do this by proving that their defining statements,

□ ϕ ⟹ ϕx  and  ωx ⟺ ⊥,

are equivalent. If the first holds then, putting ϕ ≡ λy. (x ≠ y) in the first form of Definition 8.3,

ωx ≡ □(λy. x ≠ y) ⟹ (λy. x ≠ y)x ≡ (x ≠ x) ≡ ⊥.

Conversely, if ωx ⇔ ⊥ then □ ϕ ⇒ ϕx for any ϕ : Σ^{H}, by Proposition 8.2(d). □

Examples 8.8 The empty subspace is compact, as are binary unions and intersections of compact subspaces of a Hausdorff space.

\begin{matrix}K & ωx & [K]ϕ \\ ∅ & ⊤ & ⊤ \\ K_{1} ∪ K_{2} & ω_{1}x ∧ ω_{2}x & [K_{1}]ϕ ∧ [K_{2}]ϕ \\ K_{1} ∩ K_{2} & ω_{1}x ∨ ω_{2}x & [K_{1}](ϕ ∨ ω_{2}) ≡ [K_{2}](ϕ ∨ ω_{1}) \end{matrix}

According to Definition 7.17, the intersection of a pair of subspaces is given by the conjunction (&) of their defining statements, but

(ω_{1}x ⇔ ⊥) & (ω_{2}x ⇔ ⊥) ⊣⊢ (ω_{1}x ∨ ω_{2}x) ⇔ ⊥

is the definition of ∨, so the intersection of the two closed subspaces is closed. The same is true of the compact ones because of the equivalence of closed and compact subspaces of either K_{1} or K_{2} in Theorem 8.15 below. □

Although we have not defined unions of general subspaces, next result shows that what we have called K_{1} ∪ K_{2} is the direct image of the coproduct (disjoint union) K_{1} + K_{2}.

Theorem 8.9 Let f : X → Y be a function (Definition 5.3) between Hausdorff spaces, and let K be a compact subspace of X. Then

[fK]ψ ≡ [K](f^{∗}ψ) ≡ [K](λx. ψ(fx))

defines a compact subspace fK ⊂ Y, called the direct image of K. If a : X is a member of K ⊂ X then fa : Y is a member of fK ⊂ Y, and fK is occupied iff K is.

Conversely, f : K ↠ fK is a proper surjection in the sense that the inverse image f^{−1}(y) ∩ K ⊂ X of each y ∈ fK ⊂ Y is compact and occupied. Proof Since X and Y are Hausdorff, we may define

ξx ≡ [K](λx′. x ≠ x′) and ωy ≡ [fK](λy′. y ≠ y′) ≡ [K](λx. y ≠ fx).

By hypothesis, [K]ϕ ⇔ ⊤ iff ϕ ∨ ξ = ⊤ : Σ^{X}, and we have to show that [fK]ψ ⇔ ⊤ iff ψ ∨ ω = ⊤ : Σ^{Y}.

(ψ ∨ ω)(fx) ≡ ψ(fx) ∨ [K](λx′. fx ≠ fx′)  def ω
⇒ ψ(fx) ∨ [K](λx′. x ≠ x′)  Lemma 5.9
≡ (ψ · f ∨ ξ)x  def ξ
(ψ ∨ ω)(y) ⇔ ψy ∨ [K](λx. fx ≠ y)  def ω
⇔ [K](λx. ψy ∨ fx ≠ y)  Proposition 8.2(c)
⇔ [K](λx. ψ(fx) ∨ fx ≠ y)  Lemma 5.9
⇐ [K](λx. ψ(fx)) ≡ [fK]ψ.  Axiom 5.7

If ψ ∨ ω = ⊤ : Σ^{Y} then (ψ · f ∨ ξ) = ⊤ : Σ^{X}, so [K](ψ · f) ≡ [fK]ψ ⇔ ⊤, by the first part. Conversely, from the second, if [fK]ψ ⇔ ⊤ then (ψ ∨ ω) = ⊤ : Σ^{Y}.

If a ∈ K, so [K]ϕ ⇒ ϕa, then [fK]ψ ≡ [K](ψ · f) ⟹ (ψ · f) a ≡ ψ(fa), so fa ∈ fK. Also, [fK]⊥ ≡ [K](⊥ · f) ≡ [K]⊥ ⇔ ⊥.

Since Y is Hausdorff, {y} and f^{−1}(y) are closed, by Lemma 7.20. the intersection f^{−1}(y) ∩ K exists, and is closed and compact by Example 8.8, with

[f^{−1}(y) ∩ K]ϕ ⟺ [K](λx. y ≠_{Y} fx ∨ ϕx),

so [f^{−1}(y) ∩ K]⊥ ⟺ [K](λx. y ≠_{Y} fx) ≡ ωy.

Hence f^{−1}(y) ∩ K is occupied iff y ∈ fK ⊂ Y. □

We now turn from subspaces to spaces.

Definition 8.10 A space K is compact if it has a universal quantifier, written ∀_{K}, such that, for x : K and ϕ : Σ^{K},

∀_{K}⊤ ⇔ ⊤  and  ∀_{K}ϕ ⟹ ϕx,

the latter being called the absolute instantiation rule. In other words, K is a compact subspace of itself with ω ≡ ⊥, and any expression of type K is a member of □ in the sense of Definition 8.3. (This simple definition is sufficient because of Axiom 5.6.)

We look at the logical meaning of this before the topological one.

Notation 8.11 We shall write ∀x:K. ϕx for ∀_{K}ϕ when K is a compact space, and by extension also when it is a compact subspace, i.e. for [K]ϕ. This simply means that we replace the notation

□(λx:K. \begin{matrix}− \\ − \end{matrix}) by ∀x:K. \begin{matrix}− \\ − \end{matrix}.

This use of logical notation is justified by Proposition 8.2 and the following rules of inference.

Warning 8.12 The quantifier ∀ must be understood strictly according to the rules in this section, cf. Remark 5.1. It does not mean “for every definable point”. There is an occupied compact subspace that has no points at all (Example 16.15) and even the real interval 𝕀 may satisfy ⊢ ϕa for every term ⊢ a : 𝕀 but not ∀x:𝕀. ϕx [I, Section 15].

Theorem 8.13 In a compact space, ∀_{K} satisfies the two-way rule on the left:

…, x : K ⊢ σ ⇒ ϕx ; = ; … ⊢ σ ⇒ ∀x:K. ϕx.  …, x : H, ωx ⇔ ⊥ ⊢ σ ⇒ ϕx ; = ; … ⊢ σ ⇒ □ ϕ.

where σ : Σ must not involve the variable x : K. This is the dual of Axiom 5.10 for ∃. Similarly, in a Hausdorff space H, the modal operator □ and co-classifier ω for a compact subspace satisfy the rule on the right. Proof By Axiom 5.6 and Notation 7.8, the rule on the right above is

…, x : H, σ ⇔ ⊤ ⊢ ⊤ ⇒ ϕx ∨ ωx ; = ; …, σ ⇔ ⊤ ⊢ ⊤ ⇒ □ ϕ  or  …, σ ⇔ ⊤ ⊢ ⊤ = ϕ ∨ ω : Σ^{H} ; = ; …, σ ⇔ ⊤ ⊢ ⊤ ⇒ □ ϕ

which is Definition 8.1. The other rule is the special case where ωx ≡ ⊥. □

Lemma 8.14 In a compact Hausdorff space, ϕx ⟺ ∀y. (x ≠ y) ∨ ϕy. Proof This is the dual of Lemma 5.14 for overt discrete spaces.

…, x, y : K ⊢ ϕx ⇒ (x ≠ y) ∨ ϕy  Lemma 5.9
…, x : K ⊢ ϕx ⇒ ∀y. (x ≠ y) ∨ ϕy  Theorem 8.13
⇒ (x ≠ x) ∨ ϕx  y ≡ x, Definition 8.10
⇔ ϕx.  □

From this we deduce the familiar topological result.

Theorem 8.15 The closed and compact spaces of a compact Hausdorff space agree, where

ωx ≡ □(λy. x ≠ y) and □ ϕ ≡ ∀_{K}(ϕ ∨ ω) ≡ ∀x:K. ϕx ∨ ωx

translate between ω and □. Proof When the ambient space is compact, the right hand side of the rule in Definition 8.1 is equivalent to ∀_{K}(ϕ ∨ ω) ⇔ ⊤, so these two equations re-state that Definition. Proposition 8.7 showed that the two notions of membership agree.

The translation ω ↦ □ ↦ ω′ is the identity by Lemma 8.14:

ω′x ≡ □(λy. x ≠ y) ≡ ∀_{K}(λy. x ≠ y ∨ ωy) ⇔ ωx.

So too is that □ ↦ ω ↦ □′, by Axiom 5.6 and because

□′ ϕ ⇔ ⊤ ⊣⊢ ∀_{K}(ϕ ∨ ω) ⇔ ⊤ ⊣⊢ ϕ ∨ ω = ⊤ ⊣⊢ □ ϕ ⇔ ⊤.  □

Being compact as a subspace was defined in terms of the topology of the ambient space. Before we can say that the subspace is compact as a space in its own right, we have to define its own topology. We can do this, using Axiom 7.10, if the subspace is also either closed or open. Recall, however, that we may only form the type C from an operator □ if it has no parameters. This is why we prefer to work with this operator instead of the space, and subsequent results will not depend on forming it.

Theorem 8.16 Any compact subspace of a Hausdorff space is itself a compact space. Proof From □ : Σ^{Σ^{H}} define ωx ≡ □(λy. x ≠ y) and C ≡ {x : H | ωx ⇔ ⊤} using Axiom 7.9. Then, by Axiom 7.10, the topology of C has

I : Σ^{C} ≅ {ϕ : Σ^{X} | ω ⩽ ϕ} ↣ Σ^{X},

and we use this Σ-splitting I to define ∀_{C}ψ ≡ □(Iψ). This satisfies absolute instantiation for x : C and ψ : Σ^{C},

∀_{C}ψ ≡ □(Iψ) ≡ □ ψ ⟹ ωx ∨ ψx ≡ ψx

because ωx ⇔ ⊥ and ω ⩽ ψ = Iψ, whilst ∀_{C}⊤ ≡ □(I⊤_{C}) ≡ □ ⊤_{X} ⇔ ⊤. □

Remark 8.17 Returning to logic, the significance of the deduction rule for subspaces (on the right in Theorem 8.13) is that we may treat □ as a bounded universal quantifier.

For example, in Section 10 we shall consider, for d, u : ℝ and ϕ : Σ^{ℝ},

□ ϕ ≡ [d, u]ϕ ≡ ∀x:(d ≤ x ≤ u). ϕx.

That is, we can reason about it as if the subspace

K ≡ {x : H | ¬ωx} = {x : H | □ ⩽ λϕ. ϕx} ⊂ H

were actually a space in its own right (even when ω and □ depend on parameters).

Remark 8.18 This account of compact subspaces has relied on the Hausdorffness assumption, which ought to be enough, given that we intend to study ℝ and ℝ^{n}. However, when we introduce (closed) overt subspaces in Section 11, we would like to do so in the form of the lattice dual of the theory of (open) compact subspaces (cf. Axiom 5.6), whereas ℝ does not enjoy the dual property to Hausdorffness, which is discreteness. A small detour from the topology of ℝ^{n} is therefore appropriate.

There are ample supplies of open compact subspaces in

(a) Cantor space, with the “middle third” construction, where they are finite unions of “whole segments” of diameter 3^{−n} for some n;

(b) Cantor space, considered as the space of paths through an infinite binary tree, where they are determined by a finite sub-tree;

(c) Σ^{ℕ}, whose denotation is P(ℕ) with the Scott topology, where they are determined by finite subsets on ℕ;

(d) ℝ^{n} with the Zariski topology, in which each polynomial f defines a basic open subspace W_{f} ≡ {x | fx ≠ 0} that is also compact in this topology.

Definition 8.19 A compact open subspace of a (not necessarily Hausdorff) space X is defined by a pair (□, α), where □ : Σ^{Σ^{X}} and α : Σ^{X} satisfy

□ ϕ ⇔ ⊤ ⊣⊢ α ⩽ ϕ

for any ϕ : Σ^{X}. Equivalently (by Axiom 5.6), □ ϕ ∧ αx ⟹ ϕx and □ α ⇔ ⊤.

Exercise 8.20 Show that

(a) if □ and □′ both satisfy the definition for the same α then □ = □′;

(b) if α and α′ both satisfy the definition for the same □ then α = α′;

(c) □ satisfies Proposition 8.2, but the relative instantiation rule is □ ϕ ∧ αa ⇒ ϕa, and each side of the commutative law is equivalent to

x, y : X, α_{1}x ⇔ α_{1}y ⇔ ⊤ ⊢ ϕxy ⇔ ⊤;

(d) any term a : X is a member of □ in the sense of Definition 8.3 (□ ⩽ λϕ. ϕa) iff it is a member of the open subspace classified by α (αa ⇔ ⊤); and

(e) the rule of inference in Theorem 8.13 becomes

…, x : X, αx ⇔ ⊤ ⊢ σ ⇒ ϕx = … ⊢ σ ⇒ □ ϕ.

(f) Any compact open subspace is a compact space, with ∀_{U}ψ ≡ □(Iψ), because I⊤ = α.

9 Compactness and uniformity

What has happened to the “finite open sub-cover” property? Somehow, the underlying ideas of ASD are already robust enough to allow us to develop the basic results about compactness, without mentioning finiteness. On the other hand, we can only define some rather trivial examples of compact spaces.

We need two more axioms to complete our theory. They say explicitly that all functions are Scott-continuous, and that [0, 1] ⊂ ℝ is compact in the sense of the previous section. These ideas were motivated by the infinitary and finitary parts respectively of the discussion of compactness in Notation 2.14. Our goal in this section is to use them to show that the compact subspaces of ℝ are exactly the closed and bounded ones.

Axiom 9.1 For any type X, every term F : Σ^{Σ^{X}} is Scott-continuous, i.e. it preserves directed joins, cf. Proposition 3.13.

As we explained following Axiom 5.10, a join indexed by i : I in the space Σ^{X} is an existentially quantified predicate, λx. ∃i. θ(x, i). To state the Axiom in its general form, the object I must be therefore be overt, and in practice we take it to be discrete too. See [I, Definition 4.20] for this general definition of directed joins in ASD.

However, we don’t usually need the generality in this paper because, for a great many of the issues of real analysis, it is enough to consider joins indexed by the arithmetical order on ℕ or ℚ, as we observed in Remark 3.15.

Definition 9.2 A directed relation on a space X is a predicate θ(x, i) with x : X, i : ℕ, ℚ or ℝ, and maybe other parameters, that preserves or reverses the arithmetical order in the second argument, in one or other of the following senses:

θ(x, i) ∧ (i < j < ∞) ⟹ θ(x, j)  (i↗∞)
θ(x, j) ∧ (0 < i < j) ⟹ θ(x, i).  (i ↘ 0)

We adopt the notation on the right from pre-axiomatic analysis because it is a useful mnemonic, not because i “tends” towards anything. It can easily be generalised to i↗a or i↘a.

As we saw earlier, such a relation corresponds to a semicontinuous function from X, or a ℚ-indexed family of open subsets of it. When the “finite open sub-cover” property of a compact space K is used in familiar ways in real analysis, we shall see that a relation like this lies at the core of the argument. As Proposition 10.10 illustrates, the order-preserving property is usually obvious from the form of θ.

Proposition 9.3 Let θ(x, i) be a directed relation on a space X, where i : ℕ or ℚ. Then any F : Σ^{Σ^{X}} satisfies the rule

…, x : X, i, j ⊢ (i < j) ∧ θ(x, i) ⟹ θ(x, j)
(i↗∞)
… ⊢ F (λx. ∃i. θ(x, i)) ⟹ ∃i. F (λx. θ(x, i))

or

…, x : X, i, j ⊢ (0 < i < j) ∧ θ(x, j) ⟹ θ(x, i)
(i↘0).
… ⊢ F (λx. ∃i > 0. θ(x, i)) ⟹ ∃i > 0. F (λx. θ(x, i))

Proof In the first case, the indexing space is ℕ or ℚ with the arithmetic order, which the binary operation max makes directed. The second case uses {i : ℚ | i > 0} with the reverse order and min.

□

We shall see in Corollary 10.3 that these rules are also valid with real instead of rational values of i.

Although this result holds for any functional F on any space X, the most important application is to the necessity operator □ or quantifier ∀ for a compact subspace K ⊂ X in the sense of the previous section. Then we have the following uniformity principle.

Corollary 9.4 For any directed relation θ(k, i) on a compact space K,

∀k:K. ∃i. θ(k, i)  ⟹ ∃i. ∀k. θ(k, i)  i↗∞
or  ∀k:K. ∃i > 0. θ(k, i) ⟹ ∃i > 0. ∀k. θ(k, i).  i↘0 □

We can say things like this exactly because ours is a logic for topology and not set theory (Remark 5.1), but in order to exploit this principle in real analysis, we need to state the final axiom:

Axiom 9.5 The closed interval [0, 1] ⊂ ℝ is compact.

The closed subspace [0, 1] is co-classified by ωx ≡ (x < 0) ∨ (1 < x), by definition, so we are now saying that it also has a modal operator □ for which the pair (□, ω) satisfies Definition 8.1. This is unique by Proposition 8.2(a).

There’s nothing special about 0 and 1 in this:

Proposition 9.6 The closed interval [d, u] ⊂ ℝ, whose endpoints d, u : ℝ may be variables or expressions with parameters, is the closed subspace co-classified by

ωx ≡ x < d ∨ u < x,

and is a compact subspace, with

[d, u]ϕ ≡ ∀x:(d ≤ x ≤ u). ϕx ≡ ∀t:[0, 1]. ϕ(d(1 − t) + ut).

Proof This is an application of Theorem 8.9 and Remark 8.17. □

It is a serendipitous notational coincidence that the bracket notation [d, u] serves for both the compact subspace and its modal operator.

Remark 9.7 All compact subspaces of ℝ are closed, by Proposition 8.7, so the next question is whether, given a closed subspace, it is compact iff it is bounded. However, the meaning of “boundedness” requires some care, especially when we allow parameters.

By the definition of ∀_{K}, the compact subspace K is contained in the open interval (d, u), where d and u may be either variables or general real-valued expressions, but nevertheless specified ones, iff

∀x:K. (d < x < u).  (a)

Since this is a proposition, we may quantify d and u (if they’re variables rather than expressions). So K is bounded with unspecified bounds iff

∃du. ∀x:K. (d < x < u).  (b)

Then (a⇒b) by Axiom 5.10, and Remark 6.6 makes them equivalent, but only when the parameters in the definition of [K] are (at worst) integers or rationals, not real or logical.

Since properties (a,b) use the universal quantifier, we can only state them if we already know that the subspace is compact. On the other hand, the closed subspace co-classified by ω is contained in the open interval (d, u) iff this interval and the complementary open subspace cover ℝ, i.e.

…, x : ℝ ⊢ (d < x < u) ∨ ωx ⇔ ⊤, or λx. (d < x < u) ∨ ωx = ⊤ : Σ^{ℝ}.  (c)

It is contained in the closed interval [d, u] iff its complement contains the complement of this interval (cf. Proposition 3.9), i.e.

…, x : ℝ ⊢ (x < d) ∨ (u < x) ⇒ ωx, or λx. (x < d) ∨ (u < x) ⩽ ω : Σ^{ℝ}.  (d)

The versions of (c,d) on the left (with x free) are judgements (Axiom 5.2), whilst those on the right (with x bound by λ) are statements (Definition 4.5), to neither of which does the ASD calculus in Section 5 allow us to apply an existential quantifier.

Exercise 9.8 Show that (a ⊢ c ⊣⊢ d). For [a ⊢ d], we need

(∀x:K. d < x < u) ∧ (y < d ∨ u < y) ⟹ ωy ≡ (∀x:K. x ≠ y).

For [c ⊢ d], use Axiom 5.6. The converse, [d ⊢ c], is more difficult, since we need to enlarge the interval: choosing d′ < d and u < u′; see [I, Exercises 6.17] for how to mix < and ≤ in ℝ, and in particular how to deal with d′ < d ≤ x ≤ u < u′. □

Once again, we can solve the problem of how to avoid specifying the bounds by generalising the Euclidean reals d and u in property (d) to ascending and descending ones, δ and υ:

Definition 9.9 Let δ and υ be respectively ascending and descending reals in the sense of Definition 6.7, except that we do not yet require them to be disjoint or located (cf. Corollary 9.12). Then we write [δ, υ] ⊂ ℝ for the closed interval (subspace) that is co-classified by δ ∨ υ. We say that another closed subspace, co-classified by ω, is bounded if there are δ and υ with

∃du. δd ∧ υu  and  δ ∨ υ ⩽ ω : Σ^{ℝ}.  (e)

Lemma 9.10 If δ and υ are rounded and bounded (Definition 6.7) then the closed interval [δ, υ] is compact, with modal operator

□ ϕ ≡ ∃du. δd ∧ υu ∧ ∀y:[d, u]. (δy ∨ ϕy ∨ υy).

Proof As in Definition 8.1, from □ we first define

ωx ≡ □(λy. x ≠ y)
≡ ∃du. δd ∧ υu ∧ ∀y:[d, u]. (δy ∨ (x ≠ y) ∨ υy)
⇒ ∃du. δd ∧ υu ∧ (x < d ∨ δx ∨ υx ∨ u < x)
⇒ δx ∨ υx,  δ lower, υ upper

which follows from relative instantiation (Proposition 8.2(d)) for [d, u]. Conversely, since δ and υ are bounded there are some d and u with δd ∧ υu, so by Theorem 8.13,

δx ∨ υx ⟹ ∃du. δd ∧ υu ∧ ∀y:[d, u]. (δy ∨ (x ≠ y) ∨ υy) ≡ ωx.

For Definition 8.1, we need ϕ∨ω ≡ δ∨ϕ∨υ ⇔ ⊤ ⊣⊢ □ ϕ, in which ⊢ follows from boundedness and ∀I, and ⊣ from roundedness. □

The modal operator □ for the interval [δ, υ] has a simpler expression:

Proposition 9.11 □ ϕ ⇔ [δ, υ]ϕ ≡ ∃du. δd ∧ υu ∧ ∀x:[d, u]. ϕx. Proof In the special case where δ ≡ δ_{e} ≡ λd. d < e and υ ≡ υ_{t} ≡ λu. t < u,

□ ϕ ≡ ∃du. (d < e) ∧ (t < u) ∧ ∀y:[d, u]. (y < e) ∨ ϕy ∨ (t < y)
⇒ ∀x:[e, t]. ϕx.

We can extend this to the general case by using (general) Scott continuity of the formula F δυ ≡ □ ϕ with respect to δ and υ, with ϕ as a parameter:

□ ϕ ≡ F δυ ⇒ F (λd. ∃e. δe ∧ δ_{e}d, λt. ∃t. υt ∧ υ_{t}u)  roundedness
⇒ ∃et. δe ∧ υt ∧ F (δ_{e}, υ_{t})  Scott continuity
⇒ ∃et. δe ∧ υt ∧ ∀x:[e, t]. ϕx ≡ [δ, υ]ϕ,  above

and the implication is reversible by monotonicity. □

Corollary 9.12 The interval [δ, υ] is occupied iff δ and υ are disjoint in the sense that

δd ∧ (u < d) ∧ υu ⟺ ⊥,

cf. [I, Lemma 7.5], but empty iff they overlap. Proof We have □ ⊥ ≡ ∃du. δd ∧ υu ∧ ∀x:[d, u]. ⊥ ⟺ ∃du. δd ∧ υu ∧ (d > u). This is ⊥ iff δ and υ are disjoint in the sense given, and ⊤ iff they overlap. □

Now we are able to clarify the issues in Remark 9.7.

Proposition 9.13 Every (parametric) compact subspace of ℝ is bounded in the sense of Definition 9.9. Proof Given the modal operator □ of a compact subspace K, let

ωx ≡ □(λk. x ≠ k),  δd ≡ □(λk. d < k)  and  υu ≡ □(λk. k < u),

so δ ∨ υ ⩽ ω, whilst δ is lower and υ is upper.

In order to show that ∃u. υu, we use uniformity with respect to the directed relation θ(x, u) ≡ (x < u) as u↗∞, cf. Remark 3.15; the left-hand side holds with u ≡ k + 1:

⊤ ⟹ □(λk:K. ∃u:ℝ. k < u) ⟹ ∃u:ℝ. □(λk:K. k < u).

Then υ is rounded because, by Corollary 9.4,

υu ≡ □(λk. k < u) ⇔ □(λk. ∃ε > 0. k < u − ε)  ε ≡ \frac{1}{2}(u − k)
⇔ ∃ε > 0. □(λk. k < t − ε)  ε↘0
≡ ∃ε > 0. υ(t − ε) ⇔ ∃t. (t < u) ∧ υt.

Similarly, δ is rounded lower and bounded, and we may choose d and u so that δd ∧ (d < u) ∧ υu. Hence δ and υ satisfy Definition 9.9. □

Remark 9.14 The supremum of the compact subspace need not exist as a real number (Dedekind cut), but υ provides it as a descending real. This is the intersection of the families of upper bounds of the elements of K: we may form an infinitary intersection of open subspaces like this because it is indexed by a compact set. Since, for descending reals, the intrinsic order with which we form this intersection is the opposite of the arithmetical order (Remark 3.10), we have the supremum of K, as in Remark 3.6(a).

Theorem 9.15 Any closed subspace of ℝ is compact iff it is bounded. Proof By Theorem 8.15 and Propositions 9.11 and 9.13. □

Remark 9.16 Notice that each direction of the proof uses one of the two axioms introduced in this section, so let’s say something about their necessity.

To do this we have to say what we mean by “the real line” in settings that are very different from topology. We take ℝ to be the object of “Dedekind reals” that is defined in [I, Remark 6.9] as an equaliser of exponentials. This exists in each of the following categories:

(a) The classical category of posets and monotone functions satisfies the rest of the theory apart from Scott continuity, where Σ^{X} is the lattice of upper subsets of X. In this model, every object is compact and overt in the formal senses of Sections 8 and 11. In particular the whole line is compact but not bounded.

(b) In the category of dcpos (directed-complete partial orders) and Scott-continuous functions, the specialisation order determines the topology (cf. Remark 3.10 and Proposition 3.13). Hence every Hausdorff space is discrete and its topology is a full powerset, so the only compact Hausdorff spaces are finite ones. In particular, no non-trivial interval is compact.

Note that we are only saying that these categories obey all but one of the axioms that are stated in this paper: the full (current) ASD theory is stronger than this.

In Russian Recursive Analysis and Bishop’s Constructive Analysis (b) also fails [BR87]. You may therefore be surprised that ASD has both the Heine–Borel theorem and a computable interpretation. This is explained in [I, Section 15].

10 Continuity on the real line

Now that the calculus is complete, we can use it to express some familiar ideas in elementary analysis such as continuity, differentiability and Riemann integration.

Remark 10.1 Classically, a point x is said to be in the interior of a subset U ⊂ ℝ if x ∈ (d, u) ⊂ U for some d, u : ℝ. For any d < e < x < t < u, this is equivalent to

∃et. x ∈ (e, t) ⊂ [e, t] ⊂ (d, u) ⊂ U,

which states local compactness of ℝ (cf. Definition 3.18). This can be formulated in the ASD λ-calculus, because we can use the universal quantifier to say when a closed interval is contained in an open subspace.

Theorem 10.2 Every point a : ℝ that is a member of the open subspace classified by ϕ : Σ^{ℝ} is in its interior, in the sense that

ϕa ⟺ ∃du. (d < a < u) ∧ ∀k:[d, u]. ϕk ≡ ∃δ > 0. ∀k:[a ± δ]. ϕk.

Proof This uses the uniformity principle (Corollary 9.4) that we derived from Scott continuity of the universal quantifier. However, since in this case the existentially quantified variable δ is a parameter of the universal quantifier ∀k : [a ± δ] itself, we reformulate the problem, using the directed relation θ(k, δ) ≡ (|k − a| > δ) ∨ ϕk with δ ↘0. Then

…, k : [a ± 1] ⊢ ϕa ⇒ (k ≠ a) ∨ ϕk  Lemma 5.9
⇒ ∃δ > 0. (|k − a| > δ) ∨ ϕk  δ ≡ \frac{1}{2}|k − a|
≡ ∃δ > 0. θ(k, δ)  def θ
… ⊢ ϕa ⇒ ∀k:[a ± 1]. ∃δ > 0. θ(k, δ)  Theorem 8.13
⇒ ∃δ > 0. ∀k:[a ± 1]. θ(k, δ)  δ ↘0
⇒ ∃δ > 0. ∀k:[a ± 1]. (|k − a| > δ) ∨ ϕk  def θ
⇒ ∃δ > 0. ∀k:[a ± δ]. ϕk  Theorem 8.15
⇒ ϕa.  k ≡ a □

Before going on, you should pause to consider what we have done. This statement is not true in set theory, that is, for predicates ϕ of the logical generality with which you are familiar. We have proved a Theorem that agrees with topology, by devising a logic with axioms that are themselves appropriate to that subject (Remark 5.1).

This also ties up some loose ends in the foundations of ASD:

Corollaries 10.3 For any predicate ϕ : Σ^{ℝ},

(a) ∃x:ℝ. ϕx ⟺ ∃x:ℚ. ϕx;

(b) ϕ is rounded: ϕy ⟹ ∃x < y < z. ϕx ∧ ϕz; and

(c) ϕ( cut (δ, υ)) ⟺ ∃d < u. δd ∧ υu ∧ ∀x:[d, u]. ϕx.

(d) Also, the compact interval is [δ, υ] = ⋂ ; {[d, u] | δd ∧ υu}. □ Hence, as in Definition 3.3, it doesn’t matter whether we use ℚ or ℝ when we define the

ascending or descending reals, or invoking uniformity in Proposition 9.3. Also, Dedekind cuts (Axiom 6.8) may be eliminated in the same way as descriptions (Lemma 6.3).

It’s time to do some basic real analysis, using this key result.

Theorem 10.4 Every function f : ℝ → ℝ is continuous in the ε–δ sense. Proof For x : ℝ and ε > 0, put ϕy ≡ (|fy − fx| < ε). Then Theorem 10.2 provides the input tolerance, but in the form of a closed interval [x ± δ] instead of the traditional open one:

ε > 0 ≡ (|fx − fx| < ε) ≡ ϕx ⟺ ∃δ > 0. ∀y:[x ± δ]. ϕy,

so ε > 0 ⟹ ∃δ > 0. ∀y:[x ± δ]. (|fy − fx| < ε).  □

Remark 10.5 This statement only differs from the familiar one in that

(a) we put ε on the left of ⇒ because the calculus does not allow us to quantify it, because its range {ε : ℝ | ε > 0} is not compact; but

(b) we use the non-strict inequality |y − x| ≤ δ to bound the quantifier ∀y, since this also has to range over a compact subspace (Section 8), instead of writing a strict inequality on the left of an ⇒.

Remark 10.6 Similarly, any function of two variables is jointly continuous in the sense that

ε > 0 ⟹ ∃δ > 0. ∀x′:[x ± δ]. ∀y′:[y ± δ]. (|fx′y′ − fxy| < ε),

i.e. with the sup metric on ℝ × ℝ, so its topology Σ^{ℝ×ℝ} is the usual Tychonov one. □

When we want to interchange limiting processes in analysis such as sums of power series, and in integration and differentiation, we know that the δs that they involve have to exist uniformly in the other variables. Uniformity is essentially the ability to interchange quantifiers, as we saw in the previous section. We can use more or less the same argument that we used for continuity to prove the stronger result:

Theorem 10.7 Any function f : ℝ → ℝ is uniformly continuous on any compact subspace K ⊂ ℝ. Proof Consider the predicate x, y : ℝ, ε > 0 ⊢ ϕ(x, y, ε) ≡ (|fx − fy| < ε). Then, as before,

ε > 0 ⟺ ϕ(x, x, ε) ⟺ ∃δ > 0. ∀y:[x ± δ]. ϕ(x, y, ε).

By the same argument as in Theorem 10.2, with δ ↘0,

ε > 0 ⇒ ∀x:K. ∃δ > 0. ∀y:[x ± δ]. ϕ(x, y, ε)  Theorem 8.13
⇔ ∃δ > 0. ∀x:K. ∀y:[x ± δ]. ϕ(x, y, ε)  Corollary 9.4
⇔ ∃δ > 0. ∀x, y:K. (|x − y| > δ) ∨ (|fx − fy| < ε).  Thm. 8.15 □

Remark 10.8 Here is the translation of our argument into traditional language; it appears to be essentially the one that G.H. Hardy used in [Har08, §107]. Our ϕ classifies

U ≡ {(x, y) | |fx − fy| < ε} ⊂ K × K.

This is a neighbourhood of the diagonal, every point of which lies inside an open δ-ball within U. As the diagonal is compact, finitely many such balls suffice to cover it, and we let δ be their minimum size, which is positive.

Another, much more complicated, argument appears in many textbooks, for example [Dug66, Theorem XI 4.5]. The image of the domain K is a compact subspace of the codomain, so finitely many ε-balls cover its image, and their inverse images cover the domain. Now calculate the Lebesgue number, i.e. the size of the smallest non-empty intersection; this is the required δ.

Although the remaining sections of this paper will study continuous functions, we pause to demonstrate how the definitions of differentiation and integration can be stated in our language. The message is that they naturally yield Dedekind cuts rather than Cauchy sequences, whilst uniformity is captured by Corollary 9.4.

Definition 10.9 Many accounts of differentiability (in my view, the better ones) use the expression

f(x + h) = f(x) + hf′(x) + o(h)

instead of the limit of a quotient. Constructive authors have found it most convenient to define the derivative as the pair, (f, f′), rather than f′ alone. In order to give a definition using Dedekind cuts, we must therefore bound both the derivative and the original function,

e_{0} < f(x) < t_{0} and e_{1} < f′(x) < t_{1}.

We can express this using bounds on the function over some interval around x,

∃δ > 0. ∀h:[0, δ].  e_{0} + e_{1}h < f(x + h) < t_{0} + t_{1}h
∧ e_{0} − t_{1}h < f(x − h) < t_{0} − e_{1}h,

which confines the function to a region in the shape of a “bow tie”, cf. [EL04, §3.1]:

t_{0} + t_{1}h [figure] fx t_{0} ........................................

[figure] t_{0} − e_{1}h  e_{0} + e_{1}h [figure]
[figure: e_{0}]
e_{0} − t_{1}h
[figure: fx; x] x_{0} − δ  x_{0}  x_{0} + δ

Considered as a predicate in (e_{0}, t_{0}) or (e_{1}, t_{1}), this formula

(a) defines a Dedekind cut bounded by (e_{0}, t_{0}) since f : ℝ → ℝ is a function;

(b) is a Dedekind cut bounded by (e_{1}, t_{1}) if f is differentiable at x; but

(c) is a compact interval (Definition 9.9) bounded by (e_{1}, t_{1}) if f is Lipschitz at x. □

Differentiability also gives another example of the relationship between the quantifiers and uniformity.

Proposition 10.10 Any function that is differentiable everywhere in a compact domain K is uniformly differentiable there. Proof Inside all of the quantifiers in the definition of the derivative above there is a propositional expression ϕ(x, h) that does not depend on δ. For any such formula, we note that

(0 < δ < δ′) ∧ ∀h:[0, δ′]. ϕ(x, h) ⟹ ∀h:[0, δ]. ϕ(x, h),

simply because of the range of the quantifier ∀h. Hence, by Corollary 9.4, as δ ↘0,

∀x:K. ∃δ > 0. ∀h:[0, δ]. ϕ(x, h) ⟹ ∃δ > 0. ∀x:K. ∀h:[0, δ]. ϕ(x, h).  □

Remark 10.11 Why can’t we use the same idea to show that any convergent sequence of continuous functions on a compact space converges uniformly, and therefore to a continuous function, cf. Cauchy’s famous error at the end of [Cau21, VI 1]? Indeed, since Definition 6.12 allowed parameters, it actually defined Cauchy sequences and their limits for functions and not just numbers, whilst Theorem 10.4 showed that all functions are continuous.

The explanation is that the constructive definition of convergence requires the modulus to be specified in advance, so it is essentially already uniform convergence anyway.

We could try to write the classical definition, with unspecified modulus μ, as

∀x:K. ∃μ. ∀mn. |a_{n} − a_{m}| < μ( min(m, n)),

and then use Corollary 9.4 to interchange ∀x with ∃μ. However, our logical hygiene (Remark 5.1) prevents this: the quantifiers ∃μ and ∀mn are not permitted in ASD. The first may be allowed in an extended version of the calculus, but ∀mn is expressly forbidden, because ℕ is not compact.

Remark 10.12 Turning to integration, Archimedes obtained his classic estimate 3\frac{10}{71} < π < 3\frac{1}{7} for the area of a circle by in- and circumscribing regular 3 · 2^{n}-gons and calculating their area. More generally, for any d < a < u, where a is the claimed area or volume of the curved figure, there are enclosed and enclosing figures whose magnitudes are more easily calculated (for example, because the figures are rectilinear) and lie within these bounds.

These ds and us form a Dedekind cut, which defines the area or volume a.

Riemann integration generalises Archimedes’ method, but the details are usually over-specified, raising the obligation to check that different methods of division yield the same answer. Using Dedekind cuts completely avoids this.

For the “figures with easily calculated area”, we take step functions. Whilst these are not continuous in the usual sense, they are semi-continuous (Example 3.5), which is anyway more appropriate to defining upper and lower bounds. Then write ∑_{0}^{1} f^{±}x dx for the total areas of the rectangles under these functions. Putting this into our notation is simply a matter of coding arithmetic and inequalities.

Any function f : 𝕀 → ℝ is therefore Riemann-integrable.

For d and u to be under- and over-estimates of ∫_{0}^{1} fx dx, we need to show that

∃f^{+}f^{−}. d < ∑_{0}^{1} f^{−}x dx ∧ ∀x:[0, 1]. f^{−}x < fx < f^{+}x ∧ ∑_{0}^{1} f^{+}x dx < u.

This is a predicate in d and u, for which we write δd ∧ υu : Σ. Clearly δ is lower and υ upper, and they are disjoint since f^{−} < f < f^{+}. They are also rounded, by Corollary 10.3(b), so we just have to show that they are bounded and located. We do this by defining step functions f^{±} whose integrals ∑_{0}^{1} f^{±}x dx differ by less than any given ε > 0, which exist because of uniform continuity of f.

The reason why we have not asserted this as a Theorem is that ∃f^{+}f^{−} quantifies over a hyperspace of step functions (Remark 5.11), so integration is a combinatorial argument that depends on our use of overt discrete spaces in the role of sets. In fact, a step function may be taken to be defined by a list of rationals (the vertices of the jumps), which may in turn be encoded as a single integer. Hence the quantifier is meaningful and the hyper-space is overt, but we shall explain the topological ideas, and the reason for insisting on rationals, in Remark 12.16. □

Remark 10.13 In summary, to what extent does Σ^{ℝ} resemble the usual (“Euclidean”) topology on the real line?

(a) Any open interval (d, u) is an open subspace {x : ℝ | ϕx} with ϕx ≡ (d < x < u);

(b) Σ^{ℝ} has ⊤, ⊥, ∧, ∨ and ∃_{ℕ};

(c) indeed it has ∃_{N} for any overt object N, as we shall see in the next section; but

(d) it does not have “arbitrary” joins;

(e) in particular, we cannot form the interior of an arbitrary subset, i.e. the union of all open subspaces that this contains (Example 16.6);

(f) it has meets indexed by compact spaces, cf. [Nac92]; and

(g) if a point belongs to an open subspace, then some (closed) interval around that point is also contained in the subspace (Theorem 10.2).

Conversely, Theorem 13.15 will show that any open subspace is expressible as a union of disjoint open intervals, and Corollary 15.8 that this expression is unique.

11 Overt subspaces

Now we are ready to give a formal introduction to overtness, of which we saw an example in Section 2. This very novel concept is invisible in (even intuitionistic) point–set topology, for a reason that we shall see at the end of this section, so we have to rely entirely on our new calculus.

As our guide, we exploit the lattice duality with the notion of compactness and follow the plan of Sections 8 and 9 as closely as possible. Before going on, you should therefore be sure that you thoroughly understand how the formalism there relates to your own knowledge of compact subspaces, and then refer back to those sections while you read this one.

Under the lattice duality, the theory of open or overt subspaces of (overt) discrete spaces corresponds to that of closed or compact subspaces of (compact) Hausdorff spaces (Theorem 11.20). However, the ambient space that primarily interests us in this paper is Hausdorff, not discrete. More fundamentally, we know that the open and closed phenomena in general topology do not quite match, for example ℕ is overt but not compact, whilst Scott continuity (Axiom 9.1) is about directed joins and not meets.

Since things are not exactly dual we must start from a different place. Motivated by our interest in stable zeroes (Proposition 2.12), we choose the dual of Definition 8.19 for a compact open subspace.

Definition 11.1 A closed overt subspace of a space X is defined by a pair of terms (♢, ω), in which ω : Σ^{X} is its co-classifier qua closed subspace and ♢ : Σ^{Σ^{X}} is its possibility modal operator qua overt one. For ♢ to have this type means that ♢ ϕ is a proposition (a term of type Σ). The terms ♢ and ω must be related by the rule that, for any expression ϕ : Σ^{X},

♢ ϕ ⇔ ⊥ ⊣⊢ ϕ ⩽ ω,

cf. Proposition 2.15. Equivalently (by Axiom 5.6),

ϕx ⟹ ωx ∨ ♢ ϕ  and  ♢ ω ⇔ ⊥,

the first part of which we call relative instantiation, cf. Axiom 5.10. If we want to name the subspace, we write ⟨S⟩ for ♢. The intended meaning of ♢ ϕ is that ϕ touches the subspace represented by ♢, cf. Proposition 2.2, whereas in Section 8, ϕ covered □.

Proposition 11.2 For a : H, σ : Σ, ϕ, ψ : Σ^{H} and θ : Σ^{H_{1}×H_{2}}, ♢ operators obey

(a) uniqueness: if ♢ and ♢′ both satisfy the definition for the same ω then ♢ = ♢′, and similarly if ω and ω′ satisfy it for the same ♢ then ω = ω′;

(b) preservation of joins: ♢ ⊥ ⇔ ⊥ and ♢(ϕ ∨ ψ) ⇔ ♢ ϕ ∨ ♢ ψ;

(c) the Frobenius law: σ ∧ ♢ ϕ ⇔ ♢(λx. σ ∧ ϕx);

(d) substitution inside any expression to which ♢ is applied; and

(e) commutativity: ⟨S_{1}⟩(λx. ⟨S_{2}⟩(λy. θxy)) ⇔ ⟨S_{2}⟩(λy. ⟨S_{1}⟩(λx. θxy)). Proof It would be a valuable exercise to transcribe the proof of Proposition 8.2 and Exercise 8.20, replacing each symbol with its lattice dual. Uniqueness comes from ϕ ⩽ ω′ ⊣⊢ ♢ ϕ ⇔ ⊥ ⊣⊢ ϕ ⩽ ω ⊣⊢ ♢′ ϕ ⇔ ⊥ and Axiom 5.6. The Frobenius law follows from Proposition 5.8 and the substitution property is that for λ-application (Axiom 7.7). Finally, either side of the commutative law is ⊥ iff

x, y : H, ω_{1}x ⇔ ω_{2}y ⇔ ⊥ ⊢ ϕxy ⇔ ⊥.  □

Remark 11.3 Since ♢ automatically preserves directed joins (it is Scott-continuous, Axiom 9.1), it actually preserves all joins, as in Theorem 2.5. That’s not quite right: it preserves joins indexed by other overt objects, and the same is true of inverse image maps (f^{−1}, Definition 7.19). Another way of putting this is that possibility operators commute, which is what we have just said. Unlike in the lattice-theoretic or localic language, we are able to make identical statements about meets and joins.

We resist the temptation to define ♢ simply as an operator that preserves joins because it is not yet clear whether this will still be appropriate in the generalisation envisaged in Remark 7.13.

Example 11.4 As in Proposition 2.15(d) and Example 8.5, any point defines an overt subspace {a}, with ♢ ϕ ≡ ϕa and (in a Hausdorff space) ωx ≡ (x ≠ a). Relative instantiation for this is Lemma 5.9.

Conversely, any term P : Σ^{Σ^{H}} that obeys the rules for both modal operators (it is enough that it preserve ⊤, ⊥, ∧ and ∨) is called prime, and arises as P ≡ λϕ. ϕa from a unique point a [G, §10]. □

Definition 11.5 We say that a : X is a member of the overt subspace, a ∈ ♢, if, for any ϕ : Σ^{X},

ϕa ⟹ ♢ ϕ, or λϕ. ϕa ⩽ ♢ : Σ^{Σ^{X}} .

An overt subspace is said to be inhabited if ♢ ⊤ ⇔ ⊤ (cf. Proposition 2.15(c)). The existence property (Remark 6.6) provides an actual member of any inhabited overt subspace of ℕ or ℚ (without parameters) and future work will show the same for ℝ.

This notion of membership is another example to which we may apply Notation 7.15 to define a subspace, S ≡ {x : X | λϕ. ϕx ⩽ ♢}, cf. Proposition 2.12. Although we have not given any condition on ♢ alone that says when it defines an overt subspace, the two directions of Definition 11.1 now state the containments S ⊃ Z and S ⊂ Z respectively, in the sense of Definition 7.17.

We sometimes refer to the two-way relationship as the non-singular case. In Section 2 we saw that the singular case arises, for example, from double zeroes of polynomials, where relative instantiation fails but we still have ♢ ω ⇔ ⊥.

Proposition 11.6 In the non-singular case, the two notions of membership for a closed overt subspace agree. In the singular case, the overt subspace lies inside the closed one. Proof S ⊂ Z comes from ♢ ω ⇔ ⊥ because, if x ∈ ♢ then (putting ϕ ≡ ω in the definition) ωx ⇒ ♢ ω ⇔ ⊥, so ωx ⇔ ⊥. Conversely, Z ⊂ S is relative instantiation, ϕx ⇒ ωx ∨ ♢ ϕ, when ωx ⇔ ⊥. □

Proposition 11.7 If d ≤ u : ℝ then the interval [d, u] ⊂ ℝ is closed overt, with

ωx ≡ (x < d) ∨ (u < x) and ♢ ϕ ≡ ϕd ∨ (∃x:ℝ. d < x < u ∧ ϕx) ∨ ϕu.

If d < u then ♢ ϕ is just ∃x:ℝ. d < x < u ∧ ϕx.

The interval [d, +∞) is also closed overt, with

ωx ≡ (x < d) and ♢ ϕ ≡ ∃x:ℝ. (d < x) ∧ ϕx,

and we may define (−∞, u] in a similar way. Proof By Proposition 9.6, ω co-classifies the closed interval and then ♢ ω expands to (u < d) ⇔ ⊥. By Lemma 5.9,

ϕx ⟹ (x < d) ∨ ϕd ∨ (d < x).

The conjunction of this with the similar formula with u gives relative instantiation,

ϕx ⟹ (x < d ∨ u < x) ∨ (ϕd ∨ (∃y. d < y < u ∧ ϕy) ∨ ϕu) ≡ ωx ∨ ♢ ϕ.  □

Examples 11.8 The empty subspace is overt, as is the union of any two closed overt subspaces, but the intersection may fail to be overt, even in the simplest cases, {a} ∩ {b} and [d, u] ∩ [e, t].

\begin{matrix}S & ωx & ⟨S⟩ϕ \\ ∅ & ⊤ & ⊥ \\ S_{1} ∪ S_{2} & ω_{1}x ∧ ω_{2}x & ⟨S_{1}⟩ϕ ∨ ⟨S_{2}⟩ϕ \\ S_{1} ∩ S_{2} & ω_{1}x ∨ ω_{2}x & Example 16.4 \end{matrix}  □

We shall come back to subspaces shortly, but first let’s look at overt spaces.

Definition 11.9 A space S is overt if it has an existential quantifier, ∃_{S}, such that, for x : S and ϕ : Σ^{S},

∃_{S}⊥ ⇔ ⊥  and  ϕx ⟹ ∃_{S}ϕ,

the latter being called the absolute instantiation rule. In other words, S is a closed overt subspace of itself with ω ≡ ⊥, and any expression of type S is a member of ♢ in the sense of Definition 11.5.

Examples 11.10 The spaces ℕ, ℚ and ℝ are overt (Remark 5.11).

We write ∃x:S. ϕx for ∃_{S}ϕ when S is an overt space, so ∃x:S. ϕx means ⟨S⟩(λx. ϕx). We sometimes also use ∃ for overt subspaces, i.e. for ⟨S⟩ϕ.

Proposition 11.11 Any closed overt subspace is an overt space. Proof As in Theorem 8.16, given (♢, ω), let C ≡ {x : X | ωx ⇔ ⊥} with Σ-splitting I : Σ^{C} ↣ Σ^{X} (Axiom 7.10) and ∃_{C}ψ ≡ ♢(Iψ), so ∃_{C}⊥_{C} ≡ ♢(I⊥_{C}) ⇔ ♢ ω ⇔ ⊥. Then, since ω ⩽ ψ = Iψ, we have, for x : C and ψ : Σ^{C},

ψx ⟹ ωx ∨ ♢ ψ ⟺ ∃_{C}ψ.  □

The quantifier is justified by Proposition 11.2 and the following rules of inference.

Theorem 11.12 In an overt space, ∃_{S} satisfies the two-way rule on the left,

…, x : S ⊢ ϕx ⇒ σ ; = ; … ⊢ ∃x:S. ϕx ⇒ σ  …, x : X, ωx ⇔ ⊥ ⊢ ϕx ⇒ σ ; = ; … ⊢ ♢ ϕ ⇒ σ

where σ : Σ must not involve the variable x. Similarly, ♢ and ω for a closed overt subspace of X satisfy the rule on the right.

As in Remark 8.17, ♢ is a bounded existential quantifier, with which we can reason about members of the subspace as if this were itself a space, cf. Exercise 2.10. Proof By Axiom 5.6, the rule on the right is

…, x : X, σ ⇔ ⊥ ⊢ ϕx ⟹ ωx ; = ; …, σ ⇔ ⊥ ⊢ ♢ ϕ ⟹ ⊥  or  …, σ ⇔ ⊥ ⊢ ϕ ⩽ ω : Σ^{X} ; = ; …, σ ⇔ ⊥ ⊢ ♢ ϕ ⟹ ⊥

which is Definition 11.1. The rule on the left is the special case where ωx ≡ ⊥. □

The exact analogue of Theorem 8.9 for the direct image of f : X → Y when X is overt would require Y to be discrete, whereas we are interested in Hausdorff spaces. Nevertheless, the situation has an extremely important example that explains why Proposition 2.12 gave the closure of the overt subspace ♢.

Notation 11.13 Let ⟨S⟩ be an overt subspace of X, and f : X → Y. Then

⟨fS⟩ψ ≡ ⟨S⟩(f^{∗}ψ) ≡ ⟨S⟩(λx. ψ(fx))

is called the direct image of ⟨S⟩. If a : X is a member of ⟨S⟩ then fa : Y is a member of ⟨fS⟩, whilst ⟨fS⟩ preserves joins. If S is inhabited then so too is fS because

⟨fS⟩⊤ ⟺ ⟨S⟩(⊤ · f) ⟺ ⟨S⟩⊤ ⟺ ⊤.

This doesn’t satisfy the whole of Definition 11.1, because we haven’t defined ω for fS, but this deficit will be rectified in Proposition 12.12 when we have compactness too. In a sense, ⟨fS⟩ is the closure of the image, because it is contained in any closed subspace whose inverse image contains ⟨S⟩, since ⟨fS⟩ω ⇔ ⊥ iff ⟨S⟩(f^{∗}ω) ⇔ ⊥.

Example 11.14 The modal operator for the direct image of any map f : ℕ → X is

♢ ϕ ≡ ∃n:ℕ. ϕ(fn).

Let a : X be a member of ♢ (Definition 11.5). For any neighbourhood ϕ : Σ^{X} of a,

ϕa ⟹ ♢ ϕ ≡ ∃n. ϕ(fn),

so, since ϕ was arbitrary, a is an accumulation point of the sequence in the traditional sense, cf. Example 2.11(b). Maybe we should have used this name instead of “member” in Definition 11.5. This phenomenon is the dual of Warning 8.4.

Note that, in our usage, the members of a sequence (as well as its limit, if any) are accumulation points of it. However, we are not saying that the sequence has a limit.

Notice that we have only used the topological properties of ℕ, not its arithmetic, recursion or cardinality. Hence the idea generalises to accumulation points of nets of whatever size and shape, so long as they are definable in the underlying calculus.

Remark 11.15 Conversely, every operator ⊢ ♢ : Σ^{Σ^{ℝ}} that is definable in the ASD calculus and preserves joins (♢ ⊥ ⇔ ⊥ and ♢(ϕ ∨ ψ) ⇔ ♢ ϕ ∨ ♢ ψ) is of the form ♢ ϕ ⇔ ∃n:U . ϕ(fn) for some function f : U → ℝ with U ⊂ ℕ open (recursively enumerable). This will be proved in future work, essentially by applying dependent choice to Remark 6.11. Overtness therefore links computability with the Bolzano–Weierstrass theorem about accumulation points of infinite sets of points.

Returning to subspaces, there are, of course, good reasons why we only find closed compact subspaces of ℝ and not open ones. Despite this and the observation about accumulation points, there are also lots of open overt subspaces, because we have the dual of Proposition 8.7 that any closed subspace of a compact space is compact:

Proposition 11.16 Any open subspace of an overt space is overt. Proof Let α : Σ^{X}, where X has ∃_{X}. Then

♢ ϕ ≡ ∃x:X. ϕx ∧ αx  satisfies  ♢ ϕ ⇔ ⊥ ⊣⊢ ϕ ∧ α = ⊥

and Proposition 11.2, defining an open overt subspace. If a ∈ α (αa ⇔ ⊤) then a ∈ ♢ (λϕ. ϕa ⩽ ♢), but in view of the observation about accumulation points, the converse need not hold. Once again, we leave it as an exercise to adapt Propositions 11.2 and 11.11 to open overt subspaces. □

Example 11.17 For any d, u : ℝ, the open interval (d, u) ⊂ ℝ is classified by λx. d < x < u. More generally, for any ascending real δ and descending one υ, the interval (υ, δ) ⊂ ℝ is classified by δ ∧ υ. These are both overt, where ♢ ϕ is

⟨d, u⟩ϕ ≡ ∃x. (d < x < u) ∧ ϕx  or  ⟨υ, δ⟩ϕ ≡ ∃x. δx ∧ ϕx ∧ υx,

and are inhabited iff d < u or ∃x. δx ∧ υx.

Notice that, if d < u, the formula for ♢ is the same as that for the closed interval [d, u] in Proposition 11.7; this is due to the results above concerning accumulation points. □

This is the setting for the dual of Proposition 9.13. The ascending real δ is the union of the families of lower bounds of the elements of K. We may form this union because it is indexed by an overt set. Since, for ascending reals, the intrinsic and arithmetical orders agree (Remark 3.10), we have the supremum of K as an ascending real, cf. Remark 3.6(b).

Proposition 11.18 For any overt subspace ♢ of ℝ,

δd ≡ ♢(λx. d < x)  and  υu ≡ ♢(λx. x < u)

provide the supremum δ as an ascending real and the infimum υ a descending one. Since

∃d. δd ⟺ ∃u. υu ⟺ ♢ ⊤,

δ and υ are bounded iff ♢ is inhabited. If ♢ is open, classified by α, then α ⩽ δ ∧ υ. Proof By transitivity of < and the Frobenius law for ♢, δ is lower, whilst it is rounded by interpolation and Frobenius, or by Theorem 10.2. Then

∃u. υu ≡ ∃u. ♢(λx. x < u) ⟺ ♢(λx. ∃u. x < u) ⟺ ♢ ⊤

by commutation of ∃ and ♢ (Proposition 11.2(f)) and extrapolation of < (Lemma 5.13). If ♢ is defined from α then α ⩽ δ ∧ υ because, by Theorem 10.2,

αy ⟹ ∃xz. αx ∧ (x < y < z) ∧ αz ⟹ δy ∧ υy.  □

Exercise 11.19 Develop the notion of overt locally closed subspace (Axiom 7.10), using

♢ ϕ ⇔ ⊥ ⊣⊢ ϕ ∧ α ⩽ ω.

Show that the half-open, half-closed intervals [e, t), (e, t], [e, δ) and (υ, t] are overt, where

⟨[e, δ)⟩ϕ ≡ ∃x. (e < x) ∧ ϕx ∧ δx ≡ ⟨e, δ⟩ϕ.  □

We have given an account of overt (sub)spaces in the Hausdorff setting because of our focus on real analysis, but this is a seriously one-sided view, because overt discrete spaces play the important role of sets. Since developing this in detail would double the length of this paper, we just mention a couple of points of a topological nature.

Relying, as always, on the duality, we know that the familiar correspondence between closed and compact subspaces takes its strongest form in a compact Hausdorff space (Theorem 8.15). Similarly, we have

Theorem 11.20 The open and overt spaces of an overt discrete space X are in bijection, by

αx ≡ ♢(λy. x = y) and ♢ ϕ ≡ ∃_{X}(ϕ ∧ α) ≡ ∃x:X. ϕx ∧ αx.  □

Corollary 11.21 The following formulations of recursively enumerable subsets of ℕ agree:

(a) an open subset is defined by a program α that terminates on input n if n belongs to the subset of ℕ in question;

(b) an enumeration is the direct image of a (maybe partial) function ℕ → ℕ as in Notation 11.13 (we actually have the dual of Theorem 8.9); and

(c) an overt subset is defined by a program ♢ for which ♢ ϕ terminates on a user-supplied test ϕ if the open subspace classified by ϕ and the overt one encoded by ♢ have some number in common. □

Remark 11.22 This also explains why overtness is invisible in topology based on points. If a space X has a “set” |X| of points then |X| ↠ X is a surjective continuous function from an overt discrete space, so X itself is overt by Notation 11.13.

12 Compact overt subspaces

The combination of overtness and compactness is extremely powerful in constructive topology, as we shall see in the remainder of the paper. These concepts are defined by modal operators □ and ♢ that are expressions of type Σ^{Σ^{ℝ}} satisfying the mixed modal laws in Proposition 2.16. Since □ and ♢ may involve parameters, the maximum of the subspace that they define will also be an expression in the same parameters.

We begin by showing that the mixed modal laws characterise the situation in which a closed subspace of a Hausdorff space is both overt and compact.

Proposition 12.1 Let (□, ω) define a compact subspace of a Hausdorff space H, and let ♢ be another operator on H such that ♢ ω ⇔ ⊥ and ♢(ϕ ∨ ψ) ⇔ ♢ ϕ ∨ ♢ ψ. Then □ and ♢ always satisfy

□ ϕ ∧ ♢ ψ ⟹ ♢(ϕ ∧ ψ)

and the three subspaces have ♢ ⊂ ω = □ in the sense that (cf. Definition 7.17)

λϕ. ϕa ⩽ ♢ ⊢ ωa ⇔ ⊥ ⊣⊢ □ ⩽ λϕ. ϕa.

The operators also obey the other mixed law

□(ϕ ∨ ψ) ⟹ □ ϕ ∨ ♢ ψ

iff (♢, ω) define a closed overt subspace, i.e. they satisfy relative instantiation,

ϕx ⟹ ωx ∨ ♢ ϕ,

and in this case all three subspaces coincide.

Proof If □ ϕ ⇔ ⊤ then ⊤ ⩽ ϕ ∨ ω, so ψ ⩽ (ϕ ∨ ω) ∧ ψ ⩽ (ϕ ∧ ψ) ∨ ω. Hence

□ ϕ ⇔ ⊤ ⊢ ♢ ψ ⟹ ♢ ((ϕ ∧ ψ) ∨ ω) ⟹ ♢(ϕ ∧ ψ) ∨ ♢ ω ⟹ ♢(ϕ ∧ ψ),

giving the first modal law by Axiom 5.6. Assuming the other,

ϕx ∧ □ ⊤ ⟹ □(λy. ϕx) ⟹ □(λy. x ≠ y ∨ ϕy) ⟹ □(λy. x ≠ y) ∨ ♢ ϕ ≡ ωx ∨ ♢ ϕ

by Proposition 5.8 and Lemma 5.9. Conversely, by Definitions 8.1 and 11.1,

□(ϕ ∨ ψ) ⇔ ⊤, ♢ ψ ⇔ ⊥ ⊢ ϕ ∨ ψ ∨ ω = ⊤ & ψ ⩽ ω
⊢ ϕ ∨ ω = ⊤ ⊢ ⊤ ⇒ □ ϕ

and again Axiom 5.6 gives the modal law. The closed and compact subspaces are equal by Proposition 8.7, and they contain or agree with the overt one by Proposition 11.6. □

Corollary 12.2 Let ♢ and □ be any terms of type Σ^{Σ^{H}} for a Hausdorff space H, and put ωx ≡ □(λy. x ≠ y). Then (□, ω) and (♢, ω) satisfy Definitions 8.1 and 11.1 iff

□ ⊤ ⇔ ⊤  ♢ ω ⇔ ⊥  and  □(ϕ ∨ ψ) ⟹ □ ϕ ∨ ♢ ψ,

the last being equivalent to relative instantiation, ϕx ⇒ ωx ∨ ♢ ϕ. Proof [⊢] The definitions and Propositions 8.2 and 11.2 give the first two equations and relative instantiation.

[⊣] The backward directions of the two definitions are ♢ ω ⇔ ⊥ and

⊤ = ϕ ∨ ω ⊢ ⊤ ⟹ □(ϕ ∨ ω) ⟹ □ ϕ ∨ ♢ ω ⟹ □ ϕ.

Forwards, we are given relative instantiation for ♢, whilst for □ we have

ωx ∨ ϕx ≡ □(λy. x ≠ y) ∨ (ϕx ∧ □ ⊤)
⇔ □(λy. x ≠ y ∨ ϕx)  Proposition 5.8
⇔ □(λy. x ≠ y ∨ ϕy) ⟸ □ ϕ.  Lemma 5.9 □

Applying the mixed modal laws in even the simplest case already has a dramatic result:

Theorem 12.3 Let K be a compact overt subspace. Then it is decidable (Lemma 6.4) whether K is empty. If it’s not, then it is both occupied and inhabited (so these words mean the same thing in this case) and □ ⩽ ♢. Proof If K is empty then □ ⊥ ⇔ ⊤ and ♢ ⊤ ⇔ ⊥, whereas if it’s occupied then □ ⊥ ⇔ ⊥ and if it’s inhabited then ♢ ⊤ ⇔ ⊤. These situations are complementary because

⊤ ⇔ □(⊥ ∨ ⊤) ⟹ □ ⊥ ∨ ♢ ⊤  and  ⊥ ⇔ ♢(⊥ ∧ ⊤) ⟸ □ ⊥ ∧ ♢ ⊤.

Also □ ϕ ⇔ □(⊥ ∨ ϕ) ⟹ □ ⊥ ∨ ♢ ϕ ⇔ ♢ ϕ,

or □ ϕ ⇔ ♢ ⊤ ∨ □ ϕ ⟹ ♢(⊤ ∨ ϕ) ⇔ ♢ ϕ.

Conversely,  □ ⩽ ♢ ⊢ □ ⊥ ⇒ ♢ ⊥ ≡ ⊥ and ⊤ ≡ □ ⊤ ⇒ ♢ ⊤.  □

Remark 12.4 The dichotomy is in the strict logical sense, of which the topological manifestation (cf. Remark 4.6) is that the parameter space Γ is a disjoint union of two clopen subspaces, not just of an open and a closed one. Therefore, if Γ is connected, for example if Γ ≡ ℝ^{n}, something in this short argument has to break at any singularities.

As we saw informally in Proposition 2.15, it is the modal law □(ϕ∨ψ) ⇒ □ ϕ∨♢ ψ that we lose, together with relative instantiation, ϕx ⇒ ωx∨♢ ϕ. Even in this singular case, Proposition 11.6 still ensures that any member or accumulation point of ♢ belongs to the closed subspace co-classified by ω.

Recall from Lemma 6.4 that clopen subspaces correspond to maps H → 2.

Lemma 12.5 Any clopen subspace of a compact overt space X is also compact overt, with

□ θ ≡ ∀x:X. θx ∨ ωx and ♢ θ ≡ ∃x:X. θx ∨ αx,

where α and ω are the given complementary open subspaces. Proof Theorem 8.15 linked □ and ω. Then θ ⩽ ω ⊣⊢ θ ∧ α = ⊤ ⊣⊢ ♢ θ ⇔ ⊤. □

Notation 12.6 Now we are ready to consider the central question about which subsets of ℝ have suprema as Euclidean real numbers. Classically, any non-empty subset K ⊂ ℝ that has an upper bound has a least one. In that setting, there would be no loss of generality in stating this only when K is also closed and bounded below, i.e. compact.

In our calculus, we have already shown that any compact subspace K has a supremum, but in general this is only a descending real number (Proposition 9.13). On the other hand, any overt subspace also has a supremum, but this is an ascending real (Proposition 11.18). These define

δd ≡ ♢(λk. d < k) and υu ≡ □(λk. k < u)

in terms of ♢ and □. If K is empty, these definitions give

max ∅ ≡ −∞ ≡ (λd. ⊥, λu. ⊤) and min ∅ ≡ +∞ ≡ (λd. ⊤, λu. ⊥).

This case is characterised positively, if perversely, by max ∅ < min ∅, but since it is decidable, for the moment we assume that it does not apply.

The duality between overtness and compactness is reflected in a symmetry of the proof that (δ, υ) is a Dedekind cut. This result was inspired by the constructive least upper bound principle (Definition 3.7), but interpreting the quantifiers that it involves in our topological sense:

Proposition 12.7 (Andrej Bauer) If K is non-empty then the pair (δ, υ) is a Dedekind cut. Hence, by Axiom 6.8, there is a unique a : ℝ such that

(d < a) ⟺ δd ≡ ♢(λk. d < k) and (a < u) ⟺ υu ≡ □(λk. k < u).

Proof We know that δ and υ are rounded, so it remains to show that they are disjoint, located and bounded. The proofs are dual, using the mixed modal laws and ♢ σ ⇒ σ ⇒ □ σ. The first also uses transitivity and the second locatedness of the order on ℝ (Axiom 4.9).

(δd ∧ υu) ≡ ♢(λk. d < k) ∧ □(λk. k < u) ⟹ ♢(λk. d < k ∧ k < u) ⟹ (d < u)
(δd ∨ υu) ≡ ♢(λk. d < k) ∨ □(λk. k < u) ⟸ □(λk. d < k ∨ k < u) ⟸ (d < u).

Propositions 9.13 and 11.18 showed respectively that ∃d. δd and ∃u. υu ⇔ ♢ ⊤ ⇔ ⊤. □

Hence K has a supremum a, but it’s better than this:

Lemma 12.8 There is a greatest element, a ∈ K. Proof By Axiom 4.9 and one of the mixed modal laws,

ωa ≡ □(λk. a ≠ k) ⇔ □(λk. a < k ∨ k < a)
⇒ ♢(λk. a < k) ∨ □(λk. k < a)
≡ δa ∨ υa ⇔ (a < a) ∨ (a < a) ⇔ ⊥.

Hence a belongs to the closed subspace, and □ ϕ ⟹ ϕa ⟹ ♢ ϕ by the relative instantiation laws for □ and ♢. □

Theorem 12.9 Any overt compact subspace K ⊂ ℝ is either empty or has a greatest member, max K ≡ a ∈ K. This satisfies, for x : ℝ,

(x < max K) ⇔ (∃k:K. x < k)
(max K < x) ⇔ (∀k:K. k < x)
k : K ⊢ k ≤ max K

and {…, k : K ⊢ k ≤ x \atop … ⊢ max K ≤ x}

Proof The first two properties re-state Proposition 12.7, which also gives, for k : K,

(max K < k) ≡ □(λk′. k′ < k) ⟹ (k < k) ⇔ ⊥,

so k ≤ max K by Example 4.6. The rule on the right is obtained by substitution of max K for k : K. □

Exercise 12.10 Let a, b : ℝ ⇉ ℝ be two functions, so there is no question of using a case analysis on whether a ≤ b or a ≥ b. Regarding them as terms a, b : ℝ with a real parameter, define the parametric modal operators [K] and ⟨K⟩ that make the (ℝ-indexed) subspace K ≡ {a, b} ⊂ ℝ compact and overt. Show that

max(a, b) ≡ max K ≡ (δ, υ) ⇔ (δ_{a} ∨ δ_{b}, υ_{a} ∧ υ_{b}).

The properties listed in Theorem 12.9 are those for binary max in [I, Prop. 9.8]. □

Corollary 12.11 Any overt compact subspace K ⊂ ℝ either

(a) is observably empty, in which case [K]⊥ ⇔ ⊤, or

(b) has a definable member, namely max K, and in this case ⟨K⟩⊤ ⇔ ⊤. We therefore obtain a particular element of K ⊂ ℝ without using dependent choice. □

What can we say about where a function attains its bounds?

Proposition 12.12 Let f : X → Y be a function between Hausdorff spaces, and K ⊂ X a compact overt subspace. Then its image fK ⊂ Y is also compact overt. Proof We prove the modal laws in Corollary 12.2 for fK ⊂ Y.

[fK]⊤_{Y} ≡ [K]⊤_{X} ⇔ ⊤
⟨fK⟩ω_{fK} ≡ ⟨fK⟩(λy_{1}. [fK](λy_{2}. y_{1} ≠ y_{2}))  def ω_{fK}
≡ ⟨K⟩(λx_{1}. [fK](λy_{2}. fx_{1} ≠ y_{2}))  Notation 11.13
≡ ⟨K⟩(λx_{1}. [K](λx_{2}. fx_{1} ≠ fx_{2}))  Theorem 8.9
⇒ ⟨K⟩(λx_{1}. [K](λx_{2}. x_{1} ≠ x_{2}))  Lemma 5.9
≡ ⟨K⟩ω_{K} ⇔ ⊥  def ω_{K}

\begin{aligned}[fK](ϕ ∨ ψ) & ≡ & [K](ϕ · f ∨ ψ · f) & ⟹ & [K](ϕ · f) ∨ ⟨K⟩(ψ · f) & ≡ & [fK]ϕ ∨ ⟨fK⟩ψ \\ ⟨fK⟩(ϕ ∧ ψ) & ≡ & ⟨K⟩(ϕ · f ∧ ψ · f) & ⟸ & [K](ϕ · f) ∧ ⟨K⟩(ψ · f) & ≡ & [fK]ϕ ∧ ⟨fK⟩ψ. \end{aligned}  □

Corollary 12.13 Any function f : K → ℝ on a non-empty compact overt space is bounded, and attains its bounds on an occupied compact subspace Z ⊂ K.

However, Z need not be overt (Example 16.15). Proof Since the image fK ⊂ ℝ is an occupied compact overt subspace of ℝ, it has a maximum b ∈ fK. The inverse image Z ≡ {x : K | fx = b} ⊂ K of b is compact and occupied, by Theorem 8.9. □

Remark 12.14 We shall see in Section 14 that, given a polynomial equation (such as x^{3} − x = 0) with distinct roots ({−1, 0, +1}), the argument above does indeed yield the greatest root (+1).

In the singular case, □ and ♢ only satisfy one of the mixed modal laws, namely the one that was used to prove disjointness of the Dedekind cut in Lemma 12.7, whilst the other law and locatedness fail. The pseudo-cut (δ, υ) nevertheless defines a compact interval [δ, υ] in the sense of Proposition 9.11, whose endpoints are the ascending real δ and the descending one υ.

For example, the polynomial equation x^{3} + x^{2} = 0 has a stable zero at −1 and a double (unstable) one at 0, so {−1} ≡ S ⊂ Z ≡ {−1, 0}. Then δ = sup S = −1 and υ = sup Z = 0, so the interval-valued supremum of the zero set is [−1, 0].

Remark 12.15 Other systems of constructive analysis prove similar results using an idea from the classical theory of metric spaces. A subset K is called totally bounded if, for each ε > 0, there is a finite subset S_{ε} ⊂ K such that ∀x:K. ∃y ∈ S_{ε}. |x − y| < ε. (See [SS70, Example 134.3] for a classical metric on ℝ with a bounded subspace that is not totally bounded.)

If K ⊂ ℝ is closed and totally bounded, either the sets S_{ε} are all empty, in which case K is empty too, or x_{n} ≡ max(S_{2^{−n}}) defines a Cauchy sequence that converges to max K [TvD88, Lemma 6.1.7].

But if we are given explicit finite sets S_{1}, S_{1/2}, S_{1/4}, ..., with the above property in any compact metric space K, we may concatenate them to define a map a_{(−)} : ℕ → K. Then ♢ ψ ≡ ∃n. ψa_{n} (Example 11.14) satisfies ψx ⇒ ♢ ψ by Theorem 10.2, and hence the modal laws, so K is an overt space.

Bas Spitters has investigated how overtness is related to locatedness and other notions in constructive analysis [Spi10].

Remark 12.16 In contrast to the (infinite) subspaces of ℝ that we have just discussed, compact overt discrete spaces are Kuratowski-finite [G, Theorem 9.10]: they can be listed, but it may not be possible to eliminate repetitions from a list because equality need not be decidable [Kur20]. If such a space is also Hausdorff, i.e. its equality is decidable, then it is finite in the usual sense, being listable without repetitions, so we can say how many elements it has.

As in Proposition 12.1, we can use the modal operators to describe compact overt subspaces as pairs of terms. Whereas such a subspace was closed in the Hausdorff case and co-classified by ω, in the discrete case it is open (Definition 8.19) and classified by

αx ≡ ♢(λy. x = y),  with  □ α ⇔ ⊤.

Moreover, there is an overt discrete space KX whose members are pairs (□, ♢) of terms that satisfy the modal laws and therefore represent Kuratowski-finite subsets of X. Hence KX is the finite powerset P_{f}(X) or free semilattice. There is also an object List X that is the free monoid. The general constructions of KX and List X in [E] are rather difficult, but in the cases of X ≡ ℕ or ℚ, there are well known formulae for the bijections KX ≅ ℕ and List X ≅ ℕ.

These results may be used to develop combinatorial arguments such as the definition of the Riemann integral in Remark 10.12 and the results of Section 15, but it is important to appreciate that they rely on topological ideas. A list is not an indeterminate finite collection of points in a space, but a single point of a hyper-space. In order to be able to write it as a_{0}, …, a_{n−1} with a finite number of members (albeit possibly with repetition) and argue by induction, etc., its members have to be drawn from an overt discrete space.

This is why we insist on lists of rational numbers.

The Vietoris space of compact overt subspaces of a Hausdorff space such as ℝ is an entirely different beast, whose modal operators (called t ≡ □ and m ≡ ♢) are described for locales in [Joh82, §III.4].

13 Connectedness

Connectedness is the abstraction of the intermediate value theorem from ℝ to other topological spaces, so the classical proof that the interval is connected is essentially that of Theorem 1.1(a). This is a weak definition because it denies the existence of a strong kind of separation, into clopen parts.

The accounts that we find in constructive analysis use a weaker test, which therefore yields stronger definitions of connectedess, and fewer spaces are connected in the constructive sense. Indeed Example 16.5, which deletes “part of” a point from the line, is not connected constructively, whereas it would appear to satisfy the classical definition. But, as usual, the difference between the classical and constructive results is subtle, so this does not in fact change the status of the traditional examples of unintuitively connected spaces [SS70].

For their constructive definition and proof that 𝕀 is connected, the followers of Brouwer and Bishop make use of the interval-halving argument in Theorems 1.1(b) and 1.7, which Mark Mandelkern [Man83] attributes to Ray Mines and Fred Richman. It leads directly to a useful approximate form of the intermediate value theorem: see [TvD88, Proposition 6.1.4] for the Brouwer school and [BB85, Theorem 2.4.8] for Bishop’s.

Category theory uses yet another formulation, with arbitrary discrete spaces in place of 2. This is again a stronger notion of connectedness, to the extent that Bishop cannot prove that ℝ satisfies it, because this relies on the Heine–Borel theorem. However, as the investigation also requires a combinatorial argument, we postpone it to Section 15, and confine our attention in this section to the binary notions of connectedness.

Remark 13.1 In these definitions, tests of “separation” may be expressed by saying that certain open subspaces cover or are inhabited. These ideas are naturally expressed in terms of the modal operators □ and ♢ that we have developed, and these allow us to say respectively whether compact and overt subspaces are connected.

This gives rise to two versions of even our definition, with two approximate intermediate value theorems. This is another example of the way in which ASD elucidates the open–closed duality in topology. It turns out that the Brouwer–Bishop definition agrees with ours for overt subspaces.

A consequence of this duality in ASD (in which Axiom 5.6 is crucial) is that we may use the classical proof that 𝕀 is connected, which it is in all of the senses that we consider. Unlike Theorem 1.7, our proof does not use dependent choice.

Our dual results for compact spaces do not seem to occur in the constructive literature. There are several possible reasons for this, one of which is that the conclusion of our definition is a disjunction. Other constructive theories are based on intuitionistic set theory, where ∨ carries much a stronger sense than in ASD, cf. the remarks before Lemma 13.16. So our results about compact connectedness would probably have to be wrapped in double negations in Bishop’s or Brouwer’s settings, making them just inferior versions of the ones that they already have.

Another reason is that, according to Bishop’s usage, a “compact” subspace also has to be totally bounded, and therefore overt (Remark 12.15), so he never considers compact intervals [δ, υ] with non-Euclidean endpoints (Definition 9.9). But these are exactly the compact connected subspaces of ℝ in ASD (Theorem 15.11), whilst the proof of this apparently requires the Heine– Borel property, which Bishop does not accept.

Definition 13.2 We call an open or closed subspace C ⊂ H of a Hausdorff space

(a) overt connected if it is given by ♢ : Σ^{Σ^{H}} (Definition 11.1) for which

♢ ⊤ ⇔ ⊤ and …, ϕ, ψ : Σ^{H}, ϕ ∨ ψ = ⊤_{C} ⊢ ♢ ϕ ∧ ♢ ψ ⟹ ♢(ϕ ∧ ψ),

so whenever C ⊂ U ∪ V is covered by inhabited open subspaces, they must intersect;

(b) compact connected if it is given by □ : Σ^{Σ^{H}} (Definition 8.1) for which

□ ⊥ ⇔ ⊥ and …, ϕ, ψ : Σ^{H}, ϕ ∧ ψ = ⊥_{C} ⊢ □ ϕ ∨ □ ψ ⟸ □(ϕ ∨ ψ),

so whenever C ⊂ U ∪ V is covered by disjoint open subspaces then one of them is enough. The modal operators in these expressions are the quantifiers that say that C is overt (Proposition 11.11 or 11.16) or compact (Theorem 8.16 or Exercise 8.20(e)) as a space in itself. We defined these quantifiers (applied to ψ : Σ^{C}) in terms of the map I : Σ^{C} ↣ Σ^{X} given by Axiom 7.10. (C now stands for “connected”, not closed.)

It will now be more convenient to use the modal operators themselves, applied to ϕ, ψ : Σ^{X}, instead of constructing the subspace C. If C is open, classified by α : Σ^{H}, then the equation ϕ = ⊥_{C} means ϕ ∧ α = ⊥ : Σ^{H} and ϕ = ⊤_{C} means ϕ ⩾ α : Σ^{H}. On the other hand, if it is a closed subspace co-classified by ω : Σ^{H} then ϕ = ⊥_{C} means ϕ ⩽ ω : Σ^{H} and ϕ = ⊤_{C} means ϕ ∨ ω = ⊤ : Σ^{H} (Axiom 7.10).

Exercise 13.3 Give the English translation of the symbolic definitions, but in terms of the closed subspaces that ϕ and ψ co-classify. [Hint: they swap places.]

We will show that ℝ is overt connected and that 𝕀 has both properties, but first we see how the two definitions yield the approximate intermediate value theorems.

Proposition 13.4 Any function f : X → ℝ on an overt connected space X that takes values both above −ε and below +ε also takes values within any ε > 0 of zero:

ε > 0 ∧ ∃xz:X. (−ε < fx) ∧ (fz < +ε) ⟹ ∃y:X. (−ε < fy < +ε),

so the open, overt subspace {x : X | |fx| < ε} is inhabited. Proof Let ϕx ≡ (−ε < fx) and ψx ≡ (fx < +ε). Then ♢ ϕ ⇔ ♢ ψ ⇔ ⊤ by hypothesis, and ϕ ∨ ψ = ⊤_{X} by locatedness for ℝ (Axiom 4.9). Then overt connectedness says that

⊤ ⇔ ∃xz. (−ε < fx) ∧ (fz < +ε)
≡ ♢ ϕ ∧ ♢ ψ
⇒ ♢(ϕ ∧ ψ) ≡ ∃y. (−ε < fy < +ε).  □

Compact connectedness gives another approximate intermediate value theorem:

Proposition 13.5 Let f : K → ℝ be a function on a compact connected space such that both of the closed, compact subspaces {x : K | fx ≥ 0} and {x : K | fx ≤ 0} are occupied (Definition 8.6). Then so too is their intersection, Z ≡ {x : K | fx = 0}. Proof Let ϕx ≡ (0 < fx) and ψx ≡ (fx < 0), so ϕ ∧ ψ = ⊥_{K}, whilst by hypothesis □ ϕ ⇔ □ ψ ⇔ ⊥, Then compact connectedness says that

⊥ ⟺ (∀x. 0 < fx) ∨ (∀x. fx < 0) ≡ □ ϕ ∨ □ ψ ⟸ □(ϕ ∨ ψ) ≡ (∀x. fx ≠ 0).  □

These two approximate theorems may be seen as transferring connectedness along a function between two spaces, which we can also say more abstractly:

Proposition 13.6 The direct image under f : X → Y of a compact or overt connected subspace C ⊂ X, in the senses of Theorem 8.9 and Notation 11.13 respectively, is also connected as a subspace of Y. Proof Let ϕ, ψ : Σ^{Y}. If ϕ ∧ ψ = ⊥_{fC} with C compact, so ϕ · f ∧ ψ · f = ⊥_{C}, then

[fC](ϕ ∨ ψ) ≡ [C](ϕ · f ∨ ψ · f) ⟹ [C](ϕ · f) ∨ [C](ψ · f) ≡ [fC]ϕ ∨ [fC]ψ.

Similarly, if ϕ ∨ ψ = ⊤_{fC} with C overt then ϕ · f ∨ ψ · f = ⊤_{C} and

⟨fC⟩(ϕ ∧ ψ) ≡ ⟨C⟩(ϕ · f ∧ ψ · f) ⟸ ⟨C⟩(ϕ · f) ∧ ⟨C⟩(ψ · f) ≡ ⟨fC⟩ϕ ∧ ⟨fC⟩ψ.  □

From here one could go on to develop the idea of path-connectedness. However, we really need to show that our two definitions agree with each other and with the traditional one. This is where the modal operators and their mixed laws come into their own, and once again the Phoa principle makes it all work.

Proposition 13.7 Let C ⊂ H be a non-empty compact overt subspace of a Hausdorff space, so it has (□, ♢) satisfying both mixed modal laws (Proposition 12.1). Then the following are equivalent:

(a) ♢ defines an overt connected subspace;

(b) □(ϕ ∨ ψ) ∧ ♢ ϕ ∧ ♢ ψ ⟹ ♢(ϕ ∧ ψ);

(c) if two disjoint open sets cover C then they are not both inhabited;

(d) □ defines a compact connected subspace;

(e) □(ϕ ∨ ψ) ⟹ □ ϕ ∨ □ ψ ∨ ♢(ϕ ∧ ψ);

(f) if two disjoint open sets cover C then just one of them already covers it;

(g) if K ⊂ C is clopen then either K = ∅ or K = C; and

(h) any function f : C → 2 is constant.

Examples 16.5 and 16.8 are classically connected, but the former is not compact and so cannot satisfy (a), whilst the latter fails (d) and overtness. Proof When we have both modal operators available, we may use Definitions 8.1 and 11.1 to turn equations of type Σ^{C} into propositions. Hence (a) becomes

□(ϕ ∨ ψ) ⇔ ⊤ ⊣⊢ ϕ ∨ ψ = ⊤_{C} ⊢ ♢ ϕ ∧ ♢ ψ ⟹ ♢(ϕ ∧ ψ),

which is equivalent to (b) by Axiom 5.6. Similarly (d) is

♢(ϕ ∧ ψ) ⇔ ⊥ ⊣⊢ ϕ ∧ ψ = ⊥_{C} ⊢ □(ϕ ∨ ψ) ⟹ □ ϕ ∨ □ ψ,

which is equivalent to (e) by Axiom 5.6.

Under the same transformation, condition (c) says

□(ϕ ∨ ψ) ⇔ ⊤, ♢(ϕ ∧ ψ) ⇔ ⊥ ⊢ ♢ ϕ ∧ ♢ ψ ⇔ ⊥,

which, by Axiom 5.6, is equivalent to (b), whilst (f) says

□(ϕ ∨ ψ) ⇔ ⊤, ♢(ϕ ∧ ψ) ⇔ ⊥ ⊢ ⊤ ⇔ □ ϕ ∨ □ ψ,

which is (e).

The traditional formulations (g,h) are equivalent to these by Lemmas 6.4 and 12.5, so it remains to show that (b) and (e) are equivalent.

[b⊢e]: One mixed modal law (with ϕ and ψ in both roles and using distributivity) gives

□(ϕ ∨ ψ) ⟹ (□ ϕ ∨ ♢ ψ) ∧ (□ ψ ∨ ♢ ϕ) ⟹ □ ϕ ∨ □ ψ ∨ (♢ ϕ ∧ ♢ ψ),

which is almost the same as (e), apart from the last disjunct, for which we use (b). [e⊢b]: The lattice-dual argument using other mixed modal law gives

♢(ϕ ∧ ψ) ⟸ (□ ϕ ∧ ♢ ψ) ∨ (□ ψ ∧ ♢ ϕ) ⟸ (□ ϕ ∨ □ ψ) ∧ ♢ ϕ ∧ ♢ ψ,

which only differs from (b) in the first conjunct, for which we use (e). □

Now we concentrate on the space 𝕀 ≡ [d, u] ⊂ ℝ, which is closed, compact and overt by Proposition 11.7. We find that the classical proof (Theorem 1.1(a)) is valid in ASD:

Lemma 13.8 Any non-empty clopen subspace K ⊂ [d, u] contains the endpoint u. Proof By Lemma 12.5, K is overt and compact, so by Theorem 12.9 it has a maximum element, a ∈ K ⊂ 𝕀 ≡ [d, u]. Now, K is in particular the relative open subspace of 𝕀 that is classified by the restriction of some ϕ : Σ^{ℝ} (cf. Axiom 7.10), so ϕa ⇔ ⊤. By Theorem 10.2, a is in the interior of ϕ, now treated as an open subspace of ℝ:

max K ≡ a ∈ (e, t) ⊂ [e, t] ⊂ ϕ ⊂ ℝ.

If u ≠ a then a < u, so, without loss of generality, a < t < u. Since K is also closed, let ψ : Σ^{ℝ} classify its complement. Putting these ideas together,

ϕa ∧ (u ≠ a) ⇒ ∃et. (e < a < t < u) ∧ ∀x:[e, t]. ϕx
⇒ ∃t:𝕀. ϕt ∧ (max K < t)  a ≡ max K, x ≡ t
⇒ ∃t:𝕀. ϕt ∧ ∀x:K. (x < t)  Theorem 12.9
⇒ ∃t:𝕀. ϕt ∧ ∀x:𝕀. ψx ∨ (x < t)  Lemma 12.5
⇒ ∃t:𝕀. ϕt ∧ ψt ⟺ ⊥,  x ≡ t, disjointness

so (u ≠ a) ⇒ ⊥, but this means u = a ∈ K by Definition 4.8. □

Theorem 13.9 The interval 𝕀 is connected in all of the above senses. Proof For Proposition 13.7(g), let 𝕀 = K ∪ K′ be a disjoint union of clopen subspaces. By Theorem 12.3, it is decidable whether K is empty, but if it is not then u ∈ K by the Lemma, and similarly for K′. Then, of the four cases

\begin{matrix}K = ∅ & K′ = ∅ & K = ∅ & u ∈ K′ \\ u ∈ K & K′ = ∅ & u ∈ K & u ∈ K′, \end{matrix}

only the second and third have K and K′ complementary. □

Theorem 13.10 The real line ℝ is overt connected. Proof Let ϕ, ψ : Σ^{ℝ} with ϕ ∨ ψ = ⊤_{ℝ} and (∃x:ℝ. ϕx) ⇔ ⊤ ⇔ (∃z:ℝ. ψz).

Recalling the idioms for ∃ (Axiom 5.10), consider the restrictions of ϕ and ψ to [x, z] or [z, x]. These satisfy the hypotheses for overt connectedness of the closed interval, so (∃y:[x, z]. ϕy∧ψy) ⇔ ⊤, whence (∃y:ℝ. ϕy ∧ ψy) ⇔ ⊤. □

The approximate intermediate value theorems for 𝕀 → ℝ and ℝ → ℝ now follow:

Corollary 13.11 Let f : 𝕀 ≡ [d, u] → ℝ be any (continuous) function satisfying f(d) ≤ 0 ≤ f(u), even one that hovers (Example 1.2). Then the compact subspace Z ⊂ 𝕀 of all zeroes is occupied. □

Next we characterise open intervals in the sense of Example 11.17. The formulations of convexity come from [Man83]; they are a one-dimensional version of path connectedness.

Proposition 13.12 The following are equivalent for the open subspace classified by α : Σ^{ℝ}:

(a) it is an overt connected subspace;

(b) it is inhabited and paraconvex: αx ∧ (x < y < z) ∧ αz ⟹ αy;

(c) it is inhabited and convex: αx ∧ (x < z) ∧ αz ⟹ ∀y:[x, z]. αy; and

(d) α = δ ∧ υ, an inhabited open interval. Proof Any open subspace is overt, with ♢ ϕ ≡ ∃x:ℝ. αx∧ϕx, by Proposition 11.16, and all four conditions give ♢ ⊤ ⇔ ⊤.

[c⊢a]: We adapt the proof of Theorem 13.10, with the open subspace classified by α instead of ℝ. If α ⩽ ϕ ∨ ψ, αx ∧ ϕx and αz ∧ ψz then by convexity the closed interval [x, z] or [z, x] is covered by (α ∧ ϕ) ∨ (α ∧ ψ). Hence overt connectedness of this interval gives ∃y. αy ∧ ϕy ∧ ψy.

[a⊢d] By Proposition 11.18, α ⩽ δ ∧ υ where δd ≡ ♢(λz. d < z) ≡ ∃z. (d < z) ∧ αz and υu ≡ ♢(λx. x < u) ≡ ∃x. αx ∧ (x < u). For equality, let y : ℝ and consider ϕ_{y} ≡ λz. (y < z) and ψ_{y}x ≡ λx. (x < y), so

♢ ϕ_{y} ≡ δy, ♢ ψ_{y} ≡ υy but ♢(ϕ_{y} ∧ ψ_{y}) ⟺ ∃x. (y < x) ∧ (x < y) ⟺ ⊥.

If αy ⇔ ⊥ then αx ⇒ (x ≠ y) ⇒ ϕ_{y}x ∨ ψ_{y}x, so ⊤_{C} ≡ α ⩽ ϕ_{y} ∨ ψ_{y} and we may use overt connectedness. Then

αy ⇔ ⊥ ⊢ δy ∧ υy ≡ ♢ ϕ_{y} ∧ ♢ ψ_{y} ⟹ ♢(ϕ_{y} ∧ ψ_{y}) ≡ ⊥,

so δ ∧ υ ⩽ α by Axiom 5.6.

[d⊢c⊣⊢b]: By Theorem 10.2 and since δ is lower and υ is upper. □

Exercise 13.13 Show that the locally closed intervals such as [e, δ) in Exercise 11.19 are also overt connected.

This notion of open interval (with descending and ascending endpoints instead of Euclidean ones) is the one that we require in order to complete the classification of open subspaces of ℝ that we began in Remark 10.13.

Lemma 13.14 For any ϕ : Σ^{ℝ},

(x ≈_{ϕ} y) ≡ ([x, y] ⊂ ϕ) ∧ ([y, x] ⊂ ϕ)
≡ (x > y ∨ ∀z:[x, y]. ϕz) ∧ (x < y ∨ ∀z:[y, x]. ϕz),

is an open partial equivalence relation on ℝ that is reflexive exactly on the open subspace classified by ϕ:

ϕx ⟺ (x ≈ x),  x ≈_{ϕ} y ⟹ y ≈_{ϕ} x and x ≈_{ϕ} y ≈_{ϕ} z ⟹ x ≈_{ϕ} z.  □

This idea was used in Theorem 2.5; we explicitly make it symmetric because the formulae in [I, § 10] for the bounded quantifier ∀z:[x, y]. ϕz depended on x ≤ y.

Theorem 13.15 Every open subspace of ℝ is the union of disjoint open intervals. Proof As with any equivalence relation, the classes are “disjoint” in the sense that if any two overlap, they actually coincide. Each of these classes is convex open and therefore an interval in our sense. Finally, (x ≈_{ϕ} x) ⇒ ϕx from the definition. We return to this decomposition in Proposition 15.7. □

Turning to compact connectedness, the analogue of Proposition 13.12(a⊢d) appears to solve a problem that we might at first think is impossible. Imagine arriving from a hike at an isolated bus stop to find the timetable obliterated. The one daily bus is not there now (ωx), but how can we decide whether we should wait for it (δx) or if it has already gone (υx)? In fact, this just illustrates that the meaning of ∨ is weaker in ASD than in other constructive logics: our argument strengthens the observation about the present to a time-variable one, saying that either the bus hasn’t come yet or it will never come again, but it doesn’t say which of these is the case.

Lemma 13.16 Any compact connected subspace K ≡ (□, ω) ⊂ ℝ is an occupied compact interval [δ, υ] (Definition 9.9). Proof By Proposition 9.13, δ ∨ υ ⩽ ω, where

δd ≡ □(λz. d < z)  and  υu ≡ □(λx. x < u)

are rounded and bounded. They are disjoint by Corollary 9.12 because K is occupied.

To show that δ ∨ υ ⩾ ω, let y : ℝ and consider ϕ_{y} ≡ λx. (y < x) and ψ_{y}x ≡ λx. (x < y), so ϕ_{y} ∧ ψ_{y} = ⊥. Then by compact connectedness,

δy ∨ υy ≡ □ ϕ_{y} ∨ □ ψ_{y} ⟸ □(ϕ_{y} ∨ ψ_{y}) ≡ □(λx. y < x ∨ x < y) ≡ ωy.  □

Corollary 13.17 Any compact overt connected subspace K ⊂ ℝ is an interval [d, u] with Euclidean endpoints, where d ≡ inf K ≤ u ≡ sup K by Theorem 12.9. □

It seems that we cannot prove that every compact interval [δ, υ] is connected either as the dual of Proposition 13.12(c⊢a) or by using Scott continuity applied to Theorem 13.9. We have to apply a combinatorial argument to the four-fold cover by δ ∨ ϕ ∨ ψ ∨ υ (Theorem 15.11).

There are two other situations about which the definitions that we have given are unable to say anything. First, there ought to be a general notion of overt subspace instead of the open, closed and locally closed special cases. Second, we would also like to say that the closed subspaces [δ, +∞) and (−∞, υ] that are co-classified by an ascending or descending real number are connected, even though they are not compact and need not be overt.

14 The intermediate value theorem

We can now prove the intermediate value theorem within ASD, in the two forms (non-singular and singular) that we discussed in Section 2. In the non-singular case on a closed bounded interval, the approximate forms of the theorem in the previous section are enough to ensure that the solutionset S_{f} = Z_{f} is compact, overt and non-empty, and therefore has a maximum element. We begin by formulating the relevant definitions from Sections 1 and 2 in ASD.

Definition 14.1 A function …, x : ℝ ⊢ fx : ℝ (Definition 5.3)

(a) doesn’t hover (cf. Definition 1.4) if, for d, u : ℝ,

d < u ⟹ ∃x. (d < x < u) ∧ (fx ≠ 0);

(b) doesn’t touch from below without crossing if

(d < u) ∧ (fd < 0) ∧ (fu < 0) ⟹ (∀x:[d, u]. fx < 0) ∨ (∃x:[d, u]. fx > 0);

(c) and doesn’t touch from above without crossing if

(d < u) ∧ (fd > 0) ∧ (fu > 0) ⟹ (∀x:[d, u]. fx > 0) ∨ (∃x:[d, u]. fx < 0).

(d) A real number a : ℝ is a stable zero of f (cf. Definition 1.8) if

(d < a < u) ⟹ ∃et. (d < e < t < u) ∧ (fe < 0 < ft ∨ fe > 0 > ft);

(e) and the possibility modal operator ♢ : Σ^{Σ^{ℝ}} is, for ϕ : Σ^{ℝ},

♢ ϕ ≡ ∃d < u. (∀x:[d, u]. ϕx) ∧ (fd < 0 < fu ∨ fd > 0 > fu),

so fd < 0 < fu ⟹ ♢ ⊤.

(f) The solution co-classifier (or non-solution classifier) is ωx ≡ (fx ≠ 0), which defines an open subspace W_{f} and a closed one Z_{f}; and,

(g) restricting to an interval 𝕀 ≡ [d, u], the necessity modal operator □ : Σ^{Σ^{𝕀}} is

□ ϕ ≡ ∀x:𝕀. (fx ≠ 0) ∨ ϕx,

which makes Z_{f} a compact subspace.

Proposition 14.2 The stable zeroes are exactly the members or accumulation points of ♢ in the sense of Definition 11.5. Proof If a is a stable zero then, by Theorem 10.2,

ϕa ⇒ ∃du. (d < a < u) ∧ ∀x:[d, u]. ϕx
⇒ ∃detu. (d < e < t < u) ∧ (fe < 0 < ft ∨ fe > 0 > ft) ∧ ∀x:[e, t]. ϕx
⇒ ♢ ϕ.

Conversely, suppose that ϕa ⇒ ♢ ϕ and let d < a < u. With ϕx ≡ (d < x < u),

⊤ ⇔ ϕa ⇒ ♢ ϕ ⇒ ∃et. (d < e < t < u) ∧ (fe < 0 < ft ∨ fe > 0 > ft).  □

Recall from Definition 11.1 that ♢ and ω define a closed overt subspace iff they satisfy ♢ ω ⇔ ⊥ and relative instantiation, ϕx ⇒ ωx ∨ ♢ ϕ. The first of these comes for free:

Lemma 14.3 ♢ ω ⇔ ⊥.

Proof With ϕx ≡ (fx > 0) and ψx ≡ (fx < 0),

♢ ω ≡ ∃d < u. (∀x:[d, u]. fx ≠ 0) ∧ (fd < 0 < fu ∨ fu < 0 < fd)
⇒ ∃d < u. (∀x:[d, u]. ϕx ∨ ψx) ∧ (∃y:[d, u]. ϕy) ∧ (∃z:[d, u]. ψz)
⇒ ∃d < u. ∃w:[d, u]. ϕw ∧ ψw
⇒ ∃w:ℝ. 0 < fw < 0 ⇔ ⊥

by connectedness of [d, u] in the form of Proposition 13.7(b). □

Hence if a ∈ ♢ then a ∈ {x | ¬ωx}, or S_{f} ⊂ Z_{f} in the notation of Section 2. In order to characterise the non-singular case, S_{f} = Z_{f}, we therefore show that relative instantiation is equivalent to the conditions in Definition 14.1.

Lemma 14.4 If f doesn’t hover or touch without crossing then ♢ and ω satisfy relative instantiation. Proof If ϕx then ∃du. (d < x < u) ∧ ∀y:[d, u]. ϕy by Theorem 10.2, and, since f doesn’t hover in (d, x) or (x, u), there are d < e < x < t < u with fe ≠ 0 and ft ≠ 0, so without loss of generality fd ≠ 0 and fu ≠ 0.

This gives four cases, according as fd < 0 or fd > 0 and as fu < 0 or fu > 0. Two of them say

∃d < u. (fd < 0 < fu ∨ fd > 0 > fu) ∧ ∀y:[d, u]. ϕy,

which is ♢ ϕ. Since f doesn’t touch from below without crossing, i.e.

(fd < 0 ∧ fu < 0) ⟹ (∀y:[d, u]. fy < 0) ∨ (∃y:[d, u]. fy > 0),

in the third case we deduce (fx ≠ 0) from the ∀ disjunct, whilst the other one provides a straddling interval [d, y] and so ♢ ϕ. The fourth yields the same conclusion since f doesn’t touch from above without crossing. Hence ϕx ⇒ ωx ∨ ♢ ϕ in all four cases. □

Lemma 14.5 If ♢ and ω satisfy relative instantiation then f doesn’t hover. Proof Given d < u, consider ϕx ≡ (d < x < u), for which

♢ ϕ ≡ ∃et. (d < e < t < u) ∧ (fe < 0 < ft ∨ fe > 0 > ft)
⇒ ∃y. (d < y < u) ∧ (fy ≠ 0).

Then (d < x < u) ⟹ (fx ≠ 0) ∨ ♢ ϕ ⟹ ∃y. (d < y < u) ∧ (fy ≠ 0). □

Lemma 14.6 If ♢ and ω satisfy relative instantiation then f doesn’t touch from below without crossing. Proof We are given e < t with fe < 0 and ft < 0. By Theorem 10.2, there are d < e < t < u with ∀x:[d, e]. fx < 0 and ∀x:[t, u]. fx < 0. Relative instantiation for ϕx ≡ (d < x < u) gives

⊤ ⇔ ∀x:[e, t]. ϕx
⇒ ∀x:[e, t]. (♢ ϕ ∨ fx < 0 ∨ fx > 0)
⇔ ♢ ϕ ∨ ∀x:[e, t]. (fx < 0 ∨ fx > 0)  Proposition 8.2(c)
⇒ ♢ ϕ ∨ (∀x:[e, t]. fx < 0) ∨ (∀x:[e, t]. fx > 0)

by compact connectedness of [e, t], since fx < 0 and fx > 0 are disjoint. But the last disjunct contradicts the hypotheses that fe < 0 and ft < 0. Finally,

♢ ϕ ⟹ ∃x:[d, u]. fx > 0 ⟹ ∃x:[e, t]. fx > 0

since ∀x:[d, e]. fx < 0 and ∀x:[t, u]. fx < 0. □

Theorem 14.7 The following are equivalent for f : ℝ → ℝ:

(a) all zeroes are stable;

(b) f doesn’t hover or touch without crossing;

(c) ♢ and ω satisfy relative instantiation, ϕx ⟹ ωx ∨ ♢ ϕ, so they define a closed overt subspace; and

(d) in any interval, ♢ and □ satisfy the mixed modal law □(ϕ ∨ ψ) ⇒ □ ϕ ∨ ♢ ψ, so they define a compact overt subspace of that interval.

Proof [a⊣⊢c] by Lemma 14.3 and Proposition 11.6, [b⊣⊢c] by the previous three lemmas and [c⊣⊢d] by Proposition 12.1. □

Corollary 14.8 In this case, Bolzano’s formula for a zero in Theorem 1.1(a),

sup {y ∈ 𝕀 | fy ≤ 0},

is, after all, not only valid in ASD but also computationally meaningful. Proof The compact overt subspace is either empty or has a maximum (Theorem 12.9), but it cannot be empty by Propositions 13.4f. □

Now we turn to the singular case, of functions that may touch without crossing. We are still looking for stable zeroes, because finding tangential points requires other evidence that the function does take a value that is equal to zero (Section 1). However, the impact of the following results (which were developed while this paper was already in the reviewing process) is on the case where the stable and unstable zeroes are densely mixed, rather than simply for polynomials with double zeroes.

In the non-singular case the operator ♢ had very strong topological properties (relative instantiation and the mixed modal law) that related it to the closed or compact space of all zeroes, but this knowledge is no longer of any help now that the two spaces are different. Note that the Brouwer degree is not defined in this situation either.

Nevertheless, we argued that Theorems 2.5 and 2.8 capture the computational ideas behind solving equations. However, we leave the translation of the former into ASD as an exercise, and instead consider a new argument that has the generality of the classical intermediate value theorem.

Example 1.2 is typical of intermediate-value questions that arise in the real world, such as exactly when the boom of 2007 turned into the crash of 2009: the more economic indicators we investigate, the muddier it becomes. The common-sense answer is that it happened during a certain interval, on which we may place upper and lower bounds. However, since these are extremely imprecise, this concession to classical pure mathematicians will not appeal to numerical analysts.

We therefore propose

Definition 14.9 A solution of an equation fx = 0 (where f : [d, u] → ℝ with fd < 0 < fu) is not necessarily a point but an occupied compact interval, i.e. a Dedekind pseudo-cut [δ, υ] in the sense of Definition 9.9. Of course, there may be many such intervals, just as f may have many zeroes in the usual pointwise sense.

Definition 14.10 An open subspace ϕ : Σ^{ℝ} is contour-closed if it is a union of open intervals at whose (Euclidean) endpoints the function is non-zero:

ϕx ⟺ ∃du. (d < x < u) ∧ (fd ≠ 0) ∧ (fu ≠ 0) ∧ ∀y:[d, u]. ϕy.

We are thinking of geographical contours here: if ϕ includes part of a hovering interval then it contains the whole of it. In Example 1.2, the interval (0, 3) is contour-closed but (0, 1\frac{2}{3}) and (1\frac{1}{3}, 3) are not. On the other hand, f doesn’t hover iff every open subspace is contour-closed.

Lemma 14.11 Any union or binary intersection of contour-closed open subspaces is contourclosed. If ϕ is contour-closed then so are its components, the convex open intervals in Theorem 13.15. If (unlike Example 1.11) f is not eventually constantly zero then ⊤ is contour-closed. □

Then the generalisation of Theorem 2.5 is

Theorem 14.12 Restricted to contour-closed open sets, the operator ♢ preserves joins and satisfies the (easy) mixed modal law □ ϕ ∧ ♢ ψ ⇒ ♢(ϕ ∧ ψ). Proof By Definition 14.1, ♢(∃i. θ_{i}) says that there is a straddling interval [d, u] that is covered by the union ∃i. θ_{i}. By Definition 14.10, each member θ_{i} of this union is itself a union of intervals (e, t) with fe ≠ 0 ≠ ft, so

♢(∃i. θ_{i}) ≡ ∃du. (fd < 0 < fu ∨ fd > 0 > fu)
∧ ∀x:[d, u]. ∃i. ∃et. (e < x < t)
∧ (fe ≠ 0 ∧ ft ≠ 0) ∧ ∀y:[e, t]. θ_{i}y.

Now we apply the Heine–Borel theorem in its traditional form to the open cover indexed by (i, e, t). This uses general Scott continuity (Axiom 9.1), the hyper-space of lists from an overt discrete space (Remark 12.16) and a combinatorial argument like those in the next section. It yields

♢(∃i. θ_{i}) ⇔ ∃du:ℚ. (fd < 0 < fu ∨ fd > 0 > fu)
∧ ∃ℓ:List (I × ℚ × ℚ).
(∀x:[d, u]. ∃(i, e, t) ∈ ℓ. (e < x < t))
∧ (∀(i, e, t) ∈ ℓ. (fe ≠ 0 ∧ ft ≠ 0) ∧ ∀y:[e, t]. θ_{i}y),

in which, by Theorem 10.2, we may assume that d, u and all of the e and t in the list ℓ are distinct. Arranging them in numerical order, some successive pair (p, q) must have fp < 0 < fq or fp > 0 > fq. Although p and q are not the e and t of any (i, e, t) ∈ ℓ because the intervals must overlap, nevertheless the interval [p, q] is part of some such [e, t], and therefore ∃i. ∀y:[p, q]. θ_{i}y. Hence ∃i. ♢ θ_{i} and the modal law also follows using Proposition 12.1 and Lemma 14.3. □

Corollary 14.13 For any function f : 𝕀 ≡ [d, u] → ℝ with fd < 0 < fu, there is a nondeterministic program ♢ ⊤ that finds arbitrarily close approximations to interval-valued stable zeroes. Proof In Theorem 1.7 we found a nested sequence of open intervals for which the function takes non-zero values with opposite signs at the endpoints. The non-hovering condition ensured that we could divide any such interval approximately in half at a new non-zero value (Theorem 2.8), although interval-Newton methods can make much better choices (Remark 2.9). Without this condition, we can apparently do no better than prod randomly (and in parallel) in search of non-zero values. Nevertheless, if we find them then the subintervals under consideration are contour-closed, so the Theorem applies to them.

The endpoints of the sequence that we choose generate a pseudo-cut, cf. Theorem 6.14. If the non-deterministic search for non-zero values is fair (in the sense that it will eventually consider any possibility that exists, and distinguish any value from zero if it is non-zero), the function is constantly zero on the interval that this pseudo-cut defines. □

In Remark 2.6 we mentioned the classical objection that the non-hovering condition is redundant, because both hovering and non-hovering functions have zeroes, respectively for trivial and constructive reasons. Instead of this disjunction of untestable cases, we can factorise the given map f : 𝕀 → ℝ into a composite of maps that capture the purely classical and purely constructive ideas. (This also re-admits the constantly zero function.)

Lemma 14.14 The relation x #_{f} z (or just x # y) defined by

∃y. (x < y < z ∨ x > y > z) ∧ fy ≠ 0

co-classifies a closed equivalence relation: it is irreflexive, symmetric and co-transitive,

x # z ⟹ x ≠ z,  x # z ⟹ z # x  and  x # z ⟹ x # y ∨ y # z,

and its equivalence classes are compact intervals (Definition 9.9). Proof Observe that x # z ⟺ δ_{z}x ∨ υ_{z}x, where

δ_{z}x ≡ ∃y. (x < y < z) ∧ fy ≠ 0  and  υ_{z}x ≡ ∃y. (x > y > z) ∧ fy ≠ 0

are rounded and disjoint but not necessarily bounded or located. For co-transitivity, suppose δ_{z}x. Then, by Theorem 10.2,

∃uw. (x < u < w < z) ∧ ∀v:[u, w]. fv ≠ 0,  whilst  u < y ∨ y < w,

of which the first disjunct gives δ_{y}x and the second δ_{z}y. □

Theorem 14.15 Any function f : 𝕀 ≡ [d, u] → ℝ factorises as f = g · q where

(a) q : 𝕀 → 𝕀/(#_{f}) is a proper surjection onto a compact Hausdorff space and has compact connected fibres; and

(b) g : 𝕀/(#_{f}) → ℝ doesn’t hover, but if fd < 0 < fu then gd < 0 < gu. If f doesn’t hover then #_{f} is ≠ and q = id_{𝕀}, whilst if f is constantly zero then # is ⊥ and 𝕀/(#_{f}) is a singleton. Proof The quotient of an overt discrete space by an open equivalence relation is constructed in [C, Section 10], but that paper only used the part of the calculus that is strictly lattice dual (without assuming Scott continuity or anything about ℕ or ℝ), so the result is also directly applicable to the quotient of a compact Hausdorff space by a closed equivalence relation. However, this uses the more general theory of Σ-split subspaces that was sketched in Remark 7.12 and does not belong to the class of simpler types that are generated by Axiom 4.1.

The condition fd < 0 < fu ensures that δ_{z} and υ_{z} are bounded, so the fibres are compact connected (Theorem 15.11). The function f respects the closed equivalence relation #_{f} because

fx ≠ fy ⟹ x #_{f} y,

and therefore factors through the quotient. The relation #_{g} is ≠ on 𝕀/(#_{f}), so g doesn’t hover and the constructive intermediate value theorem applies to it. □

This answers the opening discussion in Section 1:

Corollary 14.16 The difference between the general classical intermediate value theorem and its restricted constructive version lies exactly in the distinction between being occupied and inhabited (Definitions 8.6 and 11.5). □

Remark 14.17 In order to generalise this argument to Brouwer’s fixed point theorem or to finding zeroes of f : ℝ^{n} → ℝ^{n}, we must replace the intervals in Definition 14.10 by polyhedra on whose faces (or (n − 1)-skeleton) f ≠ 0, cf. Remark 2.7.

The argument with alternating signs that we used in Theorem 14.12 has a well known generalisation in combinatorial topology called Sperner’s Lemma [Spe28]. For example, Dirk van Dalen[vD09] used this to generalise the approximate intermediate value theorem (Proposition 13.4). In Günter Baigger’s counterexample [Bai85, Pot07] there is a grid of zeroes (or fixed points), so its only contour-closed open subset is the whole square. □

15 Local connectedness

In ASD, as in classical topology and locale theory, 𝕀 and ℝ are connected in senses that test not just pairs of open or clopen subspaces, as we did in Section 13, but sets of them. We make this generalisation in two steps, one finitary and the other infinitary, of which the second uses Heine–Borel compactness and so fails in Bishop’s theory. We deduce that the decomposition of any open set into intervals (Theorem 13.15) is unique (this is called local connectedness) and that any occupied compact interval [δ, υ] is compact connected. Finally, we relate the notions of connectedness from constructive analysis to those that have been used in category theory.

Remark 15.1 The principal arguments in this section are combinatorial, manipulating lists of rational numbers. These rely on the theory of compact overt subspaces of overt discrete spaces, of which we gave a sketch in Remark 12.16; the details are in [C, §10] and [E].

In the following lemma, we build up a permutation p of m ≡ {i : ℕ | i < m} as a composite of swaps. This uses either group theory or programming, but both in a very simple way. Unfortunately, the simplest proof of this kind becomes extremely complicated if we dwell on the minutiae of formal logical calculi. Besides the issues in Remark 12.16, it is important to understand how the formalities relate to the usual idioms of mathematics: this is explained in [Tay99, §§1.6 & 6.5].

Note in particular that the quantifier ∃p in the following lemma, which ranges over the group of permutations of ℕ that have finite support, is justified because such permutations may be encoded as integers, so this group is an overt discrete space.

The quantification over lists in Theorem 15.11 is even more delicate than this. It is essential that we work over the overt discrete space ℚ. There, any compact overt subspace is (also discrete and so) Kuratowski-finite, which means that it may be expressed as a finite list, possibly with repetitions. As we saw in Section 12, compact overt subspaces of ℝ are entirely different beasts.

Lemma 15.2 Let θ_{0}, …, θ_{m−1} be open subsets of a space X that are each inhabited in, and together cover, an overt connected subspace S ⊂ X defined by ♢, so

…, i : ℕ ⊢ θ_{i} : Σ^{X}, ♢ θ_{i} ⇔ ⊤ and … ⊢ m : ℕ, (∃i < m. θ_{i}) = ⊤_{S}.

Then the overlaps of the θ_{i} define a connected graph, in the sense that there is some permutation p : m ≅ m for which

∀i:(1 ≤ i < m). ∃j. (0 ≤ j < i) ∧ ♢ (θ_{p(i)} ∧ θ_{p(j)}).

Proof In the subsequent infinitary argument we shall need the number m here to be a parameter, so we extend the definition of θ_{i} to all i : ℕ by putting θ_{i} ≡ ⊤ for i ≥ m.

We prove by induction on 1 ≤ k ≤ m that

∃p:m ≅ m. \{ \begin{matrix}& ∀i:(1 ≤ i < k). ∃j. (0 ≤ j < i) ∧ ♢(θ_{p(i)} ∧ θ_{p(j)}) \\ ∧ & ∀i:(k ≤ i < m). p(i) = i, \end{matrix}

where the initial case k ≡ 1 is satisfied by p ≡ id and the final one k ≡ m gives the required result. Assume the induction hypothesis for some 1 ≤ k < m and put

ϕx ≡ ∃j. (0 ≤ j < k) ∧ θ_{p(j)}x and ψx ≡ ∃i. (k ≤ i < m) ∧ θ_{i}x,

so ϕ ∨ ψ = ⊤_{S}, whilst ⊤ ⇔ ♢ θ_{p(0)} ⇒ ♢ ϕ and ⊤ ⇔ ♢ θ_{m−1} ⇒ ♢ ψ. Then, since ♢ is overt connected and preserves joins, we deduce

♢(ϕ ∧ ψ) ≡ ∃ij. (0 ≤ j < k ≤ i < m) ∧ ♢(θ_{i} ∧ θ_{p(j)}).

Let s : m ≅ m be the swap that just interchanges k with such an i ≡ p(i). Then the new permutation p′ ≡ s · p satisfies the induction hypothesis for k + 1 in place of k. □

The infinitary part of the proof relies on the Heine–Borel property, in the form of Corollary 9.4, where the directed relation ranges over ℕ rather than ℚ.

Lemma 15.3 Let ∼ be an open reflexive relation on 𝕀 ≡ [0, 1], that is,

…, x, y : ℝ ⊢ (x ∼ y) : Σ such that ∀x:[0, 1]. (x ∼ x).

Then ∼ is represented by finitely many dyadic rationals, in the sense that

∃n:ℕ. ∀x:𝕀. ∃k:ℕ. (0 ≤ k ≤ 2^{n}) ∧ (x ∼ k · 2^{−n}).

Proof

⊤ ⇔ ∀x:[0, 1]. x ∼ x  reflexivity
⇒ ∀x. ∃d, u:ℝ. (d < x < u) ∧ ∀y:[d, u]. (x ∼ y)  Theorem 10.2
⇒ ∀x. ∃n, k:ℕ. (0 ≤ k ≤ 2^{n}) ∧ (x ∼ k · 2^{−n})  Lemma 6.10
⇒ ∃n. ∀x. ∃k. (0 ≤ k ≤ 2^{n}) ∧ (x ∼ k · 2^{−n}).  Cor. 9.4, n↗∞ □

Theorem 15.4 Let ∼ be an open equivalence relation on 𝕀 ≡ [0, 1], i.e. one that satisfies the previous lemma and is also symmetric (x ∼ y ⇒ y ∼ x) and transitive (x ∼ y ∼ z ⇒ x ∼ z). Then it is indiscriminate (∀x, y:𝕀. x ∼ y) and in particular 0 ∼ 1. Proof Using n from Lemma 15.3, put m ≡ 2^{n} + 1 and θ_{i}x ≡ (x ∼ i · 2^{−n}) in Lemma 15.2, so ∼ is connected in the graph-theoretic sense. As it is also symmetric and transitive, 0 ∼ 1, and more generally ∀xy:[0, 1]. x ∼ y. □

Corollary 15.5 Any open partial equivalence relation ∼ on ℝ satisfies

(∀y:[x, z]. y ∼ y) ⟹ (x ∼ z).  □

We can also generalise the traditional notion of connectedness using maps X → 2 to infinite targets, but observe that the increase in strength comes from not requiring equality on N to be decidable:

Corollary 15.6 Any function f : X → N with N discrete (where X ≡ 𝕀, ℝ, (d, u) or (υ, δ)) is constant. Proof The open equivalence relation (x ∼ y) ≡ (fx =_{N} fy) is indiscriminate. □

We can apply this result to the decomposition in Theorem 13.15.

Proposition 15.7 The relation ≈_{ϕ} defined in Lemma 13.14 is the sparsest open relation ∼ for which

ϕx ⟹ (x ∼ x),  x ∼ y ⟹ y ∼ x  and  x ∼ y ∼ z ⟹ x ∼ z,

i.e. any other such relation, ∼, also satisfies (x ≈_{ϕ} z) ⇒ (x ∼ z).

Proof If x ≤ z then (x ≈_{ϕ} z) means ∀y:[x, z]. ϕy, so ∀y:[x, z]. y ∼ y, whence x ∼ z by Corollary 15.5. □

Corollary 15.8 The decomposition of ϕ into a union of disjoint open intervals is unique. Proof Let ϕx ⇔ ∃i. θ_{i}x be another decomposition into disjoint open intervals. Then the open relation

(x ∼ y) ≡ ∃i. θ_{i}x ∧ θ_{i}y

is symmetric and satisfies (x ∼ x) ⇔ ϕx. It is transitive because θ_{i}y ∧ θ_{j}y ⇒ (i = j) is what we meant by disjointness. Hence x ≈_{ϕ} z ⇒ x ∼ z. Conversely, suppose that x ≤ z and θ_{i}x ∧ θ_{i}z; then ∀y:[x, z]. θ_{i}x since θ_{i} is by hypothesis an interval (convex), so ∀y:[x, z]. ϕx, which is x ≈_{ϕ} z. □

In Bishop’s theory, uniqueness fails in the simplest case:

Example 15.10 (Andrej Bauer) In Recursive Analysis, let n : ℕ ⊢ θ_{n} : Σ^{ℝ} be a singular cover of [0, 1], i.e. a family of intervals of total length < \frac{1}{2} that cover all definable real numbers, whilst no finite sub-family does so. Consider the relation ∼ defined by

(x ∼ z) ≡ ∃n. ∀y:[x, z]. θ_{n}y.  Then  (x ≈ z) ⟹ |x − z| < \frac{1}{2},

where ≈ is the symmetric transitive closure of ∼ (cf. the next result). Hence ≈ must have more than one equivalence class in [0, 1]. If, however, there are only finitely many classes then 0 ≈ 1 by Lemma 15.2, so there must be infinitely many of them. □

Back in ASD, we can also take advantage of the combinatorial Lemma 15.2 to prove the converse of Lemma 13.16.

Theorem 15.11 Any compact interval C ≡ [δ, υ] with δ and υ disjoint is connected. Proof Lemma 9.10 defined □ ϕ ≡ ∀x:[δ, υ]. ϕx as

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

Compact connectedness (Definition 13.2(b)) says that the space must be occupied (as it is, by Corollary 9.12) and that, for ϕ, ψ : Σ^{ℝ},

ϕ ∧ ψ ⩽ ⊥_{C} ≡ δ ∨ υ ⊢ □(ϕ ∨ ψ) ⟹ □ ϕ ∨ □ ψ.

We can restrict attention to an interval 𝕀 ≡ [d, u] with Euclidean endpoints that satisfy δd and υu. However, the hypotheses do not make ϕ and ψ disjoint on [d, u], so we must show that

∀x:𝕀. (δx ∨ ϕx ∨ ψx ∨ υx) ⟹ ∀x:𝕀. (δx ∨ ϕx ∨ υx) ∨ ∀x:𝕀. (δx ∨ ψx ∨ υx)

on the assumption that ϕ ∧ ψ ⩽ δ ∨ υ, δd, υu, ¬υd and ¬δu (using Axiom 5.6).

Let ≈_{δ}, ≈_{ϕ}, ≈_{ψ} and ≈_{υ} be the symmetric, transitive relations that are defined from ϕ, ψ, δ and υ by Lemma 13.14. By hypothesis, their union is reflexive:

∀x:𝕀. x ≈_{δ} x ∨ x ≈_{ϕ} x ∨ x ≈_{ψ} x ∨ x ≈_{υ} x.

We could use Lemma 15.3 at this point, but it seems to lead to a longer proof.

Instead, we consider the symmetric–transitive closure ∼ of this union, which is a total equivalence relation on 𝕀. Taking some care over the definition, we write

x ∼ z ≡ ∃m. ∃θ_{0}, …, θ_{m−1} ∈ {δ, ϕ, ψ, υ}. ∃y_{1}, …, y_{m−1}:ℚ. ⋀_{i=0}^{m−1}(y_{i} ≈_{θ_{i}} y_{i+1}),

in which we understand that y_{0} ≡ x, y_{m} ≡ z and d ≤ y_{i} ≤ u, whilst the θ_{i} are distinguishable labels for the predicates, not the predicates themselves. There is no need for the y_{i} to be listed in ascending arithmetical order.

It follows from Theorem 15.4 that d ∼ u, whence (relying on Remark 15.1) there is a chain of m links θ_{i} and m + 1 nodes y_{i} with y_{0} ≡ d and y_{m} ≡ u. We claim that, unless this chain is already either {δ, ϕ, υ} or {δ, ψ, υ}, there is a shorter one.

If two adjacent links have the same label, θ_{i−1} ≡ θ_{i} ≡ θ, then

∀x:[y_{i−1}, y_{i}]. θx ∧ ∀x:[y_{i}, y_{i+1}]. θx, so ∀x:[y_{i−1}, y_{i+1}]. θx,

whatever the arithmetical order of y_{i−1}, y_{i} and y_{i+1}. In this case, we may omit the node y_{i} and obtain a shorter chain. So we may assume that successive links have different labels.

Irrespectively of the labels on its links, if any node satisfies δy_{i+1} then ∀x:[y_{0}, y_{i+1}]. δx since δ is lower. If i > 0 then this offers us a shorter chain, so i = 0 and we may also re-label the first link as θ_{0} ≡ δ. Similarly, the only occurrence of υ as a label is as the final link. Hence, since δ and υ are disjoint, there must be at least three links.

Finally, we come to the key point about connectedness. If both ϕ and ψ occur as labels then they must do so adjacently, so ϕy_{i} ∧ ψy_{i} for some i, whence δy_{i} ∨ υy_{i} by hypothesis. But then θ_{i−1} = δ or θ_{i} = υ by the foregoing argument. The only remaining possibilities are the three-link chains {δ, ϕ, υ} and {δ, ψ, υ} and so the result follows. □

The remainder of this section is not included in the journal version of the paper, which just has a précis in its Remark 15.9.

Returning to Proposition 15.7, superlatives such as “sparsest” are known as universal properties, albeit only in the lattice of open partial equivalence relations. We shall now express the decomposition into intervals as a categorical universal property, making heavy use of the properties of (pre-)open maps in [C].

First we construct the “set” of components:

Proposition 15.12 From any open subspace U ⊂ ℝ there is an open surjection p : U ↠ Q/≈_{ϕ} with open connected fibres onto an overt discrete space. Proof Let the subspace U be classified by ϕ : Σ^{ℝ} without parameters. Let Q ≡ {a : ℚ | ϕa} ⊂ ℚ, which is an open subspace of an overt discrete space, and therefore itself overt discrete (Proposition 11.16), and similarly ≈ restricts to a (total) open equivalence relation on Q. Hence the quotient Q/≈ is also an overt discrete space, and the map q : Q → Q/≈ is an open surjection [C, §10].

By Theorem 10.2, the partial equivalence relation ≈ satisfies

ϕx ⟹ ∃a. (x ≈ a)  and  (x ≈ a) ∧ (x ≈ b) ⟹ (a ≈ b),

for a, b : ℚ. Hence, for x ∈ U, x ≈ a is a description that defines [a] : Q/≈, so there is a function p : U → Q/≈ that makes the triangle commute:

ℚ ^{⊃} Q

[figure: q]

[figure: ℝ; ⊃; U; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; p; Q/≈]

The fibres of p are the equivalence classes of ≈, which are the open intervals that we obtained in Theorem 13.15. The map p goes from an overt space to a discrete one, and is therefore open [C, Lemma 10.2]; it is surjective because q is.

Explicitly, by Axiom 7.10, an open subspace θ : Σ^{U} is given by θ : Σ^{ℝ} with θ ⩽ ϕ, so we define ∃_{p}θ on the equivalence class [a] : A/(≈) by

∃_{p}θ[a] ≡ ∃b. (a ≈ b) ∧ θb.

Then θx ⟹ ∃a. (x ≈ a) ∧ θa ≡ Σ^{p}(∃_{p}θ)x.

On the other hand, ψ : Σ^{Q/(≈)} is given by ψ : Σ^{ℚ} such that ψa ⩽ ϕa and (a ≈ b) ∧ ψb ⇒ ψa, so

∃_{p}(Σ^{p}ψ)[a] ≡ ∃b. (a ≈ b) ∧ ψb ⟺ ψa.

Hence ∃_{p} ⊣ Σ^{p} and p is surjective. Finally,

(ψ ∧ ∃_{p}θ)[a] ≡ ∃b. ψa ∧ θb ∧ (a ≈ b) ⟺ ∃b. ψb ∧ θb ∧ (a ≈ b) ≡ ∃_{p}(Σ^{p}ψ ∧ θ)[a],

which is the Frobenius law making p an open map. □

Lemma 15.13 The relation ≤ on Q/≈ defined by

[x] ≤ [y] ≡ ∃a, b:ℚ. x ≈ a ≤ b ≈ y

is a total but not necessarily decidable order, in the sense that

[x] ≤ [x], [x] ≤ [y] ≤ [z] ⟹ [x] ≤ [z],
[x] ≤ [y] ≤ [x] ⟹ (x ≈ y),  [x] ≤ [y] ∨ [y] ≤ [x].  □

Theorem 15.14 Every open subspace U ⊂ ℝ is locally connected:

(a) there is a map p : U ↠ Q/≈ with Q/≈ discrete;

(b) any map f : U → M to a discrete space factors uniquely as

U  [figure: p] Q/≈

....................

M \begin{aligned}f \\ &  \end{aligned}

(c) Q/≈ is overt and p is an open surjection with overt connected fibres;

(d) this representation is unique up to unique isomorphism. Proof The relation (x ∼ y) ≡ (fx =_{M} fy) is an open partial equivalence relation on ℝ with ϕx ⇒ x ∼ x, so x ≈ y ⇒ x ∼ y by Proposition 15.7. This means that f factors uniquely through the quotient [C, Lemma 10.8]. The last part is the standard argument for universal properties: put the alternative candidate in the place of M to obtain the unique isomorphism. □

Local connectedness is studied in sheaf theory a parametric way by replacing the single overt discrete object M with a family of them indexed by some space A [JT84, §V.5].

Definition 15.15 A map m : M → A is a local homeomorphism or étale map if it is open, the pullback or fibre product M ×_{A} M exists as a type (cf. Section 7) and the diagonal map M ↪ M ×_{A} M is an open inclusion. We have to make the existence of M ×_{A} M a hypothesis because this construction has not yet been done in the ASD literature.

Theorem 15.16 The map p : U → Q/(≈) is orthogonal to any étale map m : M → A.

[figure: (∼); ⊂; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; (≈); ⊂; U × U; U; p; Q/≈]

.................... h

[figure: M; . . . . . . . . . . . . . . . .; ⊂; M ×_{A} M; . . . . . . . . . . . . . . . .; M × M; f × f; M; f; m; A; g]

This means that, whenever we have a commutative square (g · p = m · f) as on the far right of the diagram above, there is a unique map h : Q/(≈) → M that makes both triangles commute (f = h · p and g = m · h). Proof All maps (≈) → A in the diagram are equal, whilst M ×_{A} M ↪ M × M ⇉ A is an equaliser, so there is a fill-in (≈) → M ×_{A} M. Then the inverse image (∼) ↪ (≈) of the open inclusion M ↪ M ×_{A} M is an open total equivalence relation on U, so (∼) = (≈).

Symbolically, for x ≈ z, we have px = pz by construction of the quotient, and so a ≡ mfx = gpx = gpz = mfz. Similarly, any x ≤ y ≤ z has x ≈ y ≈ z and so mfy = gpy = a too. This means that the interval [x, z] lies in the single fibre over a : A. The partial equivalence relation (y ∼ y′) ≡ (fy = fy′) is defined in this fibre and is open because m : M → A is étale, but it must be indiscriminate on the interval [x, z]. Thus (x ≈ z) ⇒ (x ∼ z) ≡ (fx = fz).

Since f respects the equivalence relation (≈), it factors through the quotient Q/(≈). □

16 Some counterexamples

No account of real analysis would be complete without some pathological examples, but we are saved from a morbid fascination with them by the fact that the ASD λ-calculus only allows us to define continuous functions. We concentrate on demonstrating the necessity of the new concept of overtness and leave the task of verifying the defining properties of compact overt subspaces in Definition 8.1 and Proposition 12.1 as exercises.

Remark 16.1 A word of caution. These counterexamples rely on recursion-theoretic ideas, so the difference between falsity and unprovability is crucial. This is particularly significant when we explore the notion of connectedness, because of the fact that disconnected spaces are of positive interest in topology, in a way that is not the case for (sub)spaces that fail to be open, closed or compact.

Recall from Remark 4.5 that statements σ ⇔ τ are equations between terms that have type Σ. In algebra, when we say that “s = 1 doesn’t hold”, we do not mean that s = 0. Similarly, failure of σ ⇔ ⊤ does not signify σ ⇔ ⊥ or vice versa. We shall see that this is the best way in which to use ordinary language in order to take full practical advantage of the new concept of overtness.

We find that a verbatim reading of a classical definition in a constructive context is not the same thing as what a classical mathematician would say. In particular, we can say that Examples 16.5 and 16.8 are classically but not constructively connected. The classical mathematician, on the other hand, despite his religious conviction that all questions are decidable, would actually be unable to say which they are!

Notation 16.2 Throughout this section, consider any program P whose termination is undecidable, cf. Remark 1.3(e) [Tur35], and let

g_{n} ≡ \{ \begin{matrix}0 & if P has terminated \\ 4 & if P is still running \end{matrix} \} at time n, and g ≡ ∑_{n=0}^{∞}(−\frac{1}{2})^{n}(4 − g_{n}).

Hence g ≠ 0 iff ∃n. g_{n} < 1 iff P ever terminates. We shall also assume that it’s undecidable whether g < 0 or g ≥ 0.

The first two examples are intersections of intervals.

Example 16.3 The compact interval K ≡ {g}∩{0} ⊂ [−1, +1] ⊂ ℝ (Example 8.8) is co-classified by ω ≡ δ ∨ υ, where

δd ≡ (d < 0 ∨ g ≠ 0) and υu ≡ (0 < u ∨ g ≠ 0)

define a pseudo-cut that is rounded, bounded and (in contrast to Corollary 9.12) located. By Proposition 8.2(c) and Lemmas 8.14 and 9.10,

[K]ϕ ≡ ∃du. δd ∧ υu ∧ ∀x:[d, u]. δx ∨ ϕx ∨ υx
⇔ ∀x:[−1, +1]. x < 0 ∨ g ≠ 0 ∨ x > 0 ∨ ϕx
⇔ (g ≠ 0) ∨ ϕ0.

However, since g ≠ 0 is neither provably ⊥ nor ⊤, the proposition

(K ≅ ∅) ≡ [K]⊥ ≡ ∃x. δx ∧ υx ≡ (g ≠ 0)

is undecidable. Topologically, this means that δ and υ neither overlap nor are disjoint (Corollary 9.12), whilst K is neither empty nor occupied (cf. Theorem 12.3). This example therefore fails the nullary condition for compact connectedness, although it does obey the binary one, □(ϕ ∨ ψ) ⇒ □ ϕ ∨ □ ψ.

Example 16.4 Classically, K is either ∅ or {0}. Although both ∅ and {0} are overt, whilst ∅ is open, K itself has neither property.

If we were talking about an equation between generally defined terms that is valid in both special cases, the classical rule of inference (that separate proofs for an open set and its complementary closed set suffice) would actually be admissible [D].

However, overtness is not a property of some terms or of a subspace, but a structure, ♢. This cannot be patched together from different values for ∅ and {0}, as the following more complicated examples illustrate. This is in keeping with the idea that overtness is about computational evidence.

Example 16.5 The open complement U of K, classified by ω ≡ δ ∨ υ, is classically either ℝ or ℝ \ {0}. Since K is not open, U ⊂ ℝ is not closed and U ∩ [−1, +1] is not compact. Although U is open and so overt, it is not connected in either the constructive or overt senses, since

δ ∨ υ = ⊤_{U} and ♢ δ ⇔ ♢ υ ⇔ ⊤ do not entail ♢(δ ∧ υ) ≡ (g ≠ 0) ⇔ ⊤.

However, for any map f : U → 2, the inverse images of 0, 1 ∈ 2 have to be disjoint open subspaces. Hence f must be constant. Therefore U is connected in the classical sense, though not path connected.

Also, the family {q : ℚ | ϕq}/≈_{ϕ} in Proposition 15.12 is Kuratowski-finite (overt, discrete and compact), but not finite (Hausdorff too), because −1 ≈ +1 is undecidable. □

Example 16.6 Now consider υu ≡ ∃n. g_{n} < u, which is a descending real, as in Proposition 11.17. It is (0, ∞) if P terminates and (4, ∞) if it diverges, so in particular υ1 ⇔ υ3 ⇔ υ4 since g_{n} only assumes the values 0 and 4.

Although υ is bounded on both sides in the sense that υ0 ⇔ ⊥ and υ5 ⇔ ⊤, it has no partner δ. For if (δ, υ) were a Dedekind cut, we would have

2 < 1 ⟸ δ2 ∧ υ1 and 2 < 3 ⟹ δ2 ∨ υ3

by disjointness and locatedness respectively, so δ2 would be the logical complement of υ1 ≡ υ3, solving the halting problem for P.

The convex open overt subspace υ has no left endpoint or closure, whilst it is not possible to define the interior of its closed complement, cf. Remark 10.13(c) and [I, Warning 10.9]. □

Example 16.7 Let δ ≡ −υ, so δd ≡ ∃n. d < −g_{n}. The interval

K ≡ [δ, υ] ≡ ⋂_{n}[−g_{n}, +g_{n}] ⊂ [−5, +5]

that is co-classified by δ ∨ υ is bounded and therefore compact (Lemma 9.10). It is a directed intersection of intervals with endpoints, i.e. of compact overt subspaces (Corollary 10.3(d)). It is also compact connected, by Theorem 15.11. Classically, K = {0} if P terminates and [−4, +4] otherwise. Indeed, δ0 ⇔ υ0 ⇔ ⊥, so 0 ∈ K. However, K does not have a supremum, so by Theorem 12.9 it is not overt. □

Example 16.8 Consider the closed subspace K ⊂ [0, 8] ⊂ ℝ co-classified by

ωx ≡ (x < 0) ∨ (∃n. g_{n} < x < 8 − g_{n}) ∨ (8 < x).

This is an “inside out” version of the previous example: classically it is the doubleton {0, 8} if P terminates, and the closed interval [0, 8] otherwise. It is not overt, because ♢(0, 8) would solve the halting problem.

It is compact but not compact connected: ϕx ≡ x < 4 and ψx ≡ 4 < x satisfy □ ϕ ⇔ □ ψ ⇔ ⊥ and ϕ ∧ ψ = ⊥, but □(ϕ ∨ ψ) says that P terminates, which is not provably ⊥.

However, it is classically connected: let f : K → 2; since the halves are connected,

∀x:[0, 4]. ωx ∨ (fx = f0) and ∀x:[4, 8]. ωx ∨ (fx = f8),

so ω4 ∨ (f0 = f8) ⇔ ⊤ and (f0 ≠ f8) ⇒ ω4. But ω4 says that P terminates, which is not decidable, so this can only happen if (f0 = f8) had been given. □

Example 16.9 Now let us re-consider our introductory Example 1.2 of a function that hovers near zero. The subspace

Z ≡ {(s, x) | f_{s}(x) = 0} ⊂ [−1, +1] × [0, 3] ⊂ ℝ^{2}

of all (parametric) zeroes is closed, being co-classified by

ω(s, x) ≡ (f_{s}x ≠ 0) ≡ (x < 1) ∨ (s < 0 ∧ x < 2) ∨ (s > 0 ∧ x > 1) ∨ (x > 2),

so it is compact, with necessity modal operator [Z]θ ≡ ∀s. ∀x. (f_{s}x ≠ 0) ∨ θ(s, x).

It is also overt, with possibility operator

⟨Z⟩θ ≡ (∃s:[0, +1]. θ(s, 1)) ∨ (∃x:[1, 2]. θ(0, x)) ∨ (∃s:[−1, 0]. θ(s, 2)).

Remark 16.10 Observe that, in these formulae, the variable s

(a) is an argument of the co-classifier ω of Z considered as a closed subspace, and we obtain the co-classifier ω_{s} of the intersection

Z_{s} ≅ Z ∩ ({s} × [0, 3]) ⊂ [−1, +1] × [0, 3]

simply by fixing some value for s, so ω_{s}(x) ≡ ω(s, x); but it

(b) is not an argument of (or free in) either of the modal operators [Z] or ⟨Z⟩. The first is the symbolic manifestation of the fact that inverse images preserve open and closed subspaces (Lemma 7.20). Our map f is proper, since it goes from a compact space to a Hausdorff one, so the inverse image of any compact subspace is compact, but it is not open, so the inverse image of an overt subspace need not be overt.

Remark 16.11 Nevertheless Z_{s} ≡ {x | f_{s}(x) = 0} ⊂ [0, 3] is compact, because we obtain [Z_{s}] from ω_{s} in the same way as we obtained [Z] from ω, namely

[Z_{s}]ϕ ⇔ (∀x. f_{s}x ≠ 0 ∨ ϕx) ⇔ (s > 0 ∧ ϕ1) ∨ (∀x:[1, 2]. ϕx) ∨ (s < 0 ∧ ϕ2).

In the three separate cases where s < 0, s ≡ 0 and s > 0, Z_{s} is an overt closed interval with endpoints (max and min):

Z_{s} min Z_{s} max Z_{s}  ω_{s}x  [Z_{s}]ϕ  ⟨Z_{s}⟩ϕ
s < 0  [2, 2] 2  2  x ≠ 2  ϕ2  ϕ2
s ≡ 0  [1, 2] 1  2 x < 1 ∨ x > 2 ∀x:[1, 2]. ϕx ∃x:[1, 2]. ϕx
s > 0  [1, 1] 1  1  x ≠ 1  ϕ1  ϕ1

For any value s such that Z_{s} is overt, and therefore has endpoints, the observable predicate

min Z_{s} < max Z_{s}

is equivalent to the statement s = 0, but equality is not observable. Such an equivalence cannot be a single assertion — we must distinguish the cases s = 0 and s ≠ 0 before we can make it. Hence there is no single definition of ⟨Z_{s}⟩, max Z_{s}, min Z_{s} or choice of a zero of the function that is continuous in the parameter s.

In particular, for the undecidable value g, the subspace of all zeroes,

Z_{g} ≅ Z ∩ ({g} × [0, 3]) ⊂ [−1, +1] × [0, 3],

which is the intersection of two overt subspaces, is not itself overt. If it were, the proposition min Z_{g} < max Z_{g} would solve the halting problem for the program P.

Remark 16.12 We could alternatively try to define ⟨S_{s}⟩ either

(a) naïvely from the set of stable zeroes, cf. Exercise 2.10, but then ⟨S_{0}⟩ϕ ≡ ⊥; or

(b) from the function, as in Definition 14.1(e),

⟨S_{s}⟩ϕ ≡ ∃xy. (∀z:[x, y]. ϕz) ∧ (f_{s}x < 0) ∧ (f_{s}y > 0),

but then ⟨S_{s}⟩(0, 3) ⇔ ⊤, whilst ⟨S_{s}⟩(0, 1\frac{2}{3}) ⇔ (s > 0) and ⟨S_{s}⟩(1\frac{1}{3}, 3) ⇔ (s < 0), so this only preserves ∨ when s ≠ 0. □

The functions in the remaining examples don’t hover, but our search for a non-stable zero is hindered by the failure of existence and uniqueness respectively.

Example 16.13 Consider the parametric function that touches without crossing,

−1 ≤ s ≤ +1, −1 ≤ x ≤ +1 ⊢ f_{s}(x) ≡ x^{2} − s.

The subspaces Z ⊂ ℝ^{2} and Z_{s} ⊂ ℝ, which are defined as in the previous example, are both closed and compact. The co-classifier ω_{s} and necessity operator [Z_{s}] depend continuously on s, with

(Z_{s} ≅ ∅) ≡ [Z_{s}]⊥ ⟺ (s < 0).

But, for s ≡ g, this is not decidable, so Z_{g} is not overt, by Theorem 12.3. Indeed,

b^{2} = s ≥ 0 ⊢ ⟨Z_{s}⟩ϕ ⇔ ϕ(−b) ∨ ϕ(+b)
s < 0  ⊢ ⟨Z_{s}⟩ϕ ⇔ ⊥,

which is not continuous in s when ϕ ≡ ⊤.

On the other hand, we may define ⟨S_{s}⟩ either naïvely from the set of stable zeroes (Exercise 2.10) or from the function (Definition 14.1(e)):

⟨S_{s}⟩ϕ ⇔ ∃xy. (x^{2} < s < y^{2}) ∧ ∀z:[x, y]. ϕz
⇔ \{ \begin{matrix}ϕ(−b) ∨ ϕ(+b) & if b^{2} = s > 0 \\ ⊥ & if s ≤ 0. \end{matrix}

Notice the subtle change in the case analysis at s ≡ 0: the one for ⟨S_{s}⟩ is Scott-continuous because the inverse image of ⊥ : Σ^{Σ^{ℝ}} is the closed subspace with s ≤ 0, whereas previously we had tried to make it the open subspace with s < 0. □

Remark 16.14 Of course, as s decreases, the square roots merge and then disappear, but they vanish from S_{s} before they go from Z_{s}. In fact, we have

S_{s} = Z_{s} ∩ {x | s > 0},

so that S_{s} is locally closed (Axiom 7.10). Indeed, I have not been able to find any function f for which S_{f} does not have this property. □

Example 16.15 Consider the parametric function

−1 ≤ s ≤ +1, −π ≤ x ≤ +π ⊢ f_{s}(x) ≡ s · sin x,

but this time we want to find x for which f_{s}(x) takes its maximum value (over all x but particular s), rather than 0. As we know that the maximum value is |s|, this is the same as solving the equation

|s| − s · sin x = 0.

(Using Theorem 6.14 we may define sin x as a power series, but a polynomial such as f_{s}x ≡ sx(1 − x^{2}) would do instead. The absolute value function is an example of Exercise 12.10.) Then, as before, the parametric space of all solutions,

Z ≡ [0, 1] × \{+\frac{1}{2}π\} ∪ \{0\} × [−π, +π] ∪ [−1, 0] × \{−\frac{1}{2}π\},

is closed, compact and overt, whilst Z_{s} is closed, compact and occupied, with

[Z_{s}]ϕ ≡ (s < 0 ∨ ϕ(+π/2)) ∧ (s ≠ 0 ∨ ∀x:[−π, +π]. ϕx) ∧ (s > 0 ∨ ϕ(−π/2)).

If Z_{s} were overt, it would have a maximum and minimum, but this is discontinuous near s = 0. Indeed

s < 0 ⊢ ⟨Z_{s}⟩ϕ ⇔ ϕ(+π/2)
s ≡ 0 ⊢ ⟨Z_{s}⟩ϕ ⇔ ∃x:[−π, +π]. ϕx
s > 0 ⊢ ⟨Z_{s}⟩ϕ ⇔ ϕ(−π/2),

which is not continuous in s. On the other hand, ⟨S_{s}⟩ = ⊥, and in particular ⟨S_{s}⟩ = ⊥, whether we define them from the function or from the set of stable zeroes. □

References

[Bai85] Günter Baigger. Die Nichtkonstruktivität des Brouwerschen Fixpunktsatzes. Archiv für Mathematische Logik und Grundlagenforschung, 25(3-4):183–188, 1985.

[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, pages i–vi, Hagen, Germany, August 2008.

[BB85] Errett A. Bishop and Douglas S. Bridges. Constructive Analysis. Number 279 in Grundlehren der mathematischen Wissenschaften. Springer-Verlag, 1985.

[Bol17] Bernhard P. J. N. Bolzano. Rein analytischer Beweis des Lehrsatzes, dass zwischen je zwey Werthen, die ein entgegengesetztes resultat gewähren, wenigstens eine reelle Wurzel der Gleichen liege. 1817. English translation by Steve Russ in Historia Mathematica 7 (1980), 156–185 and The Mathematical Works of Bernhard Bolzano, Oxford University Press, 2004, pages 253–277.

[BR87] Douglas S. Bridges and Fred Richman. Varieties of Constructive Mathematics. Number 97 in London Mathematical Society Lecture Notes. Cambridge University Press, 1987.

[Bro75] Jan Brouwer. Collected Works: Philosophy and Foundations of Mathematics, volume 1. North-Holland, 1975. Edited by Arend Heyting.

[Cau21] Augustin-Louis Cauchy. Cours d’Analyse de l’école royale polytechnique, première partie: Analyse algébrique. 1821. Œvres complètes, série 2, tome 3.

[Cle87] John C. Cleary. Logical arithmetic. Future Computing Systems, 2:125–149, 1987.

[Dav05] E. Brian Davies. A defence of mathematical pluralism. Philosophia Mathematica, 13(3):252–276, 2005.

[DG03] James Dugundji and Andrzej Granas. Fixed Point Theory. Springer Verlag, 2003.

[Dug66] James Dugundji. Topology. Allyn and Bacon, 1966.

[EJ92] Jean-Claude Evard and Farhad Jafari. A complex Rolle’s theorem. American Mathematical Monthly, 99:858–869, 1992.

[EL04] Abbas Edalat and André Lieutier. Domain theory and differential calculus. Mathematical Structures in Computer Science, 14(6):771–802, 2004.

[Fox45] Ralph H. Fox. On topologies for function-spaces. Bulletin of the American Mathematical Society, 51, 1945.

[Gen35] Gerhard Gentzen. Untersuchungen über das Logische Schliessen. Mathematische Zeitschrift, 39:176–210 and 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 Manfred E. Szabo.

[GHK^{+}80] Gerhard Gierz, Karl Heinrich Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael Mislove, and Dana S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, 1980. Second edition, Continuous Lattices and Domains, published by Cambridge University Press, 2003.

[GLT89] Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[Göd31] Kurt Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38:173–198, 1931. English translations, “On Formally Undecidable Propositions of ‘Principia Mathematica’ and Related Systems” published by Oliver and Boyd, 1962 and Dover, 1992; also in “From Frege to Gödel: a Source Book in Mathematical Logic, 1879–1931”, ed. Jan van Heijenoort, Harvard University Press, 1967.

[Har08] G. H. Hardy. A Course of Pure Mathematics. Cambridge University Press, 1908. Tenth edition, 1952, frequently reprinted.

[Hey56] Arend Heyting. Intuitionism, an Introduction. Studies in Logic and the Foundations of Mathematics. North-Holland, 1956. Third edition, 1971.

[HM81] Karl H. Hofmann and Michael Mislove. Local compactness and continuous lattices. In Bernhard Banaschewski and Rudolf-Eberhard Hoffmann, editors, Continuous Lattices, number 871 in Springer Lecture Notes in Mathematics, pages 209–248, 1981.

[Hyl91] J. Martin E. Hyland. First steps in synthetic domain theory. In Aurelio Carboni, Maria-Cristina Pedicchio, and Giuseppe Rosolini, editors, Proceedings of the 1990 Como Category Conference, number 1488 in Lecture Notes in Mathematics, pages 131–156. Springer-Verlag, 1991.

[Joh82] Peter T. Johnstone. Stone Spaces. Number 3 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.

[Joh84] Peter T. Johnstone. Open locales and exponentiation. Contemporary Mathematics, 30:84–116, 1984.

[JT84] André Joyal and Myles Tierney. An extension of the Galois theory of Grothendieck. Memoirs of the American Mathematical Society, 51(309), 1984.

[Kur20] Kazimierz Kuratowski. Sur la notion d’ensemble fini. Fundamenta Mathematicae, 1:130–1, 1920.

[Lak63] Imre Lakatos. Proofs and refutations: the logic of mathematical discovery. British Journal for the Philosophy of Science, 14:1–25, 1963. Re-published by Cambridge University Press, 1976, edited by John Worrall and Elie Zahar.

[Llo78] Noel Lloyd. Degree Theory. Number 73 in Cambridge Tracts in Mathematics. Cambridge University Press, 1978.

[Man83] Mark Mandelkern. Constructive continuity. Memoirs of the American Mathematical Society, 42(277), 1983.

[Mil97] John W. Milnor. Topology from the Differentiable Viewpoint. Princeton University Press, 1997.

[Moo66] Ramon E. Moore. Interval Analysis. Automatic Computation. Prentice Hall, 1966. Second edition, Ramon Edgar Moore, Baker R Kearfott and Michael J Cloud, ”Introduction to Interval Analysis”, Society for Industrial and Applied Mathematics, Philadephia, 2009, ISBN 0989716691.

[Nac92] Leopoldo Nachbin. Compact unions of closed subsets are closed and compact intersections of open subsets are open. Portugaliae Mathematica, 49:403–9, 1992.

[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 Hubert Kennedy, Selected Works of Giuseppe Peano, Toronto University Press, 1973, pp 190–205.

[Pét53] H. Pétard. A contribution to the mathematical theory of big game hunting. Eureka, 16, 1953. Reprinted in Lion hunting and other mathematical pursuits by Ralph Boas, Gerald Alexanderson and Dale Mugler, Mathematical Association of America, 1995.

[Plo77] Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

[Pot07] Petrus H. Potgieter. Computable counter-examples to the Brouwer fixed-point theorem. arXiv:0804.3199, 2007.

[Ric56] Henry G. Rice. On completely recursively enumerable classes and their key arrays. Journal of Symbolic Logic, 21:304–8, 1956.

[Sco72] Dana S. Scott. Continuous lattices. In F. W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, number 274 in Lecture Notes in Mathematics, pages 97–136. Springer-Verlag, Berlin, 1972.

[Spe28] Emanuel Sperner. Neuer Beweis für die Ivarianz der Dimensionzahl und des Gebietes. Abh. Math. Sem. Hamburg, V:265–272, 1928.

[Spi10] Bas Spitters. Located and overt sublocales. Annals of Pure and Applied Logic, 2010. to appear.

[SS70] J. Arthur Seebach and Lynn Arthur Steen. Counterexamples in Topology. Holt, Rinehart and Winston, 1970. Republished by Springer-Verlag, 1978 and by Dover, 1995.

[Sto37] Marshall H. Stone. Applications of the theory of Boolean rings to general topology. Transactions of the American Mathematical Society, 41(3):375–481, 1937.

[Sto38] Marshall H. Stone. The representation of Boolean algebras. Bulletin of the American Mathematical Society, 44(12):807–816, 1938.

[Tay99] Paul Taylor. Practical Foundations of Mathematics. Number 59 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999.

[Tur35] Alan M. Turing. On computable numbers with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society (2), 42:230–265, 1935.

[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.

[vD09] Dirk van Dalen. Brouwer’s ε-fixed point from Sperner’s lemma. 2009.

[Ver94] Japie J. C. Vermeulen. Proper maps of locales. Journal of Pure and Applied Algebra, 92:79–107, 1994.

[Wei00] Klaus Weihrauch. Computable Analysis. Springer, Berlin, 2000.

[Wil70] Peter Wilker. Adjoint product and hom functors in general topology. Pacific Journal of Mathematics, 34:269–283, 1970.

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 2010.

[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.

[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.

[I] Andrej Bauer and Paul Taylor, The Dedekind reals in abstract Stone duality. Mathematical Structures in Computer Science, 19 (2009) 757–838.

[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.

[N] Paul Taylor, Computability in locally compact spaces. 2010.

As I was a reluctant analyst, this work would never have been done without the persistent (but friendly) cajoling of Graham White and Andrej Bauer. I would like to express my warmest appreciation for the ongoing encouragement that they have both given me. In particular, during my visit to Ljubljana in November 2004, Andrej provided the construction of the supremum of a compact overt subspace in Section 12 using Dedekind cuts that is the keystone of this paper. He also pointed out Remark 1.12 and Examples 2.11.

This work was presented at Computability and Complexity in Analysis in Kyoto in August 2005, and I am grateful to Peter Hertling and the CCA programme committee for the indulgence of allowing me to occupy altogether 80 pages of their (pre-conference) proceedings.

The paper that you see here is the fruit of illuminating discussions with numerous people since the conference. I would particularly also like to thank Jeremy Avigad, Vasco Brattka, Douglas Bridges, Robin Cockett, Thierry Coquand, Martín Escardó, Nicola Gambino, André Joyal, Achim Jung, Norbert Müller, Erik Palmgren, Petrus Potgieter, Pino Rosolini, Giovanni Sambin, Peter Schuster, Anton Setzer, Bas Spitters and Steve Vickers for their interest and encouragement in this project.

Finally, I would like to thank the anonymous referees for their care. Lengthy technical papers are not so uncommon, but in this case someone from well outside my usual circle was obliged to make a seismic shift in his entire understanding of the way in which mathematics is done. I deeply appreciate the grace with which he was willing and able to do this.