Formal theories of arithmetic have traditionally been based on either classical or intuitionistic logic, leading to the development of Peano and Heyting arithmetic, respectively. We propose to use $\mu$MALL as a formal theory of arithmetic based on linear logic. This formal system is presented as a sequent calculus proof system that extends the standard proof system for multiplicative-additive linear logic (MALL) with the addition of the logical connectives universal and existential quantifiers (first-order quantifiers), term equality and non-equality, and the least and greatest fixed point operators. We first demonstrate how functions defined using $\mu$MALL relational specifications can be computed using a simple proof search algorithm. By incorporating weakening and contraction into $\mu$MALL, we obtain $\mu$LK+, a natural candidate for a classical sequent calculus for arithmetic. While important proof theory results are still lacking for $\mu$LK+ (including cut-elimination and the completeness of focusing), we prove that $\mu$LK+ is consistent and that it contains Peano arithmetic. We also prove some conservativity results regarding $\mu$LK+ over $\mu$MALL.

翻译：形式算术理论传统上基于经典逻辑或直觉主义逻辑，分别发展出了皮亚诺算术和海廷算术。我们提出使用$\mu$MALL作为基于线性逻辑的形式算术理论。该形式系统以相继式演算证明系统的形式呈现，它通过添加逻辑连接词全称与存在量词（一阶量词）、项相等与不相等、以及最小与最大不动点算子，扩展了标准乘法加法线性逻辑（MALL）的证明系统。我们首先展示了如何通过简单的证明搜索算法计算由$\mu$MALL关系式规范定义的函数。通过将弱化规则与缩并规则纳入$\mu$MALL，我们得到了$\mu$LK+，这是一个作为经典算术相继式演算的自然候选系统。尽管$\mu$LK+仍缺乏重要的证明论结果（包括切割消去与聚焦完备性），但我们证明了$\mu$LK+是一致的且包含皮亚诺算术。我们还证明了$\mu$LK+相对于$\mu$MALL的一些保守性结果。