Arithmetic universes as generalized point-free spaces

• Steve Vickers

• University of Birmingham

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)