On Proof Schemata and Primitive Recursive Arithmetic
Alexander Leitsch, Anela Lolić, Stella Mahler · Kalpa publications in computing · 2024
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.