From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/36 Path: news.gmane.org!not-for-mail From: gcuri@math.unipd.it Newsgroups: gmane.science.mathematics.categories Subject: Re: Kantor dust Date: Sun, 1 Feb 2009 19:18:33 +0100 Message-ID: Reply-To: gcuri@math.unipd.it NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1233532942 19386 80.91.229.12 (2 Feb 2009 00:02:22 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 2 Feb 2009 00:02:22 +0000 (UTC) To: categories@mta.ca Original-X-From: categories@mta.ca Mon Feb 02 01:03:35 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1LTmHm-0003lA-PH for gsmc-categories@m.gmane.org; Mon, 02 Feb 2009 01:03:35 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LTljM-0001bb-Oc for categories-list@mta.ca; Sun, 01 Feb 2009 19:28:00 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:36 Archived-At: Further references on the constructive presentation of Cantor space are: 1. P. Martin-Lof, Notes on Constructive Mathematics. Almqvist and Wiksel= l, 1970. 2. M. Fourman, R. Grayson, Formal Spaces. In: The L.E.J. Brouwer Centenar= y 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 equ= ivalent to spatiality of formal Cantor space (Cantor locale). Best regards, Giovanni Curi Quoting 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. > > > > > > > ----------------------------------------------------------------- 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