home | mathematics | formal topology | introduction

Formal Topology: introduction

It often happens that the structure of open subsets 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.

This is the idea of formal topology in general. 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. All this appeared for the first time in my 1987 paper Intuitionistic formal spaces.

A more general notion of formal topology has been introduced in the context of the basic picture.

In Some points one can find a short review (updated 2001) of formal topology, an introduction to the basic picture and a discussion on constructive mathematics (see also philosophy).