New paper "Sketches for arithmetic universes"

New paper "Sketches for arithmetic universes"

[Steve Vickers]

Some of you may have heard talks about my paper "Sketches for arithmetic uni=
verses", or even seen preliminary drafts of it. I now have a version which I=
  intend to submit shortly, and have put it on my website at

   http://www.cs.bham.ac.uk/~sjv/AUSk.pdf

I've also sent it to arXiv.

The paper is intended to help deal with a problem with geometric logic, name=
ly that it has infinities in its formalism (specifically: infinitary disjunc=
tions) that are extrinsic to the logic itself and supplied by choosing a bas=
e topos.

In practice, many of the infinities needed are countable and are not sensiti=
ve to change of base as long as the base has a natural numbers object. The a=
im of this work is to make those infinities intrinsic to the logic by adding=
  type-theoretic ingredients (specifically, list objects, hence in particular=
  nnos) that enable infinite disjunctions to be replaced by existential quant=
ification. Categorically this amounts to replacing Grothendieck toposes (ove=
r base with nno) by arithmetic universes (no base needed) - that is to say, b=
y pretoposes with parametrized list objects. Already, Milly Maietti has stud=
ied some type-theoretic issues for these.

The paper describes "contexts", finite gadgets analogous to sketches that pl=
ay the role of geometric theories, and their classifying AUs, replacing clas=
sifying toposes as generalized spaces. Maps and 2-cells for contexts are als=
o finite gadgets. The 2-category of contexts embeds fully and faithfully in t=
he 2-category of AUs, strict AU-functors, and natural transformations.

Steve=


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]