Hostname: page-component-586b7cd67f-tf8b9 Total loading time: 0 Render date: 2024-11-30T15:05:03.206Z Has data issue: false hasContentIssue false
  • English
  • Français

VALENTINI’S CUT-ELIMINATION FOR PROVABILITY LOGIC RESOLVED

Published online by Cambridge University Press:  06 March 2012

RAJEEV GORÉ  and
REVANTHA RAMANAYAKE
RAJEEV GORÉ*
Affiliation:
Logic and Computation Group, Research School of Computer Science, The Australian National University
REVANTHA RAMANAYAKE*
Affiliation:
CNRS LIX, École Polytechnique
*
*LOGIC AND COMPUTATION GROUP, RESEARCH SCHOOL OF COMPUTER SCIENCE, THE AUSTRALIAN NATIONAL UNIVERSITY, CANBERRA, ACT 0200, AUSTRALIA. E-mail: [email protected]
†CNRS LIX, ÉCOLE POLYTECHNIQUE, 91128 PALAISEAU, FRANCE. E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Valentini (1983) has presented a proof of cut-elimination for provability logic GL for a sequent calculus using sequents built from sets as opposed to multisets, thus avoiding an explicit contraction rule. From a formal point of view, it is more syntactic and satisfying to explicitly identify the applications of the contraction rule that are ‘hidden’ in proofs of cut-elimination for such sequent calculi. There is often an underlying assumption that the move to a proof of cut-elimination for sequents built from multisets is straightforward. Recently, however, it has been claimed that Valentini’s arguments to eliminate cut do not terminate when applied to a multiset formulation of the calculus with an explicit rule of contraction. The claim has led to much confusion and various authors have sought new proofs of cut-elimination for GL in a multiset setting.

Here we refute this claim by placing Valentini’s arguments in a formal setting and proving cut-elimination for sequents built from multisets. The use of sequents built from multisets enables us to accurately account for the interplay between the weakening and contraction rules. Furthermore, Valentini’s original proof relies on a novel induction parameter called “width” which is computed ‘globally’. It is difficult to verify the correctness of his induction argument based on “width.” In our formulation however, verification of the induction argument is straightforward. Finally, the multiset setting also introduces a new complication in the case of contractions above cut when the cut-formula is boxed. We deal with this using a new transformation based on Valentini’s original arguments.

Finally, we discuss the possibility of adapting this cut-elimination procedure to other logics axiomatizable by formulae of a syntactically similar form to the GL axiom.

Type
Research Article
Information
The Review of Symbolic Logic , Volume 5 , Issue 2 , June 2012 , pp. 212 - 238
Copyright
Copyright © Association for Symbolic Logic 2012

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

BIBLIOGRAPHY

Avron, A. (1984). On modal systems having arithmetical interpretations. Journal of Symbolic Logic, 49(3), 935–942.CrossRefGoogle Scholar
Avron, A. (1996). The method of hypersequents in the proof theory of propositional non-classical logics. In Logic: From Foundations to Applications (Staffordshire, 1993). Oxford Sci. Publ. New York, NY: Oxford University Press, pp. 1–32.Google Scholar
Belnap, N. D Jr. (1982). Display logic. Journal of Philosophical Logic, 11(4), 375–417.Google Scholar
Bimbó, K. (2007). , , LK, and cutfree proofs. Journal of Philosophical Logic, 36(5), 557–570.Google Scholar
Borga, M. (1983). On some proof theoretical properties of the modal logic GL. Studia Logica: An International Journal for Symbolic Logic, 42(4), 453–459.Google Scholar
Borga, M., & Gentilini, P. (1986). On the proof theory of the modal logic Grz. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 32(2), 145–148.CrossRefGoogle Scholar
Borisavljević, M., Došen, K., & Petrić, Z. (2000). On permuting cut with contraction. Mathematical Structures in Computer Science, 10(2), 99–136. The Lambek Festschrift: mathematical structures in computer science (Montreal, QC, 1997).Google Scholar
Dawson, J. E., & Goré, R. (2010). Generic methods for formalising sequent calculi applied to provability logic. In Fermüller, C. G., and Voronkov, A., editors. LPAR (Yogyakarta), Vol. 6397 of Lecture Notes in Computer Science. Berlin Heidelberg, Germany: Springer, pp. 263–277.Google Scholar
Demri, S., & Goré, R. (2002). Theoremhood-preserving maps characterizing cut elimination for modal provability logics. Journal of Logic and Computation, 12(5), 861–884.CrossRefGoogle Scholar
Došen, K. (1985). Sequent-systems for modal logic. Journal of Symbolic Logic, 50(1), 149–168.Google Scholar
Gentzen, G. (1969). The collected papers of Gerhard Gentzen. In Szabo, M. E., editor. Studies in Logic and the Foundations of Mathematics. Amsterdam: North-Holland Publishing Co.Google Scholar
Goré, R. (1999). Tableau methods for modal and temporal logics. In Handbook of Tableau Methods. Dordrecht, The Netherlands: Kluwer Academic Publishers, pp. 297–396.Google Scholar
Goré, R., Heinle, W., & Heuerding, A. (1997). Relations between propositional normal modal logics: An overview. Journal of Logic and Computation, 7(5), 649–658.Google Scholar
Goré, R., & Ramanayake, R. (2008). Valentini’s cut-elimination for provability logic resolved. In Areces, C., and Goldblatt, R., editors. Advances in Modal Logic, Vol. 7. London: College Publications, pp. 91–111.Google Scholar
Goré, R., & Ramanayake, R. (2012). Cut-elimination for weak Grzegorczyk logic Go. Accepted subject to minor revisions by Studia Logica.Google Scholar
Guglielmi, A. (2007). A system of interaction and structure. ACM Transactions on Computational Logic, 8(1), Art. 1, 64.Google Scholar
Indrzejczak, A. (1996). Cut-free sequent calculus for S5. University of Łódź, Department of Logic: Bulletin of the Section of Logic, 25(2), 95–102.Google Scholar
Leivant, D. (1981). On the proof theory of the modal logic for arithmetic provability. Journal of Symbolic Logic, 46(3), 531–538.Google Scholar
Mints, G. (2005). Cut elimination for provability logic. In Collegium Logicum 2005: Cut-Elimination.Google Scholar
Moen, A. (2001). The Proposed Algorithms for Eliminating Cuts in the Provability Calculus GLS do not Terminate. NWPT 2001, Norwegian Computing Center, 2001-12-10. http://publ.nr.no/3411.Google Scholar
Negri, S. (2005). Proof analysis in modal logic. Journal of Philosophical Logic, 34(5–6), 507–544.CrossRefGoogle Scholar
Negri, S., & von Plato, J. (2001). Structural Proof Theory. Cambridge, UK: Cambridge University Press. Appendix C by Aarne Ranta.CrossRefGoogle Scholar
Poggiolesi, F. (2008). A cut-free simple sequent calculus for modal logic S5. The Review of Symbolic Logic, 1(1), 3–15.CrossRefGoogle Scholar
Poggiolesi, F. (2009). A purely syntactic and cut-free sequent calculus for the modal logic of provability. Review of Symbolic Logic, 2(4), 593–611.CrossRefGoogle Scholar
Pottinger, G. (1983). Uniform, cut-free formulations of T, S4 and S5 (abstract). Journal of Symbolic Logic, 48, 900–901.Google Scholar
Sambin, G., & Valentini, S. (1982). The modal logic of provability. The sequential approach. Journal of Philosophical Logic, 11(3), 311–342.CrossRefGoogle Scholar
Sasaki, K. (2001). Löb’s axiom and cut-elimination theorem. Journal of the Nanzan Academic Society of Mathematical Sciences and Information Engineering, 1, 91–98.Google Scholar
Sato, M. (1980). A cut-free Gentzen-type system for the modal logic S5. Journal of Symbolic Logic, 45(1), 67–84.CrossRefGoogle Scholar
Shimura, T. (1991). Cut-free systems for the modal logic S4.3 and S4.3Grz. Reports on Mathematical Logic, 25, 57–73.Google Scholar
Shimura, T. (1992). Cut-free systems for some modal logics containing S4. Reports on Mathematical Logic, 26, 39–65.Google Scholar
Solovay, R. M. (1976). Provability interpretations of modal logic. Israel Journal of Mathematics, 25(3–4), 287–304.Google Scholar
Švejdar, V. (1999). On provability logic. Nordic Journal of Philosophical Logic, 4(2), 95–116.Google Scholar
Takeuti, G. (1987). Proof Theory (second edition), Vol. 81 of Studies in Logic and the Foundations of Mathematics. Amsterdam: North-Holland Publishing Co.Google Scholar
Troelstra, A. S., & Schwichtenberg, H. (2000). Basic Proof Theory (second edition), Vol. 43 of Cambridge Tracts in Theoretical Computer Science. Cambridge, UK: Cambridge University Press.Google Scholar
Valentini, S. (1983). The modal logic of provability: Cut-elimination. Journal of Philosophical Logic, 12(4), 471–476.CrossRefGoogle Scholar
Valentini, S. (1986). A syntactic proof of cut-elimination for GLlin. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 32(2), 137–144.Google Scholar
von Plato, J. (2001). A proof of Gentzen’s Hauptsatz without multicut. Archive for Mathematical Logic, 40(1), 9–18.Google Scholar