On Proof Schemata and Primitive Recursive Arithmetic

Inductive proofs can be represented as a proof schemata, i.e. as a parameterized se- quence 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 ex- pressivity of proof schemata as defined in 10. We show that proof schemata can simulate primitive recursive arithmetic as defined in 12. Future research will focus on an extension of the simulation to primitive recursive arithmetic using quantification as defined in 7. The translation of proofs in arithmetic to proof schemata can be considered as a crucial step in the analysis of inductive proofs.