皆様
Padova大学のFrancesco Ciraulo先生の講演のお知らせです。 どうぞふるってご参加ください。
河井 達治 北陸先端科学技術大学院大学 情報科学系 e-mail: [email protected] ----------------------------------------------- * JAIST Logic Seminar Series *
* The seminar below is held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks and EU Horizon 2020 Marie Skłodowska-Curie actions RISE project CID (http://www.jaist.ac.jp/logic/ja/core2core, http://cid.uni-trier.de/).
Date: Wednesday 31st July, 2019, 15:20-17:00 Place: JAIST, Collaboration room 6 (I-57g) (https://www.jaist.ac.jp/english/top/access/index.html)
Speaker: Francesco Ciraulo (University of Padova)
Title: Overlap algebras: a constructive alternative to complete Boolean algebras
Abstract: Although (complete) Boolean algebras does exist in a constructive framework, they fail to capture very basic examples, such as powersets. Constructively, the subsets of a given set form a complete Heyting algebra (locale), but one of a very special kind: it is an “overlap algebra”. The definition of an overlap algebra, as proposed by Giovanni Sambin some years ago, collapses to that of a complete Boolean algebra (Boolean locale) if the Principle of Excluded Middle (PEM) holds. Overlap algebras can be useful to obtain constructive versions of classical results about complete Boolean algebras. For instance, the regular open sets in a topological space form an overlap algebra. More generally, the smallest strongly dense sublocale of an overt locale is an overlap algebra. (The latter is a version of Isbell’s density theorem.) The sublocales of an overlap algebra have not been completely understood yet (contrary to the case of Boolean locales). At the moment we only know that the open sublocales of a given overlap algebra L are overlap algebras, and that there is a bijection between those sublocales of L which are overlap algebras, on one side, and the overt weakly closed sublocales of L (i.e. the points of its lower-powerlocale), on the other side. The internal locales in the topos of sheaves over a given locale L correspond to morphisms with codomain L in the (external) category of locales. In particular, internal overt locales correspond to open maps. Since overlap algebras are a special class of overt locales, it should be possible to identify internal overlap algebras in a localic topos as a special class of open maps. The ultimate goal would be to exploit the fact that a locale which is not an overlap algebra can “become” an overlap algebra internally in many Grothendieck toposes.