Categorical Structure in Theory of Arithmetic

Authors

Abstract: In this paper, we provide a categorical analysis of the arithmetic theory

I S i g m a_{1}

. We will provide a categorical proof of the classical result that the provably total recursive functions in

I S i g m a_{1}

are exactly the primitive recursive functions. Our strategy is to first construct a coherent theory of arithmetic

m a t h b b T

, and prove that

m a t h b b T

presents the initial coherent category equipped with a parametrised natural number object. This allows us to derive the provably total functions in

m a t h b b T

are exactly the primitive recursive ones, and establish some other constructive properties about

m a t h b b T

. We also show that

m a t h b b T

is exactly the

P i_{2}

-fragment of

I S i g m a_{1}

, and conclude they have the same class of provably total recursive functions.

This page was built for publication: Categorical Structure in Theory of Arithmetic