Cut-Elimination's Theorem Department of Logic Cut-elimination Theorem (CET) is one of the most important results of modern proof theory established in the framework of Sequent Calculi (SC). Gerhard Gentzen introduced SC for Intuitionistic and Classical Logic in his groundbreaking paper from 1934 devoted to Natural Deduction (ND). Although SC was treated originally as a technical tool for investigations on the properties of ND-proofs soon it became of interest in its own, for researchers in proof theory. Since then many variants of SC were devised suitable for dealing with various non-classical logics and formal theories. Also a lot of generalized versions of SC were provided like Display Calculi, Hypersequent Calculi, Many-sided Sequent Calculi. SC was also influential in the field of investigation on automated proof search leading to invention of early forms of Tableau Calculi. The rule of Cut is in a sense essential for any SC; Gentzen needed it for showing equivalence of SC with Axiomatic Calculi., namely for simulation of applications of Modus Ponens. This is not all - depending on the interpretation of sequents, Cut rule may be seen as expressing transitivity of consequence relation induced by SC, or as encoding the process of using lemmata in proof construction, or even as expressing the principle of bivalence. On the other hand it is welcome not to have it as a primitive rule of SC. Gentzen was well aware of the importance of CET and used it for showing the existence of normal ND-proofs, consistency and decidability of Propositional Intuitionistic and Classical Logic. The list of important consequences of CET may be enlarged with many technical (e.g. automated deduction, interpolation) and philosophical (e.g. analytic proofs, proof-theoretical semantics). Despite the variety of applications of CET, the methods of proving it are also of interest. The original Gentzen's proof is brilliant yet quite complicated. Since then a lot of other proof methods for CET were proposed. One can divide them roughly into indirect (semantic) and direct (constructive) proofs. The former show how to obtain cut-free proofs just from the beginning, whereas the latter are based on syntactical transformations of proofs either of local (e.g. Dragalin, Schutte) or of global character (e.g. Curry, Buss). Some of the methods were suitably abstracted and generalized in order to apply them in the framework of nonstandard variants of SC, and for many non-classical logics. The tutorial is rather self-contained but familiarity with standard results of mathematical and philosophical logic may help. It is divided into three parts: 2. We focus on the methods of proving CET and discuss the differences as well as the scope of applications of them. 3. We take a look at some generalizations of SC and related forms of CET. |
Bibliography Curry H. 1963, Foundations of Mathematical Logic, McGraw-Hill, New York Gentzen G. 1934, Untersuchungen über das Logische Schliessen, I i II, Mathematische Zeitschrift 39:176-210, 405-431. Kleene S. 1952, Introduction to Metamathematics, North Holland, Amsterdam Negri S. i J. von Plato 2001, Structural Proof Theory, Cambridge. Schütte K. 1977, Proof Theory, Springer Takeuti G. 1987, Proof Theory, North-Holland, Amsterdam Troelstra A. i H. Schwichtenberg, 1996, Basic Proof Theory, Oxford
| ||||
