[logic-ml] JAIST Logic Seminar Series

[Tatsuji Kawai]

皆様

Padova大学のFrancesco Ciraulo先生の講演のお知らせです。
どうぞふるってご参加ください。

河井 達治
北陸先端科学技術大学院大学 情報科学系
e-mail: tkawai at jaist.ac.jp
-----------------------------------------------
* 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.