13  Connectedness

Connectedness is the abstraction of the intermediate value theorem from ℝ to other topological spaces, so the classical proof that the interval is connected is essentially that of Theorem 1.1(a). This is a weak definition because it denies the existence of a strong kind of separation, into clopen parts.

The accounts that we find in constructive analysis use a weaker test, which therefore yields stronger definitions of connectedess, and fewer spaces are connected in the constructive sense. Indeed Example 16.5, which deletes “part of” a point from the line, is not connected constructively, whereas it would appear to satisfy the classical definition. But, as usual, the difference between the classical and constructive results is subtle, so this does not in fact change the status of the traditional examples of unintuitively connected spaces [SS70].

For their constructive definition and proof that I is connected, the followers of Brouwer and Bishop make use of the interval-halving argument in Theorems 1.1(b) and 1.7, which Mark Mandelkern [Man83] attributes to Ray Mines and Fred Richman. It leads directly to a useful approximate form of the intermediate value theorem: see [TvD88, Proposition 6.1.4] for the Brouwer school and [BB85, Theorem 2.4.8] for Bishop’s.

Category theory uses yet another formulation, with arbitrary discrete spaces in place of 2. This is again a stronger notion of connectedness, to the extent that Bishop cannot prove that ℝ satisfies it, because this relies on the Heine–Borel theorem. However, as the investigation also requires a combinatorial argument, we postpone it to Section 15, and confine our attention in this section to the binary notions of connectedness.

Remark 13.1 In these definitions, tests of “separation” may be expressed by saying that certain open subspaces cover or are inhabited. These ideas are naturally expressed in terms of the modal operators ▫ and ◊ that we have developed, and these allow us to say respectively whether compact and overt subspaces are connected.

This gives rise to two versions of even our definition, with two approximate intermediate value theorems. This is another example of the way in which ASD elucidates the open–closed duality in topology. It turns out that the Brouwer–Bishop definition agrees with ours for overt subspaces.

A consequence of this duality in ASD (in which Axiom 5.6 is crucial) is that we may use the classical proof that I is connected, which it is in all of the senses that we consider. Unlike Theorem 1.7, our proof does not use dependent choice.

Our dual results for compact spaces do not seem to occur in the constructive literature. There are several possible reasons for this, one of which is that the conclusion of our definition is a disjunction. Other constructive theories are based on intuitionistic set theory, where ∨ carries much a stronger sense than in ASD, cf. the remarks before Lemma 13.16. So our results about compact connectedness would probably have to be wrapped in double negations in Bishop’s or Brouwer’s settings, making them just inferior versions of the ones that they already have.

Another reason is that, according to Bishop’s usage, a “compact” subspace also has to be totally bounded, and therefore overt (Remark 12.15), so he never considers compact intervals [δ,υ] with non-Euclidean endpoints (Definition 9.9). But these are exactly the compact connected subspaces of ℝ in ASD (Theorem 15.10), whilst the proof of this apparently requires the Heine–Borel property, which Bishop does not accept.

Definition 13.2 We call an open or closed subspace C⊂ H of a Hausdorff space

1. overt connected if it is given by ◊:Σ^ΣH (Definition 11.1) for which

   ◊⊤ ⇔ ⊤   and   …,  φ,ψ:ΣH,  φ∨ψ=⊤C   ⊢   ◊φ∧◊ψ =⇒ ◊(φ∧ψ),

   so whenever C⊂ U∪ V is covered by inhabited open subspaces, they must intersect;
2. compact connected if it is given by ▫:Σ^ΣH (Definition 8.1) for which

   ▫⊥ ⇔ ⊥   and   …,  φ,ψ:ΣH,  φ∧ψ=⊥C   ⊢   ▫φ∨▫ψ ⇐= ▫(φ∨ψ),

   so whenever C⊂ U∪ V is covered by disjoint open subspaces then one of them is enough.

The modal operators in these expressions are the quantifiers that say that C is overt (Proposition 11.11 or 11.16) or compact (Theorem 8.16 or Exercise 8.20(e)) as a space in itself. We defined these quantifiers (applied to ψ:Σ^C) in terms of the map I:Σ^C↣Σ^X given by Axiom 7.10. (C now stands for “connected”, not closed.)

It will now be more convenient to use the modal operators themselves, applied to φ,ψ:Σ^X, instead of constructing the subspace C. If C is open, classified by α:Σ^H, then the equation φ=⊥_C means φ∧α=⊥:Σ^H and φ=⊤_C means φ⊒α:Σ^H. On the other hand, if it is a closed subspace co-classified by ω:Σ^H then φ=⊥_C means φ⊑ω:Σ^H and φ=⊤_C means φ∨ω=⊤:Σ^H (Axiom 7.10).

Exercise 13.3 Give the English translation of the symbolic definitions, but in terms of the closed subspaces that φ and ψ co-classify. [Hint: they swap places.]

We will show that ℝ is overt connected and that I has both properties, but first we see how the two definitions yield the approximate intermediate value theorems.

Proposition 13.4 Any function f:X→ℝ on an overt connected space X that takes values both above −ε and below +ε also takes values within any ε>0 of zero:

so the open, overt subspace {x:X ∣  |f x|<ε} is inhabited.

Proof    Let φ x≡(−ε< f x) and ψ x≡(f x<+ε). Then ◊φ⇔◊ψ⇔⊤ by hypothesis, and φ∨ψ=⊤_X by locatedness for ℝ (Axiom 4.9). Then overt connectedness says that

Compact connectedness gives another approximate intermediate value theorem:

Proposition 13.5 Let f:K→ℝ be a function on a compact connected space such that both of the closed, compact subspaces {x:K ∣ f x≥ 0} and {x:K ∣ f x≤ 0} are occupied (Definition 8.6). Then so too is their intersection, Z≡{x:K ∣ f x=0}.

Proof    Let φ x≡(0< f x) and ψ x≡(f x< 0), so φ∧ψ=⊥_K, whilst by hypothesis ▫φ⇔▫ψ⇔⊥, Then compact connectedness says that

These two approximate theorems may be seen as transferring connectedness along a function between two spaces, which we can also say more abstractly:

Proposition 13.6 The direct image under f:X→ Y of a compact or overt connected subspace C⊂ X, in the senses of Theorem 8.9 and Notation 11.13 respectively, is also connected as a subspace of Y.

Proof    Let φ,ψ:Σ^Y. If φ∧ψ=⊥_{f C} with C compact, so φ· f∧ψ· f=⊥_C, then

Similarly, if φ∨ψ=⊤_{f C} with C overt then φ· f∨ψ· f=⊤_C and

From here one could go on to develop the idea of path-connectedness. However, we really need to show that our two definitions agree with each other and with the traditional one. This is where the modal operators and their mixed laws come into their own, and once again the Phoa principle makes it all work.

Proposition 13.7 Let C⊂ H be a non-empty compact overt subspace of a Hausdorff space, so it has (▫,◊) satisfying both mixed modal laws (Proposition 12.1). Then the following are equivalent:

1. ◊ defines an overt connected subspace;
2. ▫(φ∨ψ) ∧ ◊φ ∧◊ψ =⇒ ◊(φ∧ψ) ;
3. if two disjoint open sets cover C then they are not both inhabited;
4. ▫ defines a compact connected subspace;
5. ▫(φ∨ψ) =⇒ ▫φ ∨ ▫ψ ∨ ◊(φ∧ψ);
6. if two disjoint open sets cover C then just one of them already covers it;
7. if K⊂ C is clopen then either K=∅ or K=C; and
8. any function f:C→2 is constant.

Examples 16.5 and 16.8 are classically connected, but the former is not compact and so cannot satisfy (a), whilst the latter fails (d) and overtness.

Proof    When we have both modal operators available, we may use Definitions 8.1 and 11.1 to turn equations of type Σ^C into propositions. Hence (a) becomes

which is equivalent to (b) by Axiom 5.6. Similarly (d) is

which is equivalent to (e) by Axiom 5.6.

Under the same transformation, condition (c) says

which, by Axiom 5.6, is equivalent to (b), whilst (f) says

which is (e).

The traditional formulations (g,h) are equivalent to these by Lemmas 6.4 and 12.5, so it remains to show that (b) and (e) are equivalent.

[b⊢e]: One mixed modal law (with φ and ψ in both roles and using distributivity) gives

which is almost the same as (e), apart from the last disjunct, for which we use (b).

[e⊢b]: The lattice-dual argument using other mixed modal law gives

which only differs from (b) in the first conjunct, for which we use (e).         ▫

Now we concentrate on the space I≡[d,u]⊂ℝ, which is closed, compact and overt by Proposition 11.7. We find that the classical proof (Theorem 1.1(a)) is valid in ASD:

Lemma 13.8 Any non-empty clopen subspace K⊂[d,u] contains the endpoint u.

Proof    By Lemma 12.5, K is overt and compact, so by Theorem 12.9 it has a maximum element, a∈ K⊂I≡[d,u]. Now, K is in particular the relative open subspace of I that is classified by the restriction of some φ:Σ^ℝ (cf. Axiom 7.10), so φ a⇔⊤. By Theorem 10.2, a is in the interior of φ, now treated as an open subspace of ℝ:

If u≠ a then a< u, so, without loss of generality, a< t< u. Since K is also closed, let ψ:Σ^ℝ classify its complement. Putting these ideas together,

so (u≠ a)⇒⊥, but this means u=a∈ K by Definition 4.8.         ▫

Theorem 13.9 The interval I is connected in all of the above senses.

Proof    For Proposition 13.7(g), let I=K∪ K′ be a disjoint union of clopen subspaces. By Theorem 12.3, it is decidable whether K is empty, but if it is not then u∈ K by the Lemma, and similarly for K′. Then, of the four cases

only the second and third have K and K′ complementary.         ▫

Theorem 13.10 The real line ℝ is overt connected.

Proof    Let φ,ψ:Σ^ℝ with φ∨ψ=⊤_ℝ and (∃ x:ℝ.φ x)⇔⊤⇔(∃ z:ℝ.ψ z).

Recalling the idioms for ∃ (Axiom 5.10), consider the restrictions of φ and ψ to [x,z] or [z,x]. These satisfy the hypotheses for overt connectedness of the closed interval, so (∃ y:[x,z].φ y∧ψ y)⇔⊤,  whence (∃ y:ℝ.φ y∧ψ y)⇔⊤.         ▫

The approximate intermediate value theorems for I→ℝ and ℝ→ℝ now follow:

Corollary 13.11 Let f:I≡[d,u]→ℝ be any (continuous) function satisfying f(d)≤ 0≤ f(u), even one that hovers (Example 1.2). Then the compact subspace Z⊂I of all zeroes is occupied.         ▫

Next we characterise open intervals in the sense of Example 11.17. The formulations of convexity come from [Man83]; they are a one-dimensional version of path connectedness.

Proposition 13.12 The following are equivalent for the open subspace classified by α:Σ^ℝ:

1. it is an overt connected subspace;
2. it is inhabited and paraconvex:  α x ∧ (x< y< z) ∧ α z =⇒ α y;
3. it is inhabited and convex:  α x ∧ (x< z) ∧ α z =⇒ ∀ y:[x,z].α y;  and
4. α=δ∧υ, an inhabited open interval.

Proof    Any open subspace is overt, with ◊φ≡∃ x:ℝ.α x∧φ x, by Proposition 11.16, and all four conditions give ◊⊤⇔⊤.

[c⊢a]: We adapt the proof of Theorem 13.10, with the open subspace classified by α instead of ℝ. If α⊑φ∨ψ, α x∧φ x and α z∧ψ z then by convexity the closed interval [x,z] or [z,x] is covered by (α∧φ)∨(α∧ψ). Hence overt connectedness of this interval gives ∃ y.α y∧φ y∧ψ y.

[a⊢d] By Proposition 11.18, α⊑δ∧υ where δ d≡◊(λ z.d< z)≡∃ z.(d< z)∧α z and υ u≡◊(λ x.x< u)≡∃ x.α x∧(x< u). For equality, let y:ℝ and consider φ_y≡λ z.(y< z) and ψ_y x≡λ x.(x< y), so

If α y⇔⊥ then α x⇒(x≠ y)⇒φ_y x∨ψ_y x, so ⊤_C≡α⊑φ_y∨ψ_y and we may use overt connectedness. Then

so δ∧υ⊑α by Axiom 5.6.

[d⊢c⊣⊢b]: By Theorem 10.2 and since δ is lower and υ is upper.         ▫

Exercise 13.13 Show that the locally closed intervals such as [e,δ) in Exercise 11.19 are also overt connected.

This notion of open interval (with descending and ascending endpoints instead of Euclidean ones) is the one that we require in order to complete the classification of open subspaces of ℝ that we began in Remark 10.13.

Lemma 13.14 For any φ:Σ^ℝ,

is an open partial equivalence relation on ℝ that is reflexive exactly on the open subspace classified by φ:

This idea was used in Theorem 2.5; we explicitly make it symmetric because the formulae in Corollary I 10.8 for the bounded quantifier ∀ z:[x,y].φ z depended on x≤ y.

Theorem 13.15 Every open subspace of ℝ is the union of disjoint open intervals.

Proof    As with any equivalence relation, the classes are “disjoint” in the sense that if any two overlap, they actually coincide. Each of these classes is convex open and therefore an interval in our sense. Finally, (x≈_φx)⇒φ x from the definition. We return to this decomposition in Proposition 15.7.         ▫

Turning to compact connectedness, the analogue of Proposition 13.12(a⊢d) appears to solve a problem that we might at first think is impossible. Imagine arriving from a hike at an isolated bus stop to find the timetable obliterated. The one daily bus is not there now (ω x), but how can we decide whether we should wait for it (δ x) or if it has already gone (υ x)? In fact, this just illustrates that the meaning of ∨ is weaker in ASD than in other constructive logics: our argument strengthens the observation about the present to a time-variable one, saying that either the bus hasn’t come yet or it will never come again, but it doesn’t say which of these is the case.

Lemma 13.16 Any compact connected subspace K≡(▫,ω)⊂ℝ is an occupied compact interval [δ,υ] (Definition 9.9).

Proof    By Proposition 9.13, δ∨υ⊑ω, where

are rounded and bounded. They are disjoint by Corollary 9.12 because K is occupied.

To show that δ∨υ⊒ω, let y:ℝ and consider φ_y≡λ x.(y< x) and ψ_y x≡λ x.(x< y), so φ_y∧ψ_y=⊥. Then by compact connectedness,

Corollary 13.17 Any compact overt connected subspace K⊂ℝ is an interval [d,u] with Euclidean endpoints, where d≡infK≤ u≡supK by Theorem 12.9.         ▫

It seems that we cannot prove that every compact interval [δ,υ] is connected either as the dual of Proposition 13.12(c⊢a) or by using Scott continuity applied to Theorem 13.9. We have to apply a combinatorial argument to the four-fold cover by δ∨φ∨ψ∨υ (Theorem 15.10).

There are two other situations about which the definitions that we have given are unable to say anything. First, there ought to be a general notion of overt subspace instead of the open, closed and locally closed special cases. Second, we would also like to say that the closed subspaces [δ,+∞) and (−∞,υ] that are co-classified by an ascending or descending real number are connected, even though they are not compact and need not be overt.