No label defined (Q4699355)

This paper is an introduction as the title indicates, and is a good one. The reader is expected to have heard about sequent calculi and cut-elimination. As a matter of fact, the author commences the main text with skillful explanation of the elimination procedure. He considers two kinds of nonclassical logics in this paper: modal logics and substructural logics. Among the latter, linear logic, relevant logic, etc, are touched upon, but the author mainly focuses on Lambek calculus, and its extensions by restoring some structural rules. Despite being confined mostly to propositional calculus, both classical and intuitionistic versions are considered. ``Methods'' explained are, of course, elimination of cut, and its consequences and/or applications like interpolation theorems, decision procedures, and variable separation priciples (Maksimova). Instead of exhibiting proofs, constructions, and so forth, in a `cut and dried' fashion the author explains nicely the fundamental ideas, thought processes, etc. He is also a good cicerone to the literature. A minor complaint: origins of labels are not explained. A beginner, like the reviewer half a century ago (well, not quite yet), may be entertained by information such as: In systems LK and GK, the first K is for ``klassisch'' while the second K is for ``Kripke''. Also, S4 and S5 go back to Lewis-Langford, 1920's , etc. For the entire collection see [Zbl 0919.00041].