Gregory H. Moore (ed. The Collected Papers of Bertrand Russell, Volume 5: Toward "Principia Mathematica" London and New York: Routledge, 2014, c 954 and 10 plates
substructural logics. Apart from syntactical techniques for cut elimination, some semantical techniques are developed as well. The most important consequenes of cut elimination are summarized. It follows a survey Chapter 8 on related proof systems, including natural deduction systems, tableau systems and resolution systems. The final Chapter 9 of the book is centered around various decidability procedures based on cut free calculi for many logics discussed in this book. Some special emphasis is again put on substructural logics. The latter presentation culminates in an outline of proof (due to the author and J. M. Dunn) of the decidability of the logic of pure ticket entailment; this was a major open problem in relevance logic until 2010. The chapter concludes with some remarks about sequent calculi for mathematical theories as well as typed and labeled calculi. The book includes an appendix with background information on trees, inductive proofs, and Curry's paradox. This is a very valuable monograph and an important reference work on sequent calculi for a wide range of logics, with an emphasis on substructural logics. It is carefully written with plenty of motivational material and informal explanations. The text includes a large number of exercises of varying degree of difficulty which makes it suitable as a course text as well as for self studying. A growing number of solutions to some of these exercises is available on the author's website. The book is suitable for various courses at advanced undergraduate as well as graduate level. Beginners will certainly take advantage of the thorough treatment of classical logic, whereas more advanced students will focus on nonclassical logics and their meta logical results. The choice of topics in the book is attractive to various researchers. For example, computer scientists will like the syntactic approach and the relation of sequent calculus to type systems, philosophers will find the extensive treatment of relevance logics very useful, whereas linguists will appreciate the detailed description of Lambek calculi. The book sometimes does not give original references to the various calculi included. Maybe a next edition could include a notes section for each of the chapters with historial references and pointers to related work. Moreover, the monograph due to its strong focus on sequent calculi has very little information about semantics, especially for nonclassical logics. Of course, there is not much space in a book of nearly 400 pages, but it would have been nice to add some basic semantical considerations in the text or at least in the exercises. In conclusion, Bimbo has written an excellent book on the proof theory of nonclassical and, in particular, substructural logics, which is a highly welcome and complementary addition to the previously available textbooks on structural proof theory.
The Bulletin of Symbolic Logic