皮亚诺算术与$μ$MALL
Peano Arithmetic and $μ$MALL
AI总结：
本研究提出基于线性逻辑的算术形式理论$μ$MALL，展示其函数计算方式，扩展得到经典算术系统$μ$LK+并证明其一致性、包含皮亚诺算术及相关保守性结果。
摘要：
传统上，算术形式理论要么基于经典逻辑，要么基于直觉主义逻辑，分别催生了皮亚诺算术和海廷算术的发展。我们提出将$μ$MALL用作基于线性逻辑的算术形式理论。该形式系统以相继式演算证明系统的形式呈现，它对乘法-加法线性逻辑（MALL）的标准证明系统进行了扩展，新增了逻辑连接词全称量词与存在量词（一阶量词）、项相等与不等关系，以及最小和最大不动点算子。我们首先展示了如何通过一种简单的证明搜索算法，计算用$μ$MALL关系规范定义的函数。通过将弱化和收缩规则纳入$μ$MALL，我们得到了$μ$LK+，这是经典算术相继式演算的一个自然候选系统。尽管$μ$LK+仍缺乏重要的证明论成果（包括切消定理和聚焦完备性），但我们证明了$μ$LK+具有一致性，且包含皮亚诺算术。我们还证明了若干关于$μ$LK+相对于$μ$MALL的保守性结果。
英文摘要：
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 $μ$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 $μ$MALL relational specifications can be computed using a simple proof search algorithm. By incorporating weakening and contraction into $μ$MALL, we obtain $μ$LK+, a natural candidate for a classical sequent calculus for arithmetic. While important proof theory results are still lacking for $μ$LK+ (including cut-elimination and the completeness of focusing), we prove that $μ$LK+ is consistent and that it contains Peano arithmetic. We also prove some conservativity results regarding $μ$LK+ over $μ$MALL.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
