Classical modal display logic in the calculus of structures and minimal cut-free deep inference calculi for S5

Rajeev Goré; Alwen Tiu

doi:10.1093/logcom/exm026

Classical modal display logic in the calculus of structures and minimal cut-free deep inference calculi for S5

Rajeev Goré^*, Alwen Tiu

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

10 Citations (Scopus)

Abstract

We begin by showing how to faithfully encode the Classical Modal Display Logic (CMDL) of Wansing into the Calculus of Structures (CoS) of Guglielmi. Since every CMDL calculus enjoys cut-elimination, we obtain a cut-elimination theorem for all corresponding CoS calculi. We then show how our result leads to a minimal cut-free CoS calculus for modal logic S5. No other existing CoS calculi for S5 enjoy both these properties simultaneously.

Original language	English
Pages (from-to)	767-794
Number of pages	28
Journal	Journal of Logic and Computation
Volume	17
Issue number	4
DOIs	https://doi.org/10.1093/logcom/exm026
Publication status	Published - Aug 2007

Access to Document

10.1093/logcom/exm026

Cite this

@article{a5ffdce8b53a4e2da4664fd8caf7f468,

title = "Classical modal display logic in the calculus of structures and minimal cut-free deep inference calculi for S5",

abstract = "We begin by showing how to faithfully encode the Classical Modal Display Logic (CMDL) of Wansing into the Calculus of Structures (CoS) of Guglielmi. Since every CMDL calculus enjoys cut-elimination, we obtain a cut-elimination theorem for all corresponding CoS calculi. We then show how our result leads to a minimal cut-free CoS calculus for modal logic S5. No other existing CoS calculi for S5 enjoy both these properties simultaneously.",

keywords = "Calculus of structures, Cut-free sequent calculi, Deep inference, Display logic, Proof theory of modal logic",

author = "Rajeev Gor{\'e} and Alwen Tiu",

year = "2007",

month = aug,

doi = "10.1093/logcom/exm026",

language = "English",

volume = "17",

pages = "767--794",

journal = "Journal of Logic and Computation",

issn = "0955-792X",

publisher = "Oxford University Press ",

number = "4",

}

TY - JOUR

T1 - Classical modal display logic in the calculus of structures and minimal cut-free deep inference calculi for S5

AU - Goré, Rajeev

AU - Tiu, Alwen

PY - 2007/8

Y1 - 2007/8

N2 - We begin by showing how to faithfully encode the Classical Modal Display Logic (CMDL) of Wansing into the Calculus of Structures (CoS) of Guglielmi. Since every CMDL calculus enjoys cut-elimination, we obtain a cut-elimination theorem for all corresponding CoS calculi. We then show how our result leads to a minimal cut-free CoS calculus for modal logic S5. No other existing CoS calculi for S5 enjoy both these properties simultaneously.

AB - We begin by showing how to faithfully encode the Classical Modal Display Logic (CMDL) of Wansing into the Calculus of Structures (CoS) of Guglielmi. Since every CMDL calculus enjoys cut-elimination, we obtain a cut-elimination theorem for all corresponding CoS calculi. We then show how our result leads to a minimal cut-free CoS calculus for modal logic S5. No other existing CoS calculi for S5 enjoy both these properties simultaneously.

KW - Calculus of structures

KW - Cut-free sequent calculi

KW - Deep inference

KW - Display logic

KW - Proof theory of modal logic

UR - http://www.scopus.com/inward/record.url?scp=34548396698&partnerID=8YFLogxK

U2 - 10.1093/logcom/exm026

DO - 10.1093/logcom/exm026

M3 - Article

SN - 0955-792X

VL - 17

SP - 767

EP - 794

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

IS - 4

ER -

Classical modal display logic in the calculus of structures and minimal cut-free deep inference calculi for S5

Abstract

Access to Document

Other files and links

Cite this