Categorical structure in coherent theory of arithmetic

Abstract

In this paper we provide a semantic and syntactic analysis of parametrised natural numbers object in coherent categories, or pr-coherent categories. Semantically, we show the definable functions in the initial pr-coherent category are exactly given by primitive recursive functions. We also show that any pr-coherent category supports the construction of bounded universal quantifications, which are absent in an arbitrary coherent category. Under these semantic consideration, we construct a coherent theory of arithmetic and we show its syntactic category is equivalent to the initial pr-coherent category. From a logical perspective, we also show that this theory can be identified as the Σ1-fragment of IΣ1. Thus as an application, we provide a structural proof of the classical result in proof theory that the strongly Σ1-representable functions in IΣ1 are exactly primitive recursive functions.

To appear in "Theoretical Computer Science"