Mathematical Logic in Padua

Research areas

Formal topology

Formal Topology began in the 80s as a constructive, predicative and purely point-free approach to topology enjoying the specific feature of being entirely carried out within (Martin-Löf's) Type Theory. Its origins can be traced mainly to Brouwer conception of the continuum, Locale Theory and Domain Theory (plus a consistent influence of constructive analysis from Martin-Löf's work in the subject).

In the 90s the landscape has gradually become wider and a deeper understanding has led to take into account also the situations in which points are present (see The Basic Picture below).

Nowadays what we collect under the name of Formal Topology comprises various kind of themes, and may be seen as a predicative formulation of topology that 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).

The particularly natural way in which this variety of aspects co-exists in Formal Topology makes the approach at the same time coherent and flexible, and gives hopes for a rich development.

Current researches in Formal Topology cover the connection with the study of topology in computer science, the development of topology and analysis (and mathematics in general) within type theories (as foundations and as programming languages), as well as the interactions with other foundational theories (Topos Theory, Aczel's constructive set theory,...).

The notion of Formal Topology

In formal topology the notion of open subset is given primitively. A formal topology is then a set of formal basic neighbourhoods equipped with an abstract cover relation and a positivity predicate.

Points are then defined formally in terms of opens, like in the so-called pointfree topology. The collection of formal points is called formal space.

Also the notion of continuity of functions between formal spaces is reduced to pointfree terms, that is to the notion of morphisms of formal topologies. All this appeared, for the first time, in Intuitionistic formal spaces - a first communication by G. Sambin.

A more general notion of formal topology has been subsequently introduced, based (again on an abstract cover relation and) on a binary positivity predicate allowing for a constructive pointfree theory of closed subsets.

This more general definition, together with an updated discussion on formal topology and the basic picture will be in G. Sambin: Some points in formal topology.

Some developments based on formal topology, or connected with it:

• Formal topologies provide a complete semantics for intuitionistic (linear) logic.
  Pretopologies and completeness proofs by G. Sambin contains a predicative and uniform proof.
  They can also be used to characterize Henkin sets as formal points (this can be found, among other things, in Formal topologies on the set of first order formulae by T. Coquand - S. Sadocco - G. Sambin - J. Smith).
  
  
• Domain theory (see Intuitionistic formal spaces vs. Scott domains by G. Sambin, Constructive domain theory as a branch of intuitionistic pointfree topology by G. Sambin - S. Valentini - P. Virgili.
  Concerning quantitative domain theory, see Formal topologies with weight and distance by G. Curi.
  
  
• Constructive proofs of classical results (see A constructive proof of the Heine-Borel covering theorem for formal reals by J. Cederquist and S. Negri, Tychonoff's theorem in the framework of formal topologies by S. Negri and S. Valentini, The Hahn-Banach Theorem in Type Theory by J. Cederquist - T. Coquand - S. Negri).
  
  
• Real numbers (see Numeri reali e analisi costruttiva nel contesto delle topologie formali, laurea thesis by D. Soravia, The continuum as a formal space by S. Negri and D. Soravia).
  
  
• Inductive definitions (see Inductively generated formal topologies by Th. Coquand - G. Sambin - J.Smith - S. Valentini).
  
  
• A constructive definition of metrizability for point-free topology and a pointfree axiomatization of metric spaces (in a work by G. Curi to appear).

Other available papers can be found in the homepages of G. Curi, S. Gebellato, G. Sambin, S. Valentini.

Another active research group on formal topology, is in Göteborg, where the leader is Thierry Coquand.

The First Workshop on Formal Topology has been held in Padova, October 2 - 4, 1997.

The Second Workshop on Formal Topology will be held in Venice, 4-6 April 2002.