EVENT

Prof. Giovanni Sambin at NII Logic Seminar

Outline

Date:

Monday 23 March, 2015

Time:

13:30-15:30

Place:

Room Room 1716 (17th floor), National Institute of Informatics
Access

Title:

Realizability interpretation of topology

Speaker:

Prof. Giovanni Sambin (University of Padova)

Abstract:

It is a fact of life that the classical notion of topological space can be obtained in a constructive (intuitionistic and predicative) way by starting from neighbourhoods and defining points as specific subsets of neighbourhoods. Beginning in the 80s, we introduced what is now called formal topology: a predicative and intuitionistic pointfree approach to topology. The key ingredient of a formal topology is a relation, called cover, between elements and subsets of a given set Sof formal neighbourhoods, or observables. In the 90s, we showed that the cover relation of formal topologies can be generated by induction. Given a set of observables S, a family of sets I(a) set (ain S) and a family C(a,i) of subsets of S, for a in S and i in I(a), one can generate by induction the least cover such that every C(a,i) is a cover of a. We call this an axiom-set. Soon after, I also added a positivity relation, again between elements and subsets of S, which provides a way to introduce closed subsets in a pointfree way. We showed that positivity relations can be generated coinductively from an axiom-set. It turns out that generation, by induction and by coinduction, from axiom-sets is the only postulate over a very elementary foundation, which have been shown to admit a realizability interpretation. So to obtain a realizability interpretation of constructive topology one only need to find a realizability interpretation for the principle of generation from axiom-sets.

Contact

National Institute of Informatics
Prof. Makoto Tatsuta E-mail: tatsuta[at]nii.ac.jp
*Please replace [at] with @.