Event News

Prof. Giovanni Sambin at NII Logic Seminar


Monday 23 March, 2015
Room Room 1716 (17th floor), National Institute of Informatics
Realizability interpretation of topology
Prof. Giovanni Sambin (University of Padova)
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.

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