Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Categorical structure in coherent theory of arithmetic

Lingyuan Ye

TL;DR

The paper addresses how to model computability within a weak categorical setting by using coherent categories equipped with a parametrised natural numbers object (PNO). It develops a semantic picture (the initial pr-coherent category) and a syntactic anchor (a coherent arithmetic theory $\mathbb{T}$) whose syntactic category is initial, showing definable morphisms between powers of the NNO are precisely primitive recursive functions and that bounded universal quantification is available. It then connects this to proof theory by showing $\mathbb{T}$ captures the $\Sigma_1$-fragment of $I\Sigma_1$, yielding a structural proof that strongly $\Sigma_1$-representable functions in $I\Sigma_1$ are exactly the primitive recursive functions. The work illuminates a tight correspondence between categorical logic and arithmetic, enabling glueing techniques and a constructive viewpoint on provability and truth, with potential applications to other arithmetic theories and weaker categorical bases.

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.

Categorical structure in coherent theory of arithmetic

TL;DR

The paper addresses how to model computability within a weak categorical setting by using coherent categories equipped with a parametrised natural numbers object (PNO). It develops a semantic picture (the initial pr-coherent category) and a syntactic anchor (a coherent arithmetic theory ) whose syntactic category is initial, showing definable morphisms between powers of the NNO are precisely primitive recursive functions and that bounded universal quantification is available. It then connects this to proof theory by showing captures the -fragment of , yielding a structural proof that strongly -representable functions in are exactly the primitive recursive functions. The work illuminates a tight correspondence between categorical logic and arithmetic, enabling glueing techniques and a constructive viewpoint on provability and truth, with potential applications to other arithmetic theories and weaker categorical bases.

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.
Paper Structure (21 sections, 33 theorems, 103 equations)

This paper contains 21 sections, 33 theorems, 103 equations.

Table of Contents

  1. Introduction
  2. Definable functions in the initial pr-coherent category
  3. Presentation of the initial pr-coherent category by an arithmetic theory
  4. Application of initiality
  5. Coherent arithmetic
  6. Parametrised natural numbers object in coherent categories
  7. Primitive recursion and order
  8. Induction principle
  9. Bounded $\mu$-operator
  10. Bounded universal quantifier
  11. Stability under base change
  12. Initiality of coherent arithmetic
  13. Definable functions in the initial pr-coherent category
  14. Coherent arithmetic and $I\Sigma_1$
  15. Further Proof-Theoretic Properties of Coherent Arithmetic
  16. ...and 6 more sections

Key Result

Theorem 1

In $I\Sigma_1$, the strongly $\Sigma_1$-representable functions are exactly the primitive recursive functions.

Theorems & Definitions (88)

  • Theorem : Strongly representable functions in $I\Sigma_1$
  • Definition 2.1: Function description
  • Definition 2.2: Coherent Arithmetic
  • Remark 2.3: $\mathbb{T}$ is not a coherent theory a priori
  • Remark 2.4: $\mathbb{T}$ is a coherent theory after all
  • Example 2.5: Explicit existence implies existence
  • Example 2.6: Equality is a congruence
  • Example 2.7: Successor
  • Example 2.8: Addition
  • Example 2.9: Subtraction
  • ...and 78 more