Categorical structure in coherent theory of arithmetic
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2023
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866908834721693696 |
|---|---|
| author | Ye, Lingyuan |
| author_facet | Ye, Lingyuan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2304_05477 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Categorical structure in coherent theory of arithmetic Ye, Lingyuan Logic Category Theory 03F30, 03G30, 03F10 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. |
| title | Categorical structure in coherent theory of arithmetic |
| topic | Logic Category Theory 03F30, 03G30, 03F10 |
| url | https://arxiv.org/abs/2304.05477 |