Re: Kantor dust

[gcuri@math.unipd.it]

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