Deep sequent systems for modal logic
type: Item
instance of: scholarly article
title: Deep sequent systems for modal logic
zbMATH Open document ID: 1180.03023
author: Kai Brünnler
published in: Archive for Mathematical Logic
publication date: 2009-08-27T00:00:00Z
review text: This is a very interesting paper presenting a systematic set of cut-free axiomatisations for all the basic normal modal logics formed by some combination of the axioms d, t, b, 4, 5. They are based on a form of deep inference where rules may not only be applied to the outermost connective but also deep inside formulas. The systems all enjoy the subformula property, all rules are invertible, and weakening, contraction and cut are admissible. This is achieved without reference to semantic notions like, for example, labels. The author establishes soundness, completeness and terminating proof search as well as a syntactic cut-elimination procedure. Also relations to other formalisms (a system by Kashima, the calculus of structures, labeled systems, hypersequents, and the display calculus) are studied in detail. The systems presented in this paper are not as modular as labeled systems. Brünnler and Strassburger overcome this shortcoming the sequel paper [\textit{K. Brünnler } and \textit{L. Strassburger}, Lect. Notes Comput. Sci. 5607, 152--166 (2009; Zbl 1180.03024)]. The deep inference approach to modal logic, as introduced in this paper, is essential for establishing syntactic cut-elimination for the logic of common knowledge. Such a cut-elimination procedure is presented in [\textit{K. Brünnler} and \textit{T. Studer}, Ann. Pure Appl. Logic 160, No.~1, 82--95 (2009; Zbl 1170.03007)].
reviewed by: Thomas Studer
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 5598854
zbMATH Keywords: nested sequents
zbMATH Keywords: modal logic
zbMATH Keywords: cut elimination
zbMATH Keywords: deep inference
zbMATH Keywords: subformula property
MaRDI profile type: Publication
full work available at URL: s00153-009-0137-3
OpenAlex ID: W1966647830
cites work: Display logic
cites work: Q3375282
cites work: Q3509048
cites work: A Local System for Classical Logic
cites work: CUT ELIMINATION FOR PROPOSITIONAL DYNAMIC LOGIC WITHOUT
cites work: Q4783301
cites work: Cut-free sequent calculi for some tense logics
cites work: Q5688812
cites work: Proof analysis in modal logic
cites work: The Method of Tree-Hypersequents for Modal Propositional Logic
cites work: A study of Kripke-type models for some modal logics by Gentzen's sequential method
cites work: Q5483015
cites work: A deep inference system for the modal logic S5
cites work: MELL in the calculus of structures
cites work: Q4716271
cites work: Displaying modal logic
DOI: 10.1007/S00153-009-0137-3
Recommended article: Q3509048
Recommended article: Q5483015
Recommended article: Modular Sequent Systems for Modal Logic
Recommended article: Modal sequents for normal modal logics
Recommended article: Q4636304
Recommended article: A deep inference system for the modal logic S5
Recommended article: Cut-free modal sequents for normal modal logics
Recommended article: Q4296507
Recommended article: Labelled proofs for quantified modal logic
Recommended article: Q5688809
description: scientific article; zbMATH DE number 5598854