## 2  Stable zeroes and straddling intervals

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

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

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

But the interesting thing for us is that Sf 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 Sf, that is, it contains a stable zero xUSf, then U contains (the whole of) a straddling interval,

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

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 |fg|<ε, 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 ◊U0 true when U0I, whilst ◊∅ is obviously false. Since ◊ requires the whole of the interval [e,t] to be contained in the open set, not just its endpoints, ◊Wf is also false, where Wf≡{xf 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

 ◊(⋃j∈ J Uj) ⇔ ∃ j∈ J.◊Uj.

In particular, ◊(U1U2)=⇒◊U1∨◊U2.

The hovering Example 1.2 fails this property for U1≡(0,1⅔) and U2≡(1⅓,3).

Proof    Suppose that I≡[d,u]⊂⋃jJ Uj with f d< 0< f u, and consider the open subspaces (with > for V+ and < for V)

 V± ≡  {x:ℝ ∣ ∃ j:J.∃ y:ℝ. (x< y)∧(f y≷ 0)∧ [x,y]⊂ Uj}.

For each xI, there are jJ and e,tI such that x∈(e,t)⊂[e,t]⊂ Uj, but since f doesn’t hover in (x,t) there’s some x< y< t with f y≠ 0 and [x,y]⊂ Uj. Then xV+ or xV, according to the sign of f y. Hence IV+V, whilst dV and uV+ 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 xV+V. If f x< 0 then (since xV+) there is a straddling interval [x,y]⊂ Uj with f y> 0; similarly if f x> 0 we have xV 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 ℝ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 In 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:I2I2 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:XY 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 KU with 0∈ Vf K, 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 xU⊂ℝ satisfies ◊U. If ◊ arises from the intermediate value problem for a non-hovering function, any such x is a stable zero.

Proof    Let d0≡ 0, u0≡ 1 and, by recursion, e≡⅓(2 dn+un) and t≡⅓(dn+2 un), so

 ⊤  ⇔ ◊(dn,un)  ≡  ◊((dn,t) ⋃(e,un))  ⇔ ◊(dn,t) ∨ ◊(e,un);

then at least one of the disjuncts is true, so let (dn+1,un+1) be either (dn,t) or (e,un).

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 dn and un converge to a common limit x, respectively from below and above. If xU then x∈(dn,un)⊂(x±ε)⊂ U for some ε> 0 and n, but ◊(dn,un) 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 ◊(UV) 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 ≡ (US≠∅) ≡ ∃ xS.(xU), 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 ≡ ∃ xS.(xU), where S is the open subspace {xf 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 ◊⋃iI Ui iff ∃ i.◊Ui, 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 UW iff US≠∅. If ◊ had been derived from some S′ as in Exercise 2.10 then S=S, its closure, since ◊U ⇔ (US′≠∅).         ▫

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 ℝ1;
3. the operator ◊ is the bounded existential quantifier: ◊U≡∃ xS.(xU);
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 ZfI 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 WX of a compact Hausdorff space then

 ▫U   iff   (U⋃ W)=X.

The “finite open sub-cover” definition of compactness says exactly that ▫⋃iI Ui iff ▫⋃iF Ui for some finite FI. 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 WX 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,VX. 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 XW 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 Zf of all zeroes, and ◊ using the overt subspace Sf of stable zeroes of a non-hovering continuous function ℝ→ℝ. In the non-singular situation these coincide, but for singular cases of the parameters, Sf is properly contained in Zf.

Proposition 2.16 If ▫ and ◊ arise from subspaces SZ of a Hausdorff space X, with Z≡(XW) compact, then they satisfy the modal laws: for all open U,VX,

 ▫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 f x ≡ (x−1)2(x+2) ≡  x3−3x+2 then Zf={1,−2} and Sf={−2}. The last two laws fail for the intervals U≡(−3,−1) and V≡(0,2).         ▫

Remark 2.18 Therefore, whilst the subsets Sf and Zf 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.