[logic-ml] JAIST Logic Seminar Series

[Hajime Ishihara]

皆様

バーミンガム大学のSteve Vickers先生の講演のお知らせです。
どうぞふるってご参加ください。

問合せ先：
石原　哉
北陸先端科学技術大学院大学 情報科学系
e-mail: ishihara 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, EU FP7 Marie Curie Actions IRSES project 
CORCON.
(http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/), and EU 
Horizon 2020
Marie Skłodowska-Curie actions RISE project CID.

Date: Monday 17, April, 2017, 15:20-17:00

Place: JAIST, Collaboration room 6 (I-57g)
(Access: http://www.jaist.ac.jp/english/location/access.html)

Speaker: Steve Vickers (University of Birmingham)

Title: Arithmetic universes as generalized point-free spaces

Abstract:
Point-free topology in all its guises (e.g. locales, formal topology) 
can be understood as presenting a space as a _logical theory_, for which 
the points are the models and the opens are the formulae. The logic in 
question is geometric logic, its connectives being finite conjunctions 
and arbitrary disjunctions, and then the Lindenbaum algebra (formulae 
modulo equivalence) for a theory T is a frame O[T], a complete lattice 
with binary meet distributing over all joins. Locales are frames but 
with the morphisms reversed.

Grothendieck proposed Grothendieck toposes as the generalized point-free 
spaces got when one moves to the first-order form of geometric logic. 
Then the opens (giving truth values for each point) are not enough, and 
one must move to sheaves (giving sets for each point). The Lindenbaum 
algebra now becomes a Grothendieck topos Set[T], the classifying topos 
for T, constructed using presheaves with a pasting condition, and closed 
under finite limits and arbitrary colimits in accordance with Giraud's 
theorem. The topos Set[T] canonically represents the generalized space 
of models of T.

Grothendieck used the category Set of classical sets, but we now know 
that it can be replaced by any elementary topos S. This base will 
determine the infinities available for "arbitrary" disjunctions, as well 
as governing the construction of the classifier S[T]. However, for 
theories in which all the disjunctions are countable (such as the formal 
space of reals) it doesn't matter which S is used, as long as it has a 
natural numbers object (nno). Thus the generalized space of models of T 
is not absolutely fixed as a mathematical object.

In my talk I shall present the idea of using Joyal's _arithmetic 
universes_ (AUs), pretoposes with parameterized list objects, as a 
base-independent substitute for Grothendieck toposes in which countable 
disjunctions are intrinsic to the logic rather than being supplied 
extrinsically by a base S. In [1] I have defined a 2-category Con whose 
objects ("contexts") serve as geometric theories that are sufficiently 
countable in nature, and whose morphisms are the maps of models. In [2] 
I showed how to use Con to prove results for Grothendieck toposes, 
fibred over choice of base topos. Thus we start to see AUs providing a 
free-standing foundations for a significant fragment of geometric logic 
and Grothendieck toposes, independent of base S.

My two papers -
[1] "Sketches for arithmetic universes" (arXiv:1608.01559)
[2] "Arithmetic universes and classifying toposes" (arXiv:1701.04611)