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:I→ℝ.

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,

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(|f e|,|f t|), 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₀ true when U₀⊃I, 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 ∣ f x≠ 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

In particular, ◊(U₁∪ U₂)=⇒◊U₁∨◊U₂.

The hovering Example 1.2 fails this property for U₁≡(0,1⅔) and U₂≡(1⅓,3).

Proof    Suppose that I≡[d,u]⊂⋃_{j∈ J} U_j with f d< 0< f u, and consider the open subspaces (with > for V⁺ and < for V⁻)

For each x∈I, there are j∈ J and e,t∈I 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 f y≠ 0 and [x,y]⊂ U_j. Then x∈ V⁺ or x∈ V⁻, according to the sign of f y. Hence I⊂ V⁺∪ V⁻, whilst d∈ V⁻ and u∈ V⁺ by hypothesis.

Now, since I is connected, V⁺∩ V⁻ is non-empty, so it contains some open interval, in which f doesn’t hover, so f x≠ 0 for some x∈ V⁺∩ V⁻. If f x< 0 then (since x∈ V⁺) there is a straddling interval [x,y]⊂ U_j with f y> 0; similarly if f x> 0 we have x∈ V⁻ and f y< 0. See Theorem 14.12 for another proof of this.         ▫

Remark 2.6 Some extra condition is necessary to prove this Theorem in ℝ¹, 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 Iⁿ 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:I²→I² 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∈ f U) 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∈ f U iff there is a compact subspace K⊂ U with 0∈ V⊂ f K, where V is open. Specialising further to f:ℝⁿ→ℝ^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, u₀≡ 1 and, by recursion, e≡⅓(2 d_n+u_n) and t≡⅓(d_n+2 u_n), so

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

1. 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 ∣ f x≠ 0}.
2. 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

Then

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=S′, its closure, since ◊U ⇔ (U∩ S′≠∅).         ▫

Remark 2.13 We learn from this that

1. 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;
2. 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 ℝ¹;
3. the operator ◊ is the bounded existential quantifier: ◊U≡∃ x∈ S.(x∈ U);
4. there are long-standing arguments in analysis and
5. general algorithms that use these operators (abstracted from the original question) to solve many kinds of problem in a uniform way; so
6. ◊-like properties stand exactly at the gateway between the mathematical and computational aspects of topology; but
7. 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⊂I 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

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. 

for any open subspaces U,V⊂ X. Then

1. the operator ▫ preserves finite intersections,

   ▫X  is true   and   ▫U∧▫V =⇒ ▫(U⋂ V),

2. whereas ◊ preserve finite unions (Theorem 2.5),

   ◊∅  is false   and   ◊(U⋃ V) =⇒ ◊U∨◊V.

3. The corresponding closed subspace X∖ W is non-empty iff ▫∅ is false
   iff ◊X is true ,
4. and it is a singleton iff ▫ preserves unions, iff ◊ preserves intersections .
5. 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,

whilst

hold iff S is dense in Z.         ▫

Example 2.17 If f x ≡ (x−1)²(x+2) ≡  x³−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.