Andrzej Indrzejczak - Sequents and Trees: An Introduction to the Theory and Applications of Propositional Sequent Calculi

This series is devoted to the universal approach to logic and the development of a general theory of logics. It covers topics such as global set-ups for fundamental theorems of logic and frameworks for the study of logics, in particular logical matrices, Kripke structures, combination of logics, categorical logic, abstract proof theory, consequence operators, and algebraic logic. It includes also books with historical and philosophical discussions about the nature and scope of logic. Three types of books will appear in the series: graduate textbooks, research monographs, and volumes with contributed papers. All works are peer-reviewed to meet the highest standards of scientific literature.

More information about this series at http://www.springer.com/series/7391

This book is published under the imprint Birkhuser, www.birkhauser-science.com by the registered company Springer Nature Switzerland AG

The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland

There are a lot of excellent works in proof theory using various forms of Sequent Calculi (SC) as the basic formal systems. This book is of a different character. It is not a systematic exposition of proof theory using sequent calculus but it is a methodological study of sequent calculi as such. Of course it is not possible to present sequent calculi and their applications and to avoid a presentation of important issues in proof theory. However, our aim is to focus on the tools not on the results; the latter will serve as examples illustrating proof techniques developed in the framework of sequent calculi. In my opinion sequent calculi are truly amazing kind of formal systems and they deserve a separate study. In what follows we will present several variants of rules and calculi, describe their merits and focus on their applications. In particular, we will present in detail several methods of proving the most important results like the cut-elimination theorem, completeness, decidability, interpolation.

The book is elementary and self-contained. All technical details will be introduced both formally and with informal explanations. Proofs will be presented in detail but with a lot of gaps left as exercises for the careful reader. As our aim is to show how to use sequent calculi we must underline here that it is essential to do most of the exercises to gain a working knowledge of the methods presented. There is a tendency in contemporary works to present very general results. This is theoretically valuable but for a novice it may be hard to follow. In this book we opt for a different route; we rather present several case studies which are much simpler to grasp. After careful study of such special cases, the general and uniform treatment of broad classes of similar problems may be developed more easily.

We focus on proofs. Not so much on proofs in SC since their construction is rather simple and any reader who has worked with tableau systems should have no problem with proof search in SC. We rather focus on proofs of the most profound results concerning SC. We also want to show how easily SC may be used as a general and extremely elegant framework for doing general metalogic, usually presented in the setting of axiom systems.

In particular, we are going to focus on different methods of proving the cut-elimination (or admissibility) theorem which is one of the most important results of proof theory established in the framework of SC. References to Cut-Elimination Theorem (CET) are ubiquitous in the logical literature. One may find them in so diverse fields as the foundations of mathematics, automated deduction, logical programming or philosophical logic. Despite the widespread applications of this result, it is formulated in the specific framework of sequent calculi and related systems like tableaux. Roughly speaking, the cut-elimination theorem shows that every application of this important rule called cut may be eliminated from any proof in SC for some logic or theory. Although the rule of cut is in a sense essential for any SC, the possibility of its elimination yields many important consequences like consistency, decidability, interpolation, for many logics and theories.

SC was developed in its modern form by Gerhard Gentzen [95] for intuitionistic and classical logic in 1934, although the notion of a sequent was introduced earlier by Paul Hertz [114]. In fact, Gentzen was primarily concerned with Natural Deduction (ND) and SC was devised as a technical tool for investigations on the structure of proofs in ND. Gentzens idea was not only to provide rules of ND but also to show that every ND-proof may be transformed into normal form (with no detours). However, he was able to show it directly only for intuitionistic but not for classical logic, so he resigned from its publication (see von Plato [197]). Instead he introduced SC for both logics, proved that every proof in SC may be transformed into a cut-free proof, and finally that this implies the existence of ND normal proofs for every thesis of intuitionistic and classical logic.