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 a 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 two 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 的两条保守性结果。