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 recursiontheoretic 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
g_{n} ≡  ⎧ ⎨ ⎩ 
 ⎫ ⎬ ⎭  at time n, and g ≡ 
 (−½)^{n}(4−g_{n}). 
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 coclassified by ω≡δ∨υ, where
δ d≡(d< 0∨ g≠ 0) and υ u≡(0< u∨ g≠ 0) 
define a pseudocut 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
(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: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 Kuratowskifinite (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
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< −g_{n}.
The interval
K ≡ [δ,υ] ≡ ⋂_{n} [−g_{n},+g_{n}] ⊂ [−5,+5] 
that is coclassified 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]⊂ℝ coclassified by
ω x ≡ (x< 0) ∨ (∃ n.g_{n}< x< 8−g_{n}) ∨ (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: φ 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,
∀ 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 reconsider our introductory Example 1.2
of a function that hovers near zero.
The subspace
Z ≡ {(s,x) ∣ f_{s}(x)=0} ⊂ [−1,+1]×[0,3] ⊂ ℝ^{2} 
of all (parametric) zeroes is closed, being coclassified by
ω(s,x) ≡ (f_{s} 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.(f_{s} x≠ 0) ∨ θ(s,x).
It is also overt, with possibility operator
<Z> θ ≡ (∃ 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
Z_{s} ≅ Z⋂( 
 ×[0,3]) ⊂ [−1,+1]×[0,3] 
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
[Z_{s}] φ ⇔ (∀ x. f_{s} 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, 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
minZ_{s} < maxZ_{s} 
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,
Z_{g} ≅ Z⋂( 
 ×[0,3]) ⊂ [−1,+1]×[0,3], 
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
<S_{s}>φ ≡ ∃ x y.(∀ z:[x,y].φ z) ∧ (f_{s} x< 0) ∧ (f_{s} y> 0), 
The functions in the remaining examples don’t hover, but our search for a nonstable 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 ⊢ f_{s}(x) ≡ x^{2}−s. 
The subspaces Z⊂ℝ^{2} and Z_{s}⊂ℝ, which are defined as in the previous example, are both closed and compact. The coclassifier ω_{s} and necessity operator [Z_{s}] depend continuously on s, with
(Z_{s}≅∅) ≡ [Z_{s}]⊥ ⇔ (s< 0). 
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 Scottcontinuous 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
S_{s} = Z_{s}⋂ {x ∣ s> 0}, 
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
−1≤ s≤ +1, −π≤ x≤ +π ⊢ f_{s}(x) ≡ s ·sinx, 
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
s − s · sinx = 0. 
(Using Theorem 6.14 we may define sinx as a power series, but a polynomial such as f_{s} x≡ s x(1−x^{2}) 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
[Z_{s}]φ ≡ (s< 0∨φ(+π/2)) ∧ (s≠ 0∨∀ x:[−π,+π].φ x) ∧ ( s> 0∨φ(−π/2)). 
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. ▫