Labeled sequent calculi for modal logics and implicit contractions

Archive for Mathematical Logic 52 (7-8):881-907 (2013)
  Copy   BIBTEX


The paper settles an open question concerning Negri-style labeled sequent calculi for modal logics and also, indirectly, other proof systems which make (more or less) explicit use of semantic parameters in the syntax and are thus subsumed by labeled calculi, like Brünnler’s deep sequent calculi, Poggiolesi’s tree-hypersequent calculi and Fitting’s prefixed tableau systems. Specifically, the main result we prove (through a semantic argument) is that labeled calculi for the modal logics K and D remain complete w.r.t. valid sequents whose relational part encodes a tree-like structure, when the unique rule which contains an harmful implicit contraction—by which the condition that the premises be less complex than the conclusion is violated—is modified into a contraction-free one respecting the latter condition, thus making the proof-search space finite.



    Upload a copy of this work     Papers currently archived: 94,698

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

40 (#396,080)

6 months
12 (#312,095)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Pierluigi Minari
Università degli Studi di Firenze

References found in this work

Proof Methods for Modal and Intuitionistic Logics.Melvin Fitting - 1985 - Journal of Symbolic Logic 50 (3):855-856.
Proof Analysis in Modal Logic.Sara Negri - 2005 - Journal of Philosophical Logic 34 (5-6):507-544.
Labelled deductive systems.Dov M. Gabbay - 1996 - New York: Oxford University Press.
Displaying Modal Logic.Heinrich Wansing - 1998 - Dordrecht, Netherland: Springer.
Proof analysis in intermediate logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1):71-92.

View all 15 references / Add more references