|
Abstract
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 This paper is due to appear in Foundational Theories of Classical and Constructive Mathematics, edited by Giovanni Sommaruga, whose emphasis is on philosophy rather than technicalities. I would like to thank Andrej Bauer, David Corfield, Gabor Lukasz, Pino Rosolini, Giovanni Sommaruga, and Graham White for their very helpful comments on earlier drafts of this paper. |
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 is www.PaulTaylor.EU/ASD/foufct/index.html and it was derived from ASD/foufct.tex which was last modified on 9 March 2009.