@techreport{RISC5528,author = {David M. Cerna},
title = {{Primitive Recursive Proof Systems for Arithmetic}},
language = {english},
abstract = {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.},
year = {2018},
month = {January },
note = {In revision},
institution = {RISC},
length = {20}
}