Gentzen calculi for modal propositional logic (Q987853): Difference between revisions

The book is about sequent systems (alias Gentzen calculi) for modal logic and focuses on a particular method, introduced by the author in her 2008 PhD thesis, which is called tree-hypersequent calculi. It covers the basic propositional modal logics -- extensions of the basic modal logic K by combinations of axioms D, T, 4, 5, B -- plus the modal logic GL of arithmetic provability. Part I of the book (which is identical to Chapter 1) elaborates a list of desiderata in order to make the notion of a `good' sequent calculus precise. The author starts by recalling that the proof theory for modal logic is much less developed than its model theory and that there are in particular no good sequent calculi for modal logics. Here are three of the main desiderata. (1) Explicitness: a modal operator should only appear in the lower sequent of a rule, and moreover only once so. (2) Syntactical purity: there should exist a translation from sequents to formulas such that a sequent is valid if and only if its translation is valid. (3) Existence of both a logical and a structural variant: the logical variant should have no structural rules (i.e., no weakening, no contraction, no cut), while the logical rules of the structural variant basically have to be double-line rules, i.e. rules whose upper and lower sequents are equivalent. Computational desiderata are not part of the list. The present reviewer notes that in the case of decidable logics it is however desirable to have a calculus providing a decision procedure; moreover, that procedure should stay within the computational complexity bounds for the logic. Part II overviews existing sequent systems for modal logics. As the author points out at the beginning (Chapter 2), the early systems that were proposed in the literature failed to satisfy explicitness as well as most of the other desiderata of her list. She goes on to critically examine the systems that were proposed more recently in the literature. She distinguishes purely syntactic methods (Chapter 3) from semantic methods (Chapter 4). The former contain, in particular, Wansing's display sequent calculi, while the latter contain Negri's internalized forcing calculi. Semantic methods talk explicitly about possible worlds and can therefore be expected to have difficulties to satisfy desideratum (3) of syntactic purity given that possible worlds are absent from the modal language. The author indeed gives translations from sequents to formulas only for purely syntactic methods. However, the non-existence of a translation for the semantic methods is not established (and moreover, the present reviewer wonders whether such a result would contradict the characterisation of models by Jankov-Fine formulas). Part II ends with Chapter 5 interrelating all the systems of the Chapters 3 and 4 by means of translations, some of which are original contributions of the author. The last part (Part III) contains the author's own tree-hypersequent calculi. Just as the other calculi it is based on the tree-model property that holds for the basic modal logics. While the other calculi represent trees either by sequences of numbers (such as Fitting's indexed sequent calculi) or by explicitly depicting them (such as Cerrato's semantic modal calculus), in the author's calculi trees are recursively defined as couples that are made up of a root and a list of subtrees, denoted \textit{(root/subtree1;\dots; subtreeN)}. In Chapter 6 the general and the logical variant of these calculi are defined and soundness and completeness results are proved with respect to the corresponding Hilbert systems. Chapter 7 establishes the admissibility of the cut rule. Decidability does not immediately follow from this, basically because the rule for a box in the antecedent repeats the principal formula in the upper sequent. For the logics K, KD, KT, KB, KTB, and S4 the author shows that in minimal derivations the number of applications of that rule (as well as of the special logical rules) can be bounded, thus establishing decidability. Chapter 7 contains semantic versions of the completeness results of Chapter 6. While the preceding chapters already contained soundness and completeness results for S5, Chapter 8 contains a new sequent calculus for S5 which better captures the simplicity of that logic. Finally, Chapter 9 is about the modal logic GL of arithmetic provability and Chapter 10 contains a translation from tree-hypersequent calculi into display calculi, thus completing the picture of Chapter 5.