home | mathematics | formal topology | origins

Formal Topology: origins

Formal topology began in the 80s as an intuitionistic, predicative and purely pointfree approach to topology.

Its historical roots can be traced mainly to Brouwer conception of the continuum, which was expressed in terms of choice sequences, and to pointfree geometry (Pieri, Whitehead,...) and topology (Menger, Grothendieck, Isbell, Banaschewski, Johnstone,...).

A precursor is Martin-Löf's book Notes on constructive mathematics, 1970. Other influential sources were Fourman-Grayson's formal spaces (1981) and Scott's presentation of domains via information systems (1982).

To this tradition, which is partly in common with the present impredicative theory of locales, formal topology adds the requirement of a predicative treatment. In practice, this means that it is developed over Martin-Löf type theory.

In the 90s the landscape has gradually become wider (see developments below) and the predicative nature has brought to some unexpected mathematical insights: even the right approach to the notion of a closed subset needs a conceptually new approach, where `closed' is not the complement of 'open'. Moreover, a deeper analysis has led to take into account also the situations in which points are present. See The Basic Picture ::...