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,
[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 |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_{0} true when U_{0}⊃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
◊(⋃_{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⅔) and U_{2}≡(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^{−})
V^{±} ≡ {x:ℝ ∣ ∃ j:J.∃ y:ℝ. (x< y)∧(f y≷ 0)∧ [x,y]⊂ U_{j}}. |
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 ℝ^{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 I^{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:I^{2}→I^{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∈ 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:ℝ^{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≡⅓(2 d_{n}+u_{n}) and t≡⅓(d_{n}+2 u_{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. ▫
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=S′, its closure, since ◊U ⇔ (U∩ S′≠∅). ▫
Remark 2.13 We learn from this that
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
▫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
▫X is true and ▫U∧▫V =⇒ ▫(U⋂ V), |
◊∅ is false and ◊(U⋃ V) =⇒ ◊U∨◊V. |
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 f x ≡ (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.