Kantor dust

[Paul Taylor <pt09@PaulTaylor.EU>]

There are some significant mathematical points that can be made in
response to Vasili Galchin's question about the "constructive"
existence of Cantor space,  but I fear that these are going to get
lost in the cross-fire of comments that neither state their background
assumptions nor lay out the mathematics.  It is well over a century
since we discovered that it is meaningless to talk about the absolute
truth or falsity of (semantical) statements in mathematics.

There are many many people and foundational positions that call
themselves "constructive".   Unfortunately the experts in these
theories have a tendency to assert a monopoly on the word, and ignore
the existence of the other points of view,  whilst non-experts
repeat half-remembered and mis-understood opinions that may originate
from the opponents and not the proponents of the theories.   On the
other hand, Peter Schuster and Giovanni Sambin have made some effort
in recent years to bring these disciplines together.

I am not going to attempt to make a list of "constructive" theories,
and I would strongly advise against referring to such lists elsewhere,
ESPECIALLY in Wikipedia.   Nor am I going to try to represent positions
other than my own -- I invite the respective experts to do this.

Traditionally, Cantor space is described as a subspace of R or [0,1]
using the "middle third" construction,  but I learned it like that
long before I became a constructivist of any kind, so I don't know
whether there are any constructive subtleties associated with this view.

I think of Cantor as the exponential  2^N,  so FOR EXAMPLE it makes
sense to talk about it in any CCC, or a topos.   However, the
interesting question is what it looks like as a TOPOLOGICAL SPACE,
in the many different interpretations of that phrase.

We can do topology starting from the points, or starting from the
open sets.  In the latter case, these have a basis whose members are
named by FINITE sets of integers:  a point of Cantor space is a
decidable (possibly) infinite set of integers, and lies in a basic
open set if the infinite set includes the finite one.

The first interesting mathematical question is this: if we define
Cantor space starting from its points, but take these to be given
by TOTAL RECURSIVE FUNCTIONS  N-->2,  and then put the topology
that I have just mentioned on it,  what are the properties of this
topology?   In particular, is it compact?

The answer is no, because of the "Kleene Tree".  This is a computably
defined infnite tree that has no infinite computable path.  There
are many descriptions of this, including one by Andrej Bauer:
math.andrej.com/2006/04/25/konigs-lemma-and-the-kleene-tree/

The second interesting mathematical point is that, by looking at the
open sets instead of the points as our formulation of topology, the
answer is different.

The whole of this discussion can be conducted using the closed real
interval in place of Cantor space,  so many things are better
documented in the literature for one example rather than the other.
In particular, compactness of the interval has more careful
descriptions in:

LOCALE THEORY: Michael Fourman and Martin Hyland, "Sheaf models for
  analysis", in Michael Fourman, Chris Mulvey, and Dana Scott, editors,
  "Applications of Sheaves", number 753 in Lecture Notes in Mathematics,
  pages 280--301. Springer-Verlag, 1979.

FORMAL TOPOLOGY:  Jan Cederquist and Sara Negri, "A constructive proof
   of the Heine--Borel covering theorem for formal reals", in
   Stefano Beradi and Mario Coppo, editors, "Types for Proofs and
   Programs", number 1158 in Lecture Notes in Computer Science,
   page 6275. Springer-Verlag, 1996.

ABSTRACT STONE DUALITY:  Andrej Bauer and Paul Taylor,  "The Dedekind
   reals in abstract Stone duality",  www.PaulTaylor.EU/ASD/dedras

I wrote a sketch (not a properly written paper) about the construction
of Cantor Space in ASD and its compactness in "Tychonov's Theorem in
ASD",
www.PaulTaylor.EU/ASD/misclc.php#tyctas

Paul Taylor

PS Please refer to my website as paultaylor.eu, not monad.me.uk, as
it will be moving home shortly, and I will be better able to ensure
continuity of service for the name paultaylor.eu,  whilst I would like
to discontinue monad.me.uk at some stage.