Please use this identifier to cite or link to this item: http://hdl.handle.net/1822/58110

TitleA proof-theoretic study of bi-intuitionistic propositional sequent calculus
Author(s)Pinto, Luís F.
Uustalu, Tarmo
Keywordsbi-intuitionistic logic
Labelled sequent calculus
Nested sequent calculus
Cut-elimination
Issue date1-Feb-2018
PublisherOxford Univ Press
JournalJournal of Logic and Computation
Abstract(s)Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a connective dual to implication usually called ‘exclusion’. A standard-style sequent calculus for this logic is easily obtained by extending multiple-conclusion sequent calculus for intuitionistic logic with exclusion rules dual to the implication rules (in particular, the exclusion-left rule restricts the premise to be single-assumption). However, similarly to standard-style sequent calculi for non-classical logics like S5, this calculus is incomplete without the cut rule. Motivated by the problem of proof search for propositional bi-intuitionistic logic (BiInt), various cut-free calculi with extended sequents have been proposed, including (i) a calculus of nested sequents by Goré et al., which includes rules for creation and removal of nests (called ‘nest rules’, resp. ‘unnest rules’) and (ii) a calculus of labelled sequents by the authors, derived from the Kripke semantics of BiInt, which includes ‘monotonicity rules’ to propagate truth/falsehood between accessible worlds. In this paper, we develop a proof-theoretic study of these three sequent calculi for BiInt grounded on translations between them. We start by establishing the basic meta-theory of the labelled calculus (including cut-admissibility), and use then the translations to obtain results for the other two calculi. The translation of the nested calculus into the standard-style calculus explains how the unnest rules encapsulate cuts. The translations between the labelled and the nested calculi reveal the two formats to be very close, despite the former incorporating semantic elements, and the latter being syntax-driven. Indeed, we single out (i) a labelled calculus whose sequents have a ‘label in focus’ and which includes ‘refocusing rules’ and (ii) a nested calculus with monotonicity and refocusing rules, and prove these two calculi to be isomorphic (in a bijection both at the level of sequents and at the level of derivations).
TypeArticle
URIhttp://hdl.handle.net/1822/58110
DOI10.1093/logcom/exx044
ISSN0955-792X
e-ISSN1465-363X
Publisher versionhttps://academic.oup.com/logcom/article/28/1/165/4807375
Peer-Reviewedyes
AccessOpen access
Appears in Collections:CMAT - Artigos em revistas com arbitragem / Papers in peer review journals

Files in This Item:
File Description SizeFormat 
jlc15-62-final.pdf522,44 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID