皮亚诺算术与μMALL

算术的形式理论传统上基于经典逻辑或直觉逻辑，分别导致了皮亚诺算术和海廷算术的发展。我们建议使用μMALL作为基于线性逻辑的算术形式理论。这个形式系统被呈现为序列演算证明系统，扩展了乘法-加法线性逻辑（MALL）的标准证明系统，增加了逻辑连接词的全称量词和存在量词（的一阶量词）、项的等同性和非等同性、最小和最大不动点算子。我们首先演示如何使用简单的证明搜索算法计算通过μMALL关系规范定义的函数。通过将弱化和收缩纳入μMALL，我们得到μLK+，这是一个关于算术的经典序列演算的自然候选者。尽管对于μLK+仍缺乏重要的证明理论结果（包括切除消除和聚焦的完备性），我们证明了μLK+是一致的，并且它包含皮亚诺算术。我们还证明了关于μLK+相对于μMALL的一些保守性结果。27页