connectedness

[Paul Taylor <pt07@PaulTaylor.EU>]

Vaughan Pratt's original enquiry was actually in the context of
graph theory (as I suspected at the time, and he subsequently
confirmed), but I would like to add something from the point of
view of constructive real analysis.

First, though, I would like to underline something that Steve Lack
(almost) said, namely that the category in which you index your
components, and therefore also the one in which you define
connectedness, need to be EXTENSIVE, ie their coproducts should
be disjoint, and stable under pullback, and the initial object strict.

Maybe we've over-done philology recently, but "component" means
"putting together", where we expect the parts to cover the whole
(coproduct), without overlapping (disjoint), to be distinguishable
(like disjoint union, but unlike addition and disjunction).
The modern notion of extensivity, in which Steve had a part,
captures this idea very neatly.   The equivalence between definitions
of connectedness based on 1+1 and on X+Y surely depends on stability
under pullback, and the requirement that the choice between left
and right be unique surely requires disjointness.   Maybe a close
study of Marta Bunga's work on abstract connectedness would clarify
this.

Vaughan originally asked about various categories of algebras,
and Steve mentioned commutative rings, but quietly turned their
arrows around.   Stone duality would suggest to me that one should
look for connectedness of algebras in their OPPOSITE category of
"spaces", which I understand in a generic sense that includes
sets, graphs, predomains, locales and affive varieties.

Turning to constructive analysis, let me call the categorical
definitions above that involve coproducts "binary" and
"infinitary classical connectedness".

In (almost) traditional topological language, a space X has the
binary classical connectedness property if, for any two open
subspaces U and V of X,
   IF they cover and are disjoint and inhabited THEN false.

The definition of connectedness that is used in constructive
analysis moves one of the hypotheses to the conclusion:
   IF they cover and are inhabited THEN their intersection is inhabited.

 From this definition we immediately obtain an APPROXIMATE INTERMEDIATE
VALUE THEOREM: IF a function f:X->R on a connected space takes both
positive (greater than -epsilon is enough) and negative (less than
+epsilon) values, say on inhabited open spaces U and V, then, as
U and V cover, they must intersect, ie the function takes values
within epsilon of zero.

There are well known examples of spaces that pass the classical
definition of connectedness, whilst intuitively being made up of
two or more parts (for example the graph of sin(1/x) together with
the y-axis).  Fewer spaces are connected in the constructive sense,
but I can't see any examples in which this might fix the classical
mis-definition.

There are other ways of permuting the hypotheses and conclusions of
this definition.  In particular, when the space X is compact, the
notion of covering it with opens can be internalised using the
universal quantifier or necessity operator [].   Similarly, if it
is overt, habitation can be internalised using the existential
quantifier or possibility operator <>.

Pushing these conditions across the implication can only be done
over an intuitionistic set theory at the cost of double negation.
However, in ASD, where open and closed subspaces are related via
continuous functions, and not set-theoretic complementation, the
Phoa principle allows this switch to be made without the not-not.

In the case of a compact overt space such as the interval [0,1],
the classical, constructive, compact and over definitions of
connectedness agree.

For a space that is either not compact or not overt, one of the
hypotheses must remain as an equation on the left of  |-.

Then constructive and overt connectedness agree:
    U cup V = X  |-   <>U  and  <>V   implies   <>(U cap V)

Compact connectedness is
    U cap V = 0  |-   [](U cup V)   implies   []U   or   []V.

The latter gives rise to another approximate intermediate value
theorem:   if  f:K->R  takes values  >=0  and <=0  on  OCCUPIED
subspaces, then its space of zeroes is also occupied.

Here, OCCUPIED is the name that I propose for compact spaces whose
terminal projection is a proper surjection,  just as an INHABITED
space is an overt one with an open surjection to 1.  An occupied
space need not have any points.

So far, I have only mentioned BINARY notions of connectedness,
but if we want to talk about families of connected COMPONENTS
then we must also consider INFINITARY connectedness (as Marta
stressed).  Here the results for the constructive real line are
somewhat surprising.

In order to avoid dependent types, I have found it more convenient
to discuss infinitary connectedness in terms of equivalence relations.

In classical analysis, any OPEN EQUIVALENCE RELATION on [0,1],
ie any open subspace of the square that includes the diagonal,
is symmetric in it and has the transitivity property, is
INDISCRIMINATE - it relates 0 to 1 and indeed any point to any
other.

This is not the case in Bishop's or Russian Recursive Analysis.
There is an open equivalence relation on [0,1] with infinitely
many equivalence classes, ie the interval fails the infinite
connectedness condition.   The quotient by this equivalence
relation, ie the space that indexes the components, is discrete
but not Hausdorff, ie it admits an equality relation that is
not decidable.

This one of the reasons why, at variance with many constructive
analysts, I believe that the HEINE--BOREL theorem is a necessary
part of analysis.

In ASD, which obeys Heine--Borel, any open equivalence relation
on [0,1] or R is indiscriminate, as in the classical situation,
and the line and interval are connected in the infinitary senses.
Moreover, any open subspace of R is the disjoint union of countably
many open intervals, where each of these words needs careful
constructive re-definition.

These results are in my paper "A lambda calculus for real analysis",
which was presented at CCA 2005 and you can obtain from
    www.PaulTaylor.EU/ASD
I should point out that I am at the moment re-writing part of this
paper, to include a "need to know" introduction to continuous lattices,
cf my recent posting on this.  However, the results that I have
discussed above are in the "stable" part of the text.

Paul Taylor