Proof analysis in modal logic
type: Item
instance of: scholarly article
title: Proof analysis in modal logic
zbMATH Open document ID: 1086.03045
author: Sara Negri
published in: Journal of Philosophical Logic
publication date: 2006-01-23T00:00:00Z
review text: Labelled sequent calculi, which internalize Kripke semantics into inference systems, are introduced for many normal modal logics such as K, T, K4, KB, S4, TB, S5 and GL. The calculi are cut-free and contraction-free and the validity of structural properties, invertibility of rules, admissibility of substitution, contraction and cut are proved syntactically. The interesting case of Gödel-Löb logic GL solves a long-standing open problem in the author's opinion, though the results do not quite match that claim. Firstly, the main open problem has no mention of labelled sequent calculus; so this is a partial answer. Secondly, as the author notes in the beginning of Section 6, in general cut-elimination alone does not ensure terminating proof search in a given system. So, she introduces some explicit upper bounds for terminating proof search in different systems such as those for K, KB, TB, S4 and S5. But unfortunately, the case of GL has been neglected; if it is implicit, which is not clear from the text, a brief mentioning would have removed the doubt. If there is no such a bound for GL, then the passage ``decidability properties get established in the strong form of an effective bound on proof search'' in the introduction may mislead the reader when it is not said that this does not hold for GL. Apart from these doubts, the paper contains good and original results: after the introduction and the preliminaries in Sections~1 and 2, labelled sequent calculi are introduced in Section~3, and in Section~4 the admissibility of their structural rules are proved. Section~5 is devoted to GL, and in Section~6 decidability of some of the above systems is settled. Equality is included in the systems in Subsection~7.1, and finally the paper concludes with a very interesting result on undefinability of some Kripke frame properties, such as irreflexivity and intransitivity, by modal axioms/rules. In Corollary~7.5 the author gives marvellous syntactic proofs for these well-known phenom…
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 5000204
zbMATH Keywords: Kripke semantics
zbMATH Keywords: normal modal logics
zbMATH Keywords: Gödel-Löb logic
zbMATH Keywords: labelled sequent calculi
zbMATH Keywords: admissibility of structural rules
zbMATH Keywords: decidability
zbMATH Keywords: Kripke frame
reviewed by: Saeed Salehi
describes a project that uses: TABLEAUX
describes a project that uses: Pesca
MaRDI profile type: Publication
full work available at URL: s10992-005-2267-3
OpenAlex ID: W1995718667
cites work: Natural deduction for non-classical logics
cites work: Representation, reasoning, and relational structures: a hybrid logic manifesto
cites work: Modal logic
cites work: A cut-free Gentzen formulation of the modal logic S5
cites work: Q4342093
cites work: A Systematic Presentation of Quantified Modal Logics
cites work: TABLEAUX: A general theorem prover for modal logics
cites work: Proof methods for modal and intuitionistic logics
cites work: Q3241192
cites work: Q5688807
cites work: A proof-theoretic study of the correspondence of classical logic and modal logic
cites work: On the proof theory of the modal logic for arithmetic provability
cites work: Q5598335
cites work: Q4495850
cites work: Indexed systems of sequents and cut-elimination
cites work: Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
cites work: Cut Elimination in the Presence of Axioms
cites work: Structural proof theory. With an appendix by Aarne Ranta
cites work: Proof systems for lattice theory
cites work: Proof-theoretical analysis of order relations
cites work: Translation Methods for Non-Classical Logics: An Overview
cites work: Q4325547
cites work: The modal logic of provability. The sequential approach
cites work: Q4716271
cites work: The modal logic of provability: cut-elimination
cites work: Q4342096
cites work: Q4530621
cites work: The logic of information structures
DOI: 10.1007/S10992-005-2267-3
description: scientific article; zbMATH DE number 5000204