Foundations for Computable Topology

Paul Taylor

This paper is an introduction to Abstract Stone Duality, in particular its philosophical methodology and the underlying ideas from category theory and Stone duality. An abridged version will appear in Foundational Theories of Classical and Constructive Mathematics, edited by Giovanni Sommaruga and published by Springer-Verlag (BibTeX).


Foundations should be designed for the needs of mathematics and not vice versa. We propose a general technique for doing this that exploits mathematical results in categorical logic and the duality between algebra and geometry.

This paper is a survey of the application of this technique to devising a revolutionary re-axiomatisation of general topology called Abstract Stone Duality. The Sierpinski space plays a key role as the classifier for both open and closed subspaces.

ASD is inherently computable, and has a very strong duality between open and closed concepts. It provides a purely recursive theory of elementary real analysis in which, unlike in previous approaches, the real closed interval [0,1] in ASD is compact.



Acknowledgements

I would like to thank I would like to thank Andrej Bauer, David Corfield, Anders Kock, Fred Linton, Gabor Lukasz, Andy Pitts, Sridhar Ramesh, Guiseppe Rosolini, Giovanni Sommaruga, Hayo Thielecke and Graham White for their very helpful comments on earlier drafts of this paper.


BibTEX entries

   @incollection{TaylorP:fofct,
      author    = {Taylor, Paul},
      title     = {Foundations for Computable Topology},
      editor    = {Sommaruga, Giovanni},
      booktitle = {Foundational Theories of Classical
                   and Constructive Mathematics},
      year      = 2011, month   = {January},
      number    = 76,
      publisher = {Springer-Verlag},
      series    = {Western Ontario Series in Philosophy of Science},
      isbn      = {978-94-007-0430-5},
      url       = {PaulTaylor.EU/ASD/foufct}}

Download the paper to print it

PDF,  DVI,  compressed PostScript  or  A5 booklet.


Table of contents and the HTML version

The HTML version is not up to date; it will be revised when the paper is finished and the book goes to print.


Abstract and quotations


1. Foundations for mathematics


2. Category theory and type theory

Introduction, elimination, beta and eta rules for logical connectives, and their relationship to adjunctions in category theory. Building a category from a type theory.


3. Method and critique

From headline theorems to adjunctions to introduction etc rules for new logical connectives to the new theory and its computational interpretation. Critique of the Euclid–Bourbaki style and of the traditional category of “topological spaces”, here called “Bourbaki spaces”.


4. Stone duality

The duality between algebra and geometry. Locale theory.


5. Always topologize

Expressing Stone duality using lambda-calculus and a monad. Beck’s theorem; Sigma-split subspaces and their applications.


6. The monadic framework

Categorical and type-theoretic formulation of Stone duality in this abstract form. Primes, sobriety, nuclei.


7. The Sierpinski space

Classifiers for subsets, open subspaces and closed subspaces. The Euclidean and Phoa principles.


8. Topology using the Phoa principle

Development of the lambda calculus for topology including the lattice structure and Euclidean or Phoa principles. The Euclidean principle makes Sigma a dominance. Discrete, Hausdorff, compact and overt spaces. Partial map classifier.


9. Discrete mathematics

Pretoposes and arithmetic universes. Overt discrete spaces as sets. Recursion, induction and the need for equalisers. ASD-style characterisation of elementary toposes. General recursion (minimalisation).


10. Underlying sets

The (non-computable) underlying set axiom. Overt discrete spaces form a topos. Comparing the monads.


11. Scott continuity

Formulations of Scott continuity in denotational semantics, elementary real analysis and locale theory. Characterisation and properties of locally compact spaces. Application to real analysis.


12. Beyond local compactness

This section has been completely rewritten, but is currently available only in the PDF, DVI and PS versions above; the HTML version of the old text has been removed.


Bibliography

This document was translated from LATEX by HEVEA.