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. 27 pages
Manighetti et al. (Thu,) studied this question.