Abstract
Foundations should be designed for the needs of mathematics and not vice versa. We propose a technique for doing this using the correspondence between category theory and logic and is potentially applicable to several mathematical disciplines.
“In these days the angel of topology and the devil of abstract algebra fight for the soul of every individual discipline of mathematics.” (Hermann Weyl.)
“Point-set topology is a disease from which the human race will soon recover.” (Henri Poincaré)
“Logic is the hygiene that the mathematician practises to keep his ideas healthy and strong.” (Hermann Weyl)
“Mathematics is the queen of the sciences and number theory is the queen of mathematics.” (Carl Friedrich Gauss)
“Such is the advantage of a well constructed language that its simplified notation often becomes the source of profound theories.” (Pierre-Simon Laplace)
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Appel, A. (1992) Compiling with Continuations, Cambridge: Cambridge University Press.
Barr, M. and Wells, C. (1985) Toposes, Triples and Theories, New York: Springer.
Bauer, A. (2008) Efficient Computation with Dedekind Reals, in Brattka, V., Dillhage, R., Grubba, T. and Klutch, A., eds. Fifth International Conference on Computability and Complexity in Analysis, in volume 221 of Electronic Notes in Theoretical Computer Science, Amsterdam: Elsevier.
Bauer, A., Birkedal, L. and Scott, D. (2004) Equilogical Spaces, Theoretical Computer Science 315, 35–59.
Bishop, E. and Bridges, D. (1985) Constructive Analysis, Number 279 in Grundlehren der mathematischen Wissenschaften, Heidelberg, Berlin, New York: Springer.
Bourbaki, N. (1966) Topologie Générale, Paris: Hermann, English translation, “General Topology” Berlin: Springer (1989).
Bridges, D. and Richman, F. (1987) Varieties of Constructive Mathematics, Number 97 in London Mathematical Society Lecture Notes, Cambridge: Cambridge University Press.
Brown, R. (1964) Function Spaces and Product Topologies, Quarterly Journal of Mathematics 15(1), 238–250.
Carboni, A., Lack, S. and Walters, R. (1993) Introduction to Extensive and Distributive Categories, Journal of Pure and Applied Algebra 84, 145–158.
Cardone, F. and Hindley, R. (2006) History of Lambda-Calculus and Combinatory Logic, Handbook of the History of Logic 5.
Church, A. and Rosser, B. (1936) Some Properties of Conversion, Transactions of the American Mathematical Society 39(3), 472–482.
Cleary, J. (1987) Logical Arithmetic, Future Computing Systems 2, 125–149.
Cockett, R. (1993) Introduction to Distributive Categories, Mathematical Structures in Computer Science 3, 277–307.
Corfield, D. (2003) Towards a Philosophy of Real Mathematics, Cambridge: Cambridge University Press.
Eilenberg, S. and Moore, J. (1965) Adjoint Functors and Triples, Illinois Journal of Mathematics 9, 381–98.
Fauvel, J. and Gray, J. (1987) The History of Mathematics, a Reader, London: Macmillan, Open University.
Fourman, M. and Hyland, M. (1979) Sheaf Models for Analysis, in Fourman, M., Mulvey, C. and Scott, D., eds. Applications of Sheaves, number 753 in Lecture Notes in Mathematics, Berlin, New York: Springer, pp. 280–301
Fox, R. (1945) On Topologies for Function-Spaces, Bulletin of the American Mathematical Society 51.
Gentzen, G. (1935) Untersuchungen über das logische Schliessen, Mathematische Zeitschrift 39, 176–210, 405–431, English translation, pages 68–131 in The Collected Papers of Gerhard Gentzen, edited by Manfred E. Szabo, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland.
Gierz, G., Hofmann, K., Keimel, K., Lawson, J., Mislove, M. and Scott, D. (1980) A Compendium of Continuous Lattices, Berlin, Heidelberg, New York: Springer, second edition, Continuous Lattices and Domains, Cambridge: Cambridge University Press (2003).
Girard, J.-Y. (1987) Linear Logic, Theoretical Computer Science 50, 1–102.
Hartshorne, R. (1977) Algebraic Geometry, Number 52 in Graduate Texts in Mathematics, Berlin, New York: Springer.
Hofmann, K. and Mislove, M. (1981) Local Compactness and Continuous Lattices, in Banaschewski, B. and Hoffmann, R.-E., eds. Continuous Lattices, number 871 in Lecture Notes in Mathematics, Berlin: Springer, pp. 209–248.
Howard, W. (1980) The Formulae-as-Types Notion of Construction, in Curry, H., Seldin, J. and Hindley, R., eds. To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, New York: Academic Press, pp. 479–490.
Hudak, P. (1989) Conception, Evolution and Application of Functional Programming Languages, ACM Computing Surveys 21, 355–411.
Hudak, P., Hughes, J., Peyton-Jones, S. and Wadler, P. (2007) A History of Haskell: Being Lazy with Class, in History of Programming Languages, New York: ACM Press, pp. 12–55.
Hyland, M. (1991) First Steps in Synthetic Domain Theory, in Carboni, A., Pedicchio, M.-C. and Rosolini, G., eds. Proceedings of the 1990 Como Category Conference, number 1488 in Lecture Notes in Mathematics, Berlin, Heidelberg, New York: Springer, pp. 131–156.
Isbell, J. (1986) General Function Spaces, Products and Continuous Lattices, Mathematical Proceedings of the Cambridge Philosophical Society 100, 193–205.
Johnstone, P.(1982) Stone Spaces, Number 3 in Cambridge Studies in Advanced Mathematics, Cambridge: Cambridge University Press.
Johnstone, P. (1984) Open Locales and Exponentiation, Contemporary Mathematics 30, 84–116.
Joyal, A. and Tierney, M. (1984) An Extension of the Galois Theory of Grothendieck, Memoirs of the American Mathematical Society 51(309).
Jung, A., Kegelmann, M. and Moshier, A. (2001) Stably Compact Spaces and Closed Relations, Electronic Notes in Theoretical Computer Science 45.
Kock, A. (1981) Synthetic Differential Geometry, Number 51 in London Mathematical Society Lecture Notes, Cambridge: Cambridge University Press, second edition, number 333 (2006).
Kuhn, T. (1962) The Structure of Scientific Revolutions, Chicago: University of Chicago Press.
Lakatos, I. (1963) Proofs and Refutations: The Logic of Mathematical Discovery, British Journal for the Philosophy of Science 14, 1–25, re-published by Cambridge University Press (1976), edited by John Worrall and Elie Zahar.
Lawvere, B. (1969) Adjointness in Foundations, Dialectica 23, 281–296, Reprinted with commentary in Theory and Applications of Categories Reprints 16 (2006), 1–16.
Linton, F. (1969) An Outline of Functorial Semantics, in Eckmann, B., ed. Seminar on Triples and Categorical Homology Theory, number 80 in Lecture Notes in Mathematics, Berlin, Heidelberg, New York: Springer, pp. 7–52.
Mac Lane, S. (1963) Natural Associativity and Commutativity, Rice University Studies 49, 28–46.
Mac Lane, S. (1971) Categories for the Working Mathematician, Berlin, Heidelberg and New York: Springer.
Mac Lane, S. (1988) Categories and Concepts in Perspective, in Duren, P., Askey, R. and Merzbach, U., eds. A Century of Mathematics in America, vol. 1, pp. 323–365, Providence, RI: American Mathematical Society. Addendum in vol. 3, pp. 439–441.
Manes, E. (1976) Algebraic Theories, Number 26 in Graduate Texts in Mathematics, Berlin, Heidelberg, New York: Springer.
McLarty, C. (1990) The Uses and Abuses of the History of Topos Theory, British Journal for the Philosophy of Science 41, 351–375.
Mikkelsen, C. (1976) Lattice-Theoretic and Logical Aspects of Elementary Topoi, PhD thesis, Århus: Århus Universitet, Various publications, number 25.
Moore, R. (1966) Interval Analysis, Automatic Computation, Englewood Cliff, NJ: Prentice Hall, second edition, Introduction to Interval Analysis, with Baker Kearfott and Michael Cloud, Society for Industrial and Applied Mathematics (2009).
Paré, R. (1974) Colimits in Topoi, Bulletin of the American Mathematical Society 80(3), 556–561.
Phoa, W. (1990) Domain Theory in Realizability Toposes, PhD thesis, Cambridge: University of Cambridge. University of Edinburgh Dept. of Computer Science report CST-82-91 and ECS-LFCS-91-171.
Pitts, A. (2001) Categorical Logic, in Handbook of Logic in Computer Science, vol. 5, Oxford: Oxford University Press.
Rosolini, G. (1986) Continuity and Effectiveness in Topoi, D. Phil. thesis, Oxford: University of Oxford.
Russell, B. and Whitehead, A.N. (1910–1913) Principia Mathematica, Cambridge: Cambridge University Press.
Scott, D. (1972) Continuous Lattices, in Lawvere, F.W., ed. Toposes, Algebraic Geometry and Logic, number 274 in Lecture Notes in Mathematics, Berlin, Heidelberg, New York: Springer, pp. 97–136.
Scott, D. (1993) A Type-Theoretical Alternative to ISWIM, CUCH, OWHY, Theoretical Computer Science 121, 422–440. Written in 1969.
Seldin, J. (2002) Curry’s Anticipation of the Types Used in Programming Languages, Proceedings of the Canadian Society for History and Philosophy of Mathematics 15, 148–163.
Simmons, H. (1978) The Lattice-Theoretic Part of Topological Separation Properties, Proceedings of the Edinburgh Mathematical Society (2) 21, 41–48.
Smolin, L. (2006) The Trouble with Physics, New York: Houghton Mifflin, republished by Penguin (2008).
Spitters, B. (2010) Located and overt sublocales, to appear in Annals of Pure and Applied Logic, 162, 36–54.
Steenrod, N. (1967) A Convenient Category of Topological Spaces, Michigan Mathematics Journal 14, 133–152.
Stone, M. (1937) Applications of the Theory of Boolean Rings to General Topology, Transactions of the American Mathematical Society 41, 375–481.
Stone, M. (1938) The Representation of Boolean Algebras, Bulletin of the American Mathematical Society 44, 807–816.
Tarski, A. (1935) Zur Grundlegung der Boole’schen Algebra, Fundamenta Mathematicae 24, 177–198.
Taylor, P. (1999) Practical Foundations of Mathematics, Number 59 in Cambridge Studies in Advanced Mathematics, Cambridge: Cambridge University Press.
Thielecke, H. (1997) Categorical Structure of Continuation Passing Style, PhD thesis, Edinburgh: University of Edinburgh.
Vermeulen, J. (1994) Proper Maps of Locales, Journal of Pure and Applied Algebra 92, 79–107.
Vickers, S. (1988) Topology Via Logic, volume 5 of Cambridge Tracts in Theoretical Computer Science, Cambridge: Cambridge University Press.
Wilker, P. (1970) Adjoint Product and Hom Functors in General Topology, Pacific Journal of Mathematics 34, 269–283.
Paul Taylor’s papers on the Abstract Stone Duality programme, including the extended version of this one, are available from www.paultaylor.eu/asd/
Taylor, P. (2000a) Geometric and Higher-Order Logic in Terms of Abstract Stone Duality, Theory and Applications of Categories 7, 284–338.
Taylor, P. (2000b) Non-Artin Gluing in Recursion Theory and Lifting in Abstract Stone Duality.
Taylor, P. (2002a) Sober Spaces and Continuations, Theory and Applications of Categories 10, 248–299.
Taylor, P. (2002b) Subspaces in Abstract Stone Duality, Theory and Applications of Categories 10, 300–366.
Taylor, P. (2002c) Scott Domains in Abstract Stone Duality, http://www.paultaylor.eu/asd/pcfasd.pdf
Taylor, P. (2004a) An Elementary Theory of Various Categories of Spaces and Locales.
Taylor, P. (2004b) Tychonov’s Theorem in Abstract Stone Duality.
Taylor, P. (2005) Inside Every Model of Abstract Stone Duality Lies an Arithmetic Universe, Electronic Notes in Theoretical Computer Science 122, 247–296.
Taylor, P. (2006a) Computably Based Locally Compact Spaces, Logical Methods in Computer Science 2, 1–70.
Taylor, P. (2006b) Interval Analysis Without Intervals, Real Numbers and Computers.
Taylor, P. (2009a) With Andrej Bauer, The Dedekind Reals in Abstract Stone Duality, Mathematical Structures in Computer Science 19, 757–838.
Taylor, P. (2009b) Equideductive Categories and Their Logic.
Taylor, P. (2010a) A lambda Calculus for Real Analysis, Journal of Logic and Analysis 2(5), 1–115.
Taylor, P. (2010b) Computability for Locally Compact Spaces.
Acknowledgements
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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer Science+Business Media B.V.
About this chapter
Cite this chapter
Taylor, P. (2011). Foundations for Computable Topology. In: Sommaruga, G. (eds) Foundational Theories of Classical and Constructive Mathematics. The Western Ontario Series in Philosophy of Science, vol 76. Springer, Dordrecht. https://doi.org/10.1007/978-94-007-0431-2_14
Download citation
DOI: https://doi.org/10.1007/978-94-007-0431-2_14
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-007-0430-5
Online ISBN: 978-94-007-0431-2
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)