Re: Kantor dust

Re: Kantor dust

[gcuri]

Further references on the constructive presentation of Cantor space are:

1. P. Martin-Lof,  Notes on Constructive Mathematics. Almqvist and Wiksell,
1970.

2. M. Fourman, R. Grayson, Formal Spaces. In: The L.E.J. Brouwer Centenary
Symposium,  A.S. Troelstra and D. van Dalen, eds. North Holland, 1982, pp.
107-122.

Compactness of Cantor space is equivalent to the fan theorem which is equivalent
to spatiality of formal Cantor space (Cantor locale).

Best regards,

        Giovanni Curi


Quoting 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.
>
>
>
>
>
>
>




-----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

Dipartimento di Matematica Pura ed Applicata
Universita' degli Studi di Padova
www.math.unipd.it

Re: Kantor dust

[Vaughan Pratt]

Paul Taylor wrote:
> 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/
> [...]
> ABSTRACT STONE DUALITY:  Andrej Bauer and Paul Taylor,  "The Dedekind
>   reals in abstract Stone duality",  www.PaulTaylor.EU/ASD/dedras

In concrete Stone duality, increasing structure on one side is offset by
decreasing structure on the other.  One would hope for a similar
phenomenon in abstract Stone duality.

If we can consider constructivity as part of the structure of an object,
then we should expect that the more constructive some type of object,
the less constructive the "object of all objects of that type."   So for
example if (total) recursive functions are demonstrably more
constructive than partial recursive functions by some criterion, we
should expect the set of all recursive functions to be *less*
constructive than that of partial recursive functions by the same
criterion, rather than more.

The phenomena you're observing here seem entirely consistent with this
principle, and point up the need to be clear, when judging
constructivity in some context, whether it is the collection or the
individuals therein being so judged, with the added complication that
Stone duality makes the roles of collection and individual therein
interchangeable, such as when elements of sets are understood as
ultrafilters of Boolean algebras.

Vaughan Pratt

Kantor dust

[Paul Taylor]

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.