## 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

gn  ≡

 0 if P has terminated 4 if P is still running

at time  n,   and   g ≡
 ∞ ∑ n=0
(−½)n(4−gn).

Hence g≠ 0 iff ∃ n.gn< 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]φ ≡ ∃ d u.δ 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:U2, 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.11 is Kuratowski-finite (overt, discrete and compact), but not finite (Hausdorff too), because −1≈+1 is undecidable.         ▫

Example 16.6 Now consider υ u≡∃ n.gn< 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 gn 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 Warning I 10.9.         ▫

Example 16.7 Let δ≡−υ, so δ d≡∃ n.d< −gn. The interval

 K  ≡  [δ,υ]  ≡  ⋂n [−gn,+gn] ⊂ [−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.10. 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.gn< x< 8−gn)  ∨  (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: φ xx< 4 and ψ x≡ 4< x satisfy ▫φ⇔▫ψ⇔⊥ and φ∧ψ=⊥, but ▫(φ∨ψ) says that P terminates, which is not provably ⊥.

However, it is classically connected: let f:K2; since the halves are connected,

 ∀ x:[0,4].ω x∨(f x=f 0)   and   ∀ x:[4,8].ω x∨(f x=f 8),

so ω 4∨(f 0=f 8)⇔⊤ and (f 0≠ f 8)⇒ω 4. But ω 4 says that P terminates, which is not decidable, so this can only happen if (f 0=f 8) 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) ∣ fs(x)=0}  ⊂  [−1,+1]×[0,3]  ⊂  ℝ2

of all (parametric) zeroes is closed, being co-classified by

 ω(s,x)  ≡  (fs 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.(fs x≠ 0) ∨ θ(s,x).

It is also overt, with possibility operator

  θ  ≡   (∃ 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

1. is an argument of the co-classifier ω of Z considered as a closed subspace, and we obtain the co-classifier ωs of the intersection
Zs  ≅  Z⋂(
 ⎧ ⎨ ⎩ s ⎫ ⎬ ⎭
×[0,3])  ⊂  [−1,+1]×[0,3]
simply by fixing some value for s, so ωs(x)≡ω(s,x); but it
2. 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 Zs≡{xfs(x)=0}⊂[0,3] is compact, because we obtain [Zs] from ωs in the same way as we obtained [Z] from ω, namely

 [Zs] φ  ⇔  (∀ x. fs 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, Zs is an overt closed interval with endpoints (max and min):

 Zs minZs maxZs ωs x [Zs]φ φ 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 Zs is overt, and therefore has endpoints, the observable predicate

 minZs < maxZs

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 <Zs>, maxZs, minZs 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,

Zg  ≅  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 minZg < maxZg would solve the halting problem for the program P.

Remark 16.12 We could alternatively try to define <Ss> either

1. naïvely from the set of stable zeroes, cf. Exercise 2.10, but then <S0>φ≡⊥; or
2. from the function, as in Definition 14.1(e),
 φ  ≡  ∃ x y.(∀ z:[x,y].φ z) ∧ (fs x< 0) ∧ (fs y> 0),
but then <Ss>(0,3) ⇔⊤,  whilst <Ss>(0,1⅔)⇔(s> 0) and <Ss>(1⅓,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    ⊢   fs(x)  ≡  x2−s.

The subspaces Z⊂ℝ2 and Zs⊂ℝ, which are defined as in the previous example, are both closed and compact. The co-classifier ωs and necessity operator [Zs] depend continuously on s, with

 (Zs≅∅)  ≡  [Zs]⊥  ⇔ (s< 0).

But, for sg, this is not decidable, so Zg is not overt, by Theorem 12.3. Indeed,

 b2=s≥ 0 ⊢ φ  ⇔  φ(−b)∨φ(+b) s< 0 ⊢ φ  ⇔  ⊥,

which is not continuous in s when φ≡⊤.

On the other hand, we may define <Ss> either naïvely from the set of stable zeroes (Exercise 2.10) or from the function (Definition 14.1(e)):

<Ss∃ x y.(x2sy2)∧∀ z:[x,y].φ z

 φ(−b)∨φ(+b) if  b2=s> 0 ⊥ if  s≤ 0.

Notice the subtle change in the case analysis at s≡0: the one for <Ss> 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 Ss before they go from Zs. In fact, we have

 Ss  =  Zs⋂ {x ∣ s> 0},

so that Ss is locally closed (Axiom 7.10). Indeed, I have not been able to find any function f for which Sf does not have this property.         ▫

Example 16.15 Consider the parametric function

 −1≤ s≤ +1,  −π≤ x≤ +π    ⊢   fs(x)  ≡  s ·sinx,

but this time we want to find x for which fs(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 · sinx  =  0.

(Using Theorem 6.14 we may define sinx as a power series, but a polynomial such as fs xs x(1−x2) would do instead. The absolute value function is an example of Exercise 12.10.) Then, as before, the parametric space of all solutions, is closed, compact and overt, whilst Zs is closed, compact and occupied, with

 [Zs]φ  ≡  (s< 0∨φ(+π/2))  ∧  (s≠ 0∨∀ x:[−π,+π].φ x)  ∧  ( s> 0∨φ(−π/2)).

If Zs were overt, it would have a maximum and minimum, but this is discontinuous near s=0. Indeed

 s< 0 ⊢ φ  ⇔  φ(+π/2) s≡ 0 ⊢ φ  ⇔  ∃ x:[−π,+π].φ x s> 0 ⊢ φ  ⇔  φ(−π/2),

which is not continuous in s. On the other hand, <Ss>=⊥, and in particular <Ss>=⊥, whether we define them from the function or from the set of stable zeroes.         ▫