Prof. Giovanni Sambin at NII Logic Seminar
Date: March 23, 2015, 13:30--15:30
Place: National Institute of Informatics, Room 1716 (17th floor) 場所: 国立情報学研究所 17階 1716室 (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/)
Speaker: Prof. Giovanni Sambin (University of Padova)
Title: Realizability interpretation of topology
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 S of 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 (a in 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.
問合せ先: 龍田 真 (国立情報学研究所) e-mail: tatsuta@nii.ac.jp http://research.nii.ac.jp/~tatsuta