home | mathematics | formal topology | some developments ::... 1 | 2

Formal Topology: some developments

Formal topology has become an essential tool for constructive mathematics. In particular, its predicative character is exactly what is needed to preserve the computational interpretation of mathematics (as in formal topologies) and yet connect it with infinitary notions (as in formal spaces).

Using formal topology, or ideas inspired by it, constructive treatment of several classical results have been obtained: it often happens that this is accompanied by a conceptual simplification and an increase in understanding.

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 proof theory and recursion theory) and mathematics (especially category theory and locale theory).

More in detail, some of the developments based on formal topology and some of the topics connected with it are:

- Formal topologies provide a complete semantics for intuitionistic (linear) logic: Pretopologies and completeness proofs contains a predicative and uniform proof, Formal topologies on the set of first order formulae contains a characterization of Henkin sets (that is, models) as formal points.

- Domain theory can be seen as included in formal topology: see Constructive domain theory as a branch... and Formal topology and domains.