Cut-elimination and proof schemata

Abstract

By Gentzen’s famous Hauptsatz (the cut-elimination theorem) every proof in sequent calculus for first-order logic with cuts can be transformed into a cut-free proof; cut-free proofs are analytic and consist entirely of syntactic material of the end-sequent (the proven theorem). But in systems with induction rules, cut-elimination is either impossible or does not produce proofs with the subformula property. One way to overcome this problem is to formulate induction proofs as infinite sequences of proofs in a uniform way and to develop a method, which yields a uniform description of the corresponding cut-free proofs. We present such a formalism, as an alternative to systems with induction rules, and define a corresponding cut-elimination method (based on the CERES-method for first-order logic). The basic tools of proof theory, such as sequent- and resolution calculi are enriched with inductive definitions and schemata of terms, formulas, proofs, etc. We define a class of inductive proofs which can be transformed into this formalism and subjected to schematic cut-elimination.