Erik Palmgren
University of Uppsala

"From intuitionistic to point-free topology"

Abstract:

Brouwer incorporated the Heine-Borel theorem into intuitionism by developing new mathematical axioms for choice sequences that are not fully compatible with a computational interpretation of logic. From these axioms topology could then be developed following the lines of the classical point-based theory. For lack of clear computational content these axioms were abandoned in the later development of constructive mathematics by the followers of Errett Bishop. Bishop considered the basic notion of map in topology to be a uniformly continuous function, other maps being locally of this kind. This move sidesteps the Heine-Borel theorem. However it lead to a restriction of topology to essentially metric spaces.

A parallel development lead to locale theory, in which a point is considered as a derived concept of the topology, while the notion of open cover is basic. This made it possible to naturally extend the notion of being "locally uniformly continuous" to general maps between topological spaces. In the PhD-thesis of Per Martin-L"of (1968) a point-free theory of the Cantor space is seen as a way of eliminating Brouwer's choice sequences. We show how the theory of Bishop and the point-free theory can be reconciled.

The foundational problems of point-free topology are interesting from a predicativistic point of view, and have been addressed by many researcher's since the mid 1980s. For a full formalisation of topology in various proof support systems, based on constructive type theories, these issues seem necessary to resolve. We present some recent developments in this area.

Back to Talks Page