A Cut-Free Gentzen Formulation of the Modal Logic S5 Export

@misc{Bruener, abstract = {The goal of this paper is to introduce a new Gentzen formulation of the modal logic S5. The history of this problem goes back to the fifties where a counter-example to cut-elimination was given for an otherwise natural and straightforward formulation of S5. Since then, several cut-free Gentzen style formulations of S5 have been given. However, all these systems are technically involved, and furthermore, they differ considerably from Gentzen's original formulation of classical logic. In this paper we give a new sequent system for S5 which is a straightforward and technically simple extension of Gentzen's original sequent system for classical logic. A characteristic feature is the notion of a {\em connection\/} in a proof. The new system satisfies cut-elimination as well as the subformula property. Cut-elimination is proved by giving an algorithm for eliminating cuts. The fact that we give an algorithm for eliminating cuts makes it clear that our system is susceptible to a formulae-as-types computational interpretation.\footnote{Full version of a contributed paper presented at the {\em 6th Workshop on Logic, Language, Information and Computation\/} ({\em WoLLIC'99\/}), {\tt http://www.di.ufpe.br/\~{}wollic/wollic99}, held at the Hotel Simon, National Park of Itatiaia, Rio de Janeiro, Brazil, May 25--28 1999, with scientific sponsorship by IGPL, FoLLI, ASL, SBC, and SBL, and organised by Univ.\ Federal de Pernambuco (UFPE) and Univ.\ Estadual de Campinas (UNICAMP). Financial support was given by CNPq (Brazil), CAPES (Brazil), and Facolt\`a di Scienze della Univ.\ di Verona (Italy).}}, author = {Bra\"{u}ner, Torben}, citeulike-article-id = {267580}, citeulike-linkout-0 = {http://www3.oup.co.uk/igpl/Volume_08/Issue_05/#Bruener}, citeulike-linkout-1 = {http://dx.doi.org/doi:10.1093/jigpal/8.5.629}, doi = {doi:10.1093/jigpal/8.5.629}, journal = {Logic Journal of the IGPL}, keywords = {bibtex-import, calculus, cut, elimination, logic, modal, pnc, prooftheory, s5, sequent}, number = {5}, pages = {629--643}, posted-at = {2005-07-29 08:22:39}, priority = {2}, title = {A Cut-Free Gentzen Formulation of the Modal Logic S5}, url = {http://dx.doi.org/doi:10.1093/jigpal/8.5.629}, volume = {8}, year = {2000} }

TY - GEN ID - Bruener L3 - citeulike-article-id:267580 N2 - The goal of this paper is to introduce a new Gentzen formulation of the modal logic S5. The history of this problem goes back to the fifties where a counter-example to cut-elimination was given for an otherwise natural and straightforward formulation of S5. Since then, several cut-free Gentzen style formulations of S5 have been given. However, all these systems are technically involved, and furthermore, they differ considerably from Gentzen's original formulation of classical logic. In this paper we give a new sequent system for S5 which is a straightforward and technically simple extension of Gentzen's original sequent system for classical logic. A characteristic feature is the notion of a {\em connection\/} in a proof. The new system satisfies cut-elimination as well as the subformula property. Cut-elimination is proved by giving an algorithm for eliminating cuts. The fact that we give an algorithm for eliminating cuts makes it clear that our system is susceptible to a formulae-as-types computational interpretation.\footnote{Full version of a contributed paper presented at the {\em 6th Workshop on Logic, Language, Information and Computation\/} ({\em WoLLIC'99\/}), {\tt http://www.di.ufpe.br/\~{}wollic/wollic99}, held at the Hotel Simon, National Park of Itatiaia, Rio de Janeiro, Brazil, May 25--28 1999, with scientific sponsorship by IGPL, FoLLI, ASL, SBC, and SBL, and organised by Univ.\ Federal de Pernambuco (UFPE) and Univ.\ Estadual de Campinas (UNICAMP). Financial support was given by CNPq (Brazil), CAPES (Brazil), and Facolt\`a di Scienze della Univ.\ di Verona (Italy).} IS - 5 JF - Logic Journal of the IGPL EP - 643 TI - A Cut-Free Gentzen Formulation of the Modal Logic S5 VL - 8 SP - 629 KW - bibtex-import KW - calculus KW - cut KW - elimination KW - logic KW - modal KW - pnc KW - prooftheory KW - s5 KW - sequent AU - Bra\"{u}ner, Torben PY - 2000/// UR - http://dx.doi.org/doi:10.1093/jigpal/8.5.629 ER -