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