Towards an Analysis of Proofs in Arithmetic

TL;DR

This paper explores the expressivity of proof schemata, demonstrating their ability to simulate primitive recursive arithmetic and their potential in automated proof analysis and cut-elimination.

Contribution

It shows that proof schemata can effectively simulate primitive recursive arithmetic, advancing the analysis of inductive proofs and proof transformations.

Findings

Proof schemata can represent inductive proofs as parameterized sequences.

Proof schemata can simulate primitive recursive arithmetic.

Translation of arithmetic proofs to schemata aids proof analysis.

Abstract

Inductive proofs can be represented as proof schemata, i.e. as parameterized sequences of proofs defined in a primitive recursive way. Applications of proof schemata can be found in the area of automated proof analysis where the schemata admit (schematic) cut-elimination and the construction of Herbrand systems. This work focuses on the expressivity of proof schemata. We show that proof schemata can simulate primitive recursive arithmetic. The translation of proofs in arithmetic to proof schemata can be considered as a crucial step in the analysis of inductive proofs.