Peano Arithmetic and muMALL: an Extended Abstract

EasyChair Preprint 8826

Abstract

We propose to examine some of the proof theory of arithmetic by using two proof systems. A linearized version of arithmetic is available using muMALL, which is MALL plus the following logical connective to treat first-order term structures: equality and inequality, first-order universal and existential quantification, and the least and greatest fixed point operators. The proof system muLK is an extension of muMALL in which contraction and weakening are permitted. It is known that muMALL has a cut-elimination result and is therefore consistent. We will show that muLK is consistent by embedding it into second-order linear logic. We also show that muLK contains Peano arithmetic and that in a couple of different situations, muLK is conservative over muMALL. Finally, we show that a proof that a relation represents a total function can be turned into a proof-search-based algorithm to compute that function.

Keyphrases: Peano arithmetic, linearize arithmetic, muMALL, polarity

@booklet{EasyChair:8826,
  author    = {Matteo Manighetti and Dale Miller},
  title     = {Peano Arithmetic and muMALL: an Extended Abstract},
  howpublished = {EasyChair Preprint 8826},
  year      = {EasyChair, 2022}}