Foundations for Computable Topology

Paul Taylor

Abstract: Foundations should be designed for the needs of mathematics and not vice versa. We propose a technique for doing this that exploits the correspondence between category theory and logic and is potentially applicable to several mathematical disciplines.

This method is applied to devising a new paradigm for general topology, called Abstract Stone Duality. We express the duality between algebra and geometry as an abstract monadic adjunction that we turn into a new type theory. To this we add an equation that is satisfied by the Sierpiński space, which plays a key role as the classifier for both open and closed subspaces.

In the resulting theory there is a duality between open and closed concepts. This captures many basic properties of compact and closed subspaces, despite the absence of any explicitly infinitary axiom. It offers dual results that link general topology to recursion theory.

The extensions and applications of ASD elsewhere that this paper surveys include a purely recursive theory of elementary real analysis in which, unlike in previous approaches, the real closed interval [0,1] in ASD is compact.

“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é, quoted in Comic Sections by Des MacHale.)

“Logic is the hygiene that the mathematician practises
to keep his ideas healthy and strong.”
(Hermann Weyl, quoted in American Mathematical Monthly,
volume 100, p 93.)

“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, quoted in Mathematical Maxims and Minims
by N. Rose, Raleigh Rome Press, 1988.)


This document was translated from LATEX by HEVEA.