Primitive Recursive Proof Systems for Arithmetic

Peano arithmetic, as formalized by Gentzen, can be presented as an axiom extension of the LK-calculus with equality and an additional inference rule formalizing induction. While this formalism was enough (with the addition of some meta-theoretic argumentation) to show the consistency of arithmetic, alternative formulations of induction such as the infinitary ω-rule and cyclic reasoning provide insight into the structure of arithmetic proofs obfuscated by the inference rule formulation of induction. For example, questions concerning the elimination of cut, consistency, and proof shape are given more clarity. The same could be said for functional interpretations of arithmetic such as system T which enumerates the recursive functions provably total by arithmetic. A key feature of these variations on the formalization of arithmetic is that they get somewhat closer to formalizing the concept of induction directly using the inferences of the LK-calculus, albeit by adding extra machinery at the meta-level. In this work we present a recursive sequent calculus for arithmetic which can be syntactically translated into Gentzen formalism of arithmetic and allows proof normalization to the LK-calculus with equality. [NOTE: In revision]