[kisoron-ml] Prof. Giovanni Sambin at NII Logic Seminar

[Makoto Tatsuta]

	      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 at nii.ac.jp
http://research.nii.ac.jp/~tatsuta