This comprehensive monograph is a cornerstone in the area of mathematical logic and related fields. Focusing on Gentzen-type proof theory, the book presents a detailed overview of creative works by the author and other 20th-century logicians that includes applications of proof theory to logic as well as other areas of mathematics. 1975 edition.

We introduce several restricted versions of the structural rules in the implicational fragment of Gentzen's sequent calculus LJ. For example, we permit the applications of a structural rule only if its principal formula is an implication. We investigate cut-eliminability and theorem-equivalence among various combinations of them. The results include new cut-elimination theorems for the implicational fragments of the following logics: relevant logic E, strict implication S4, and their neighbors (e.g., E-W and S4-W); BCI-logic, BCK-logic, relevant logic R, and the intuitionistic (...) logic. (shrink)

We show that the rule that allows the inference of A from A ⊗ B is admissible in many of the basic multiplicative systems. By adding this rule to these systems we get, therefore, conservative extensions in which the tensor behaves as classical conjunction. Among the systems obtained in this way the one derived from RMIm has a particular interest. We show that this system has a simple infinite-valued semantics, relative to which it is strongly complete, and a nice cut-free (...) Gentzen-type formulation which employs hypersequents . Moreover: classical logic has a simple, strong translation into this logic. This translation uses definable connectives and preserves the consequence relation of classical logic . Similar results, but with a 3-valued semantics, obtain if instead of RMIm we use RMm. (shrink)

The initial sections of this text deal with syntactical matters such as logical formalism, cut-elimination, and the embedding of intuitionistic logic in classical linear logic. Concluding chapters focus on proofnets for the multiplicative fragment and the algorithmic interpretation of cut-elimination in proofnets.