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.

Autorentext

Born in Tbilisi, Georgia, studied Mathematics at Tbilisi State University and Informatics at Vienna University of Technology, where he obtained degree of Doctor of Science in 2012. Mikheil currently works as a researcher at Vekua Institute of Applied Mathematics, Tbilisi State University and is a post-doc at Inria Saclay / Ecole Polytechnique.