3rd Workshop on Formal Topology

What is 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.

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 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".