Proof Schemata for Theories equivalent to $PA$: on the Benefit of Conservative Reflection Principles

David M. Cerna, Anela Lolic

Induction is typically formalized as a rule or axiom extension of the LK-calculus. While this extension of the sequent calculus is simple and elegant, proof transformation and anal…