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 intervalhalving 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 nonEuclidean 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
◊⊤ ⇔ ⊤ and …, φ,ψ:Σ^{H}, φ∨ψ=⊤_{C} ⊢ ◊φ∧◊ψ =⇒ ◊(φ∧ψ), 
▫⊥ ⇔ ⊥ and …, φ,ψ:Σ^{H}, φ∧ψ=⊥_{C} ⊢ ▫φ∨▫ψ ⇐= ▫(φ∨ψ), 
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 coclassified 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 ψ
coclassify. [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:
ε> 0 ∧ ∃ x z:X.(−ε< f x)∧(f z<+ε) =⇒ ∃ y:X.(−ε< f y<+ε), 
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
⊥ ⇔ (∀ x.0< f x)∨(∀ x.f x< 0) ≡ ▫φ∨▫ψ ⇐= ▫(φ∨ψ) ≡ (∀ x.f x≠ 0). ▫ 
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
[f C](φ∨ψ) ≡ [C](φ· f∨ψ· f) =⇒ [C](φ· f)∨[C](ψ· f) ≡ [f C]φ∨[f C]ψ. 
Similarly, if φ∨ψ=⊤_{f C} with C overt then φ· f∨ψ· f=⊤_{C} and
<f C>(φ∧ψ) ≡ <C>(φ· f∧ψ· f) ⇐= <C>(φ· f)∧<C>(ψ· f) ≡ <f C>φ∧<f C>ψ. ▫ 
From here one could go on to develop the idea of pathconnectedness. 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 nonempty compact overt subspace of a
Hausdorff space, so it has (▫,◊) satisfying both mixed modal
laws (Proposition 12.1).
Then the following are equivalent:
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
▫(φ∨ψ)⇔⊤ ⊣⊢ φ∨ψ=⊤_{C} ⊢ ◊φ∧◊ψ=⇒◊(φ∧ψ), 
which is equivalent to (b) by Axiom 5.6. Similarly (d) is
◊(φ∧ψ)⇔⊥ ⊣⊢ φ∧ψ=⊥_{C} ⊢ ▫(φ∨ψ)=⇒▫φ∨▫ψ, 
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 latticedual 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 nonempty 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 ℝ:
maxK≡ a∈ (e,t)⊂[e,t]⊂φ⊂ℝ. 
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 onedimensional version of path connectedness.
Proposition 13.12
The following are equivalent for the open subspace
classified by α:Σ^{ℝ}:
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
◊φ_{y} ≡ δ y, ◊ψ_{y} ≡ υ y but ◊(φ_{y}∧ψ_{y}) ⇔ ∃ x.(y< x)∧(x< y) ⇔ ⊥. 
If α y⇔⊥ then α x⇒(x≠ y)⇒φ_{y} x∨ψ_{y} x, so ⊤_{C}≡α⊑φ_{y}∨ψ_{y} and we may use overt connectedness. Then
α y⇔⊥ ⊢ δ y∧υ y ≡ ◊φ_{y}∧◊ψ_{y} =⇒ ◊(φ_{y}∧ψ_{y}) ≡ ⊥, 
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.

is an open partial equivalence relation on ℝ that is reflexive exactly on the open subspace classified by φ:
φ x ⇔ (x≈ x), x≈_{φ}y=⇒ y≈_{φ}x and x≈_{φ}y≈_{φ}z=⇒ x≈_{φ}z. ▫ 
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 timevariable 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
δ d≡▫(λ z.d< z) and υ u≡▫(λ x.x< u) 
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,
δ y∨υ y ≡ ▫φ_{y}∨▫ψ_{y} ⇐= ▫(φ_{y}∨ψ_{y}) ≡ ▫(λ x.y< x∨ x< y) ≡ ω y. ▫ 
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 fourfold 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 coclassified by an ascending or descending real number are connected, even though they are not compact and need not be overt.