Skip to main content

Foundations for Computable Topology

  • Chapter
  • First Online:

Part of the book series: The Western Ontario Series in Philosophy of Science ((WONS,volume 76))

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  • Appel, A. (1992) Compiling with Continuations, Cambridge: Cambridge University Press.

    Google Scholar 

  • Barr, M. and Wells, C. (1985) Toposes, Triples and Theories, New York: Springer.

    MATH  Google Scholar 

  • 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.

    Google Scholar 

  • Bauer, A., Birkedal, L. and Scott, D. (2004) Equilogical Spaces, Theoretical Computer Science 315, 35–59.

    Article  MathSciNet  MATH  Google Scholar 

  • Bishop, E. and Bridges, D. (1985) Constructive Analysis, Number 279 in Grundlehren der mathematischen Wissenschaften, Heidelberg, Berlin, New York: Springer.

    Book  MATH  Google Scholar 

  • Bourbaki, N. (1966) Topologie Générale, Paris: Hermann, English translation, “General Topology” Berlin: Springer (1989).

    Google Scholar 

  • Bridges, D. and Richman, F. (1987) Varieties of Constructive Mathematics, Number 97 in London Mathematical Society Lecture Notes, Cambridge: Cambridge University Press.

    Book  MATH  Google Scholar 

  • Brown, R. (1964) Function Spaces and Product Topologies, Quarterly Journal of Mathematics 15(1), 238–250.

    Article  MATH  Google Scholar 

  • Carboni, A., Lack, S. and Walters, R. (1993) Introduction to Extensive and Distributive Categories, Journal of Pure and Applied Algebra 84, 145–158.

    Article  MathSciNet  MATH  Google Scholar 

  • Cardone, F. and Hindley, R. (2006) History of Lambda-Calculus and Combinatory Logic, Handbook of the History of Logic 5.

    Google Scholar 

  • Church, A. and Rosser, B. (1936) Some Properties of Conversion, Transactions of the American Mathematical Society 39(3), 472–482.

    Article  MathSciNet  Google Scholar 

  • Cleary, J. (1987) Logical Arithmetic, Future Computing Systems 2, 125–149.

    Google Scholar 

  • Cockett, R. (1993) Introduction to Distributive Categories, Mathematical Structures in Computer Science 3, 277–307.

    Article  MathSciNet  MATH  Google Scholar 

  • Corfield, D. (2003) Towards a Philosophy of Real Mathematics, Cambridge: Cambridge University Press.

    Book  MATH  Google Scholar 

  • Eilenberg, S. and Moore, J. (1965) Adjoint Functors and Triples, Illinois Journal of Mathematics 9, 381–98.

    MathSciNet  MATH  Google Scholar 

  • Fauvel, J. and Gray, J. (1987) The History of Mathematics, a Reader, London: Macmillan, Open University.

    Google Scholar 

  • 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

    Chapter  Google Scholar 

  • Fox, R. (1945) On Topologies for Function-Spaces, Bulletin of the American Mathematical Society 51.

    Google Scholar 

  • 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.

    Article  MathSciNet  Google Scholar 

  • 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).

    Book  MATH  Google Scholar 

  • Girard, J.-Y. (1987) Linear Logic, Theoretical Computer Science 50, 1–102.

    Article  MathSciNet  MATH  Google Scholar 

  • Hartshorne, R. (1977) Algebraic Geometry, Number 52 in Graduate Texts in Mathematics, Berlin, New York: Springer.

    MATH  Google Scholar 

  • 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.

    Chapter  Google Scholar 

  • 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.

    Google Scholar 

  • Hudak, P. (1989) Conception, Evolution and Application of Functional Programming Languages, ACM Computing Surveys 21, 355–411.

    Article  Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • Isbell, J. (1986) General Function Spaces, Products and Continuous Lattices, Mathematical Proceedings of the Cambridge Philosophical Society 100, 193–205.

    Article  MathSciNet  MATH  Google Scholar 

  • Johnstone, P.(1982) Stone Spaces, Number 3 in Cambridge Studies in Advanced Mathematics, Cambridge: Cambridge University Press.

    MATH  Google Scholar 

  • Johnstone, P. (1984) Open Locales and Exponentiation, Contemporary Mathematics 30, 84–116.

    Article  MathSciNet  Google Scholar 

  • Joyal, A. and Tierney, M. (1984) An Extension of the Galois Theory of Grothendieck, Memoirs of the American Mathematical Society 51(309).

    Google Scholar 

  • Jung, A., Kegelmann, M. and Moshier, A. (2001) Stably Compact Spaces and Closed Relations, Electronic Notes in Theoretical Computer Science 45.

    Google Scholar 

  • Kock, A. (1981) Synthetic Differential Geometry, Number 51 in London Mathematical Society Lecture Notes, Cambridge: Cambridge University Press, second edition, number 333 (2006).

    MATH  Google Scholar 

  • Kuhn, T. (1962) The Structure of Scientific Revolutions, Chicago: University of Chicago Press.

    Google Scholar 

  • 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.

    Article  MathSciNet  Google Scholar 

  • Lawvere, B. (1969) Adjointness in Foundations, Dialectica 23, 281–296, Reprinted with commentary in Theory and Applications of Categories Reprints 16 (2006), 1–16.

    Article  MATH  Google Scholar 

  • 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.

    Chapter  Google Scholar 

  • Mac Lane, S. (1963) Natural Associativity and Commutativity, Rice University Studies 49, 28–46.

    MathSciNet  Google Scholar 

  • Mac Lane, S. (1971) Categories for the Working Mathematician, Berlin, Heidelberg and New York: Springer.

    Book  MATH  Google Scholar 

  • 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.

    Google Scholar 

  • Manes, E. (1976) Algebraic Theories, Number 26 in Graduate Texts in Mathematics, Berlin, Heidelberg, New York: Springer.

    Book  MATH  Google Scholar 

  • McLarty, C. (1990) The Uses and Abuses of the History of Topos Theory, British Journal for the Philosophy of Science 41, 351–375.

    Article  MathSciNet  MATH  Google Scholar 

  • Mikkelsen, C. (1976) Lattice-Theoretic and Logical Aspects of Elementary Topoi, PhD thesis, Århus: Århus Universitet, Various publications, number 25.

    Google Scholar 

  • 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).

    MATH  Google Scholar 

  • Paré, R. (1974) Colimits in Topoi, Bulletin of the American Mathematical Society 80(3), 556–561.

    Article  MathSciNet  MATH  Google Scholar 

  • 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.

    Google Scholar 

  • Pitts, A. (2001) Categorical Logic, in Handbook of Logic in Computer Science, vol. 5, Oxford: Oxford University Press.

    Google Scholar 

  • Rosolini, G. (1986) Continuity and Effectiveness in Topoi, D. Phil. thesis, Oxford: University of Oxford.

    Google Scholar 

  • Russell, B. and Whitehead, A.N. (1910–1913) Principia Mathematica, Cambridge: Cambridge University Press.

    MATH  Google Scholar 

  • 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.

    Chapter  Google Scholar 

  • Scott, D. (1993) A Type-Theoretical Alternative to ISWIM, CUCH, OWHY, Theoretical Computer Science 121, 422–440. Written in 1969.

    Article  Google Scholar 

  • 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.

    Google Scholar 

  • Simmons, H. (1978) The Lattice-Theoretic Part of Topological Separation Properties, Proceedings of the Edinburgh Mathematical Society (2) 21, 41–48.

    Article  MathSciNet  MATH  Google Scholar 

  • Smolin, L. (2006) The Trouble with Physics, New York: Houghton Mifflin, republished by Penguin (2008).

    MATH  Google Scholar 

  • Spitters, B. (2010) Located and overt sublocales, to appear in Annals of Pure and Applied Logic, 162, 36–54.

    Article  MathSciNet  MATH  Google Scholar 

  • Steenrod, N. (1967) A Convenient Category of Topological Spaces, Michigan Mathematics Journal 14, 133–152.

    Article  MathSciNet  MATH  Google Scholar 

  • Stone, M. (1937) Applications of the Theory of Boolean Rings to General Topology, Transactions of the American Mathematical Society 41, 375–481.

    Article  MathSciNet  Google Scholar 

  • Stone, M. (1938) The Representation of Boolean Algebras, Bulletin of the American Mathematical Society 44, 807–816.

    Article  MathSciNet  Google Scholar 

  • Tarski, A. (1935) Zur Grundlegung der Boole’schen Algebra, Fundamenta Mathematicae 24, 177–198.

    Google Scholar 

  • Taylor, P. (1999) Practical Foundations of Mathematics, Number 59 in Cambridge Studies in Advanced Mathematics, Cambridge: Cambridge University Press.

    MATH  Google Scholar 

  • Thielecke, H. (1997) Categorical Structure of Continuation Passing Style, PhD thesis, Edinburgh: University of Edinburgh.

    Google Scholar 

  • Vermeulen, J. (1994) Proper Maps of Locales, Journal of Pure and Applied Algebra 92, 79–107.

    Article  MathSciNet  MATH  Google Scholar 

  • Vickers, S. (1988) Topology Via Logic, volume 5 of Cambridge Tracts in Theoretical Computer Science, Cambridge: Cambridge University Press.

    Google Scholar 

  • Wilker, P. (1970) Adjoint Product and Hom Functors in General Topology, Pacific Journal of Mathematics 34, 269–283.

    Article  MathSciNet  MATH  Google Scholar 

  • 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.

    MathSciNet  MATH  Google Scholar 

  • Taylor, P. (2000b) Non-Artin Gluing in Recursion Theory and Lifting in Abstract Stone Duality.

    Google Scholar 

  • Taylor, P. (2002a) Sober Spaces and Continuations, Theory and Applications of Categories 10, 248–299.

    MathSciNet  MATH  Google Scholar 

  • Taylor, P. (2002b) Subspaces in Abstract Stone Duality, Theory and Applications of Categories 10, 300–366.

    Google Scholar 

  • 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.

    Google Scholar 

  • Taylor, P. (2004b) Tychonov’s Theorem in Abstract Stone Duality.

    Google Scholar 

  • Taylor, P. (2005) Inside Every Model of Abstract Stone Duality Lies an Arithmetic Universe, Electronic Notes in Theoretical Computer Science 122, 247–296.

    Article  Google Scholar 

  • Taylor, P. (2006a) Computably Based Locally Compact Spaces, Logical Methods in Computer Science 2, 1–70.

    Article  Google Scholar 

  • Taylor, P. (2006b) Interval Analysis Without Intervals, Real Numbers and Computers.

    Google Scholar 

  • Taylor, P. (2009a) With Andrej Bauer, The Dedekind Reals in Abstract Stone Duality, Mathematical Structures in Computer Science 19, 757–838.

    Article  MATH  Google Scholar 

  • Taylor, P. (2009b) Equideductive Categories and Their Logic.

    Google Scholar 

  • Taylor, P. (2010a) A lambda Calculus for Real Analysis, Journal of Logic and Analysis 2(5), 1–115.

    Google Scholar 

  • Taylor, P. (2010b) Computability for Locally Compact Spaces.

    Google Scholar 

Download references

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

Authors

Corresponding author

Correspondence to Paul Taylor .

Editor information

Editors and Affiliations

Rights and permissions

Reprints 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

Publish with us

Policies and ethics