Abstract Stone Duality - introduction/survey papers
People have been asking me for several years to write "introductions" to ASD, or to "write down all the axioms together". This was not possible while the core theory for locally compact spaces was still being investigated, but that process has essentially come to an end. There are now FOUR introduction/survey papers, aimed at different audiences, and all available from www.PaulTaylor.EU/ASD (lamcra) "A Lambda Calculus for Real Analysis" suitable for a general mathematical audience (intawi) "Interval Analysis Without Intervals" aimed at programmers of "exact real arithmetic" but not finished (dedras) "The Dedekind Reals in Abstract Stone Duality" (with Andrej Bauer) suitable for theoretical computer scientists (foufct) "Foundations for Computable Topology" I was invited to write this last paper for a volume on Foundations of Mathematics that is more inclined towards philosophy than technicalities and has contributions from categorists, set theorists and philosophers. My paper therefore begins with a discussion of the methodology behind ASD, and in particular the thesis that foundations can be devised FOR mathematics (rather than vice versa) by encapsulating headline theorems as universal properties and translating these into systems of introduction/elimination/beta/eta rules for new logical connectives. ASD abstracts Stone duality between algebra and topology by saying that the carriers of the algebras belong to the dual category of spaces, and formalises this as a monad. The topological meaning of Beck's characterisation of monadic adjunctions is that (certain) equalisers exist and carry the subspace topology in a canonical way. Several examples of this are given, in particular related to compactness of the real closed interval. Then the lambda calculus associated with the monad is described. The key object is the Sierpinski space Sigma. The Euclidean and Phoa principles are deduced from the property of classifying all, open or closed subsets. (A proof is included that Sierpinski classifies closed sublocales.) Conversely, the monadic and Euclidean principles make Sigma a dominance. Discrete, Hausdorff, compact and overt spaces are discussed. Set theory (ie the theory of discrete spaces) is used as a comparative case. Although most of the details of other arguments are only sketched, this paper includes the whole of the proof of the characterisation of elementary toposes using the ideas of ASD, without any mention of subobjects. Sketches of other parts of the theory are also given. The paper tries to tell the whole story of the development of ASD, from a foundational and empirical point of view, It is therefore of necessity a "broad brush" approach, as the material would easily fill a book. This paper is also meant to be complementary to the others listed above, so it says very little about the applications to elementary real analysis. It also says very little about the computational interpretation of ASD, but, at least as far as the real numbers are concerned, you can expect to hear more from Andrej and me on this subject in the future. If you would like to comment on "Foundations for Computable Topology", please do so before the end of July. Paul Taylor www.PaulTaylor.EU/ASD/foufct
participants (1)
-
Paul Taylor