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

TL;DR

This paper extends proof schemata, a recursive formalism for induction, to Peano arithmetic, establishing a conservative reflection principle and enabling proof analysis with Herbrand-like properties.

Contribution

It introduces a formalism that relates Peano arithmetic to proof schemata, facilitating proof analysis and preserving Herbrand's theorem in a new setting.

Findings

Proof schemata can be extended to Peano arithmetic.

A conservative reflection principle between PA and proof schemata is established.

Herbrand's theorem variant applies to the new formalism.

Abstract

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 analysis can be quite difficult. Theories with an induction rule, for example Peano arithmetic do not have a {\em Herbrand} theorem. In this work we extend an existing meta-theoretic formalism, so called proof schemata, a recursive formulation of induction particularly suited for proof analysis, to Peano arithmetic. This relationship provides a meaningful conservative reflection principle between \PA and an alternative proof formalism. Proof schemata have been shown to have a variant of Herbrand's theorem for classical logic which can be lifted to the subsystem of our new formalism equivalent to primitive recursive arithmetic.