The universal property of a (strong) natural number object in any
category with products delivers into the setting all the primitive
recursive functions. It has proven difficult to obtain - in a
reasonable categorical fashion - settings which have an arithmetic
power below primitive recursive. However, such settings are emerging
(notable Jim Otto in his PhD thesis provided a number of examples).
The purpose of this talk is to argue that finitistic universes, that
is extensive categories with an internal full subcategory of finite
sets, seem to provide a natural setting in which to express
subrecursive arithmetics. The talk will explore some of the properties
of these settings and describe how one may add arithmetic ... without
adding too much arithmetic!
|