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.
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
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
participants (3)
-
gcuri＠math.unipd.it -
Paul Taylor -
Vaughan Pratt