home » formal topology

The structure of opens can be given quite constructively, even when the
corresponding points have an infinitary description. Typical is the case
of real numbers: points are infinite sequences, while open subsets can
be given starting from intervals with rational endpoints. Then the idea
is that one can begin without real numbers: one defines the topology by
giving open subsets and their coverings primitively, rather than by quantifying
on points.

A formal topology is a set of formal basic neighbourhoods equipped with
an abstract cover relation and with a positivity predicate. Points are
then defined formally in terms of opens: this is the so-called pointfree
approach to topology.

The collection of formal points is called formal space. The move from
a formal topology to formal points is common in all of mathematics: choice
sequences, real numbers, the spectrum of a ring, Stone representations,
Scott domains,... are all formal spaces on some formal topology.

Also the notion of continuity of functions between formal spaces is reduced
to pointfree terms, that is to the notion of morphism of formal topologies.

A recent deveolpment is the **Basic Picture**, a deep structure
by which the symmetries and logical dualities underlying the topological
notions of open, closed, continuity are made explicit.

Duality extends also to pointfree notions, the cover being accompanied
by its dual, a positivity relation, which describes closed subsets in
formal terms and which can be generated by co-induction.

Formal topology has become an essential tool for constructive mathematics.
Its strongly constructive character permits to preserve the computational
interpretation of mathematics (formal topologies) and yet connect it with
infinitary notions (formal spaces).

Formal topology integrates techniques from:

- computer science, as in the notion of inductively, co-inductively generated formal topology;
- logic, both in the sense of foundational correctness, and by incorporating some techniques from recursion theory and proof theory, in particular the notion of inductive definitions;
- mathematics, especially category theory and locale theory.

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 constructive
type theory.

In the 90s the landscape has gradually become wider 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".