About Cut-Elimination in Schematic Proofs

Gentzen's Hauptsatz (cut-elimination theorem) is the cornerstone in proof theory. It leads to analytic proofs. But in the systems, having induction as a rule, cut-elimination is not possible in general. One way to overcome this problem is to define an infinite sequence of proofs in a uniform way and a method, which will obtain a uniform description of corresponding analytic proofs. This book presents such a formalism, alternative to the inductive systems and defines a cut-elimination method for it. First, the basic concepts of proof theory, such as sequent and resolution calculi are defined. Later they are enriched with inductive definitions and schemata of terms, formulas, proofs, etc., are obtained. The cut-elimination method for such proof schemata is illustrated on several examples. The text is self-contained, thus can be read by not only experts, but anyone else interested in mathematical logic and proof theory.