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

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

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,

However, since g≠ 0 is neither provably ⊥ nor ⊤,  the proposition

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

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

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< −g_n. The interval

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

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,

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

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

so it is compact, with necessity modal operator [Z] θ  ≡  ∀ s.∀ x.(f_s x≠ 0) ∨ θ(s,x).

It is also overt, with possibility operator

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

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):

For any value s such that Z_s is overt, and therefore has endpoints, the observable predicate

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>, maxZ_s, minZ_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,

which is the intersection of two overt subspaces, is not itself overt. If it were, the proposition minZ_g < maxZ_g would solve the halting problem for the program P.

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

1. naïvely from the set of stable zeroes, cf. Exercise 2.10, but then <S₀>φ≡⊥; or
2. from the function, as in Definition 14.1(e),

   <Ss>φ  ≡  ∃ x y.(∀ z:[x,y].φ z) ∧ (fs x< 0) ∧ (fs y> 0),

   but then <S_s>(0,3) ⇔⊤,  whilst <S_s>(0,1⅔)⇔(s> 0) and <S_s>(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,

The subspaces Z⊂ℝ² 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

But, for s≡ g, this is not decidable, so Z_g is not overt, by Theorem 12.3. Indeed,

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)):

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

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

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

(Using Theorem 6.14 we may define sinx as a power series, but a polynomial such as f_s x≡ s x(1−x²) 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 Z_s is closed, compact and occupied, with

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

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.         ▫