# Arithmetic universes as generalized point-free spaces

## 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)

Contact | ishihara@jaist.ac.jp |
---|