Hostname: page-component-78c5997874-94fs2 Total loading time: 0 Render date: 2024-11-17T16:16:59.254Z Has data issue: false hasContentIssue false
  • English
  • Français

A PURELY SYNTACTIC AND CUT-FREE SEQUENT CALCULUS FOR THE MODAL LOGIC OF PROVABILITY

Published online by Cambridge University Press:  01 December 2009

FRANCESCA POGGIOLESI
FRANCESCA POGGIOLESI*
Affiliation:
Centre For Logic and Philosophy of Science, Vrije Universiteit Brussel
*
*CENTRE FOR LOGIC AND PHILOSOPHY OF SCIENCE, VRIJE UNIVERSITEIT BRUSSEL, ETTERBEEK CAMPUS, PLEINLAAN 2, B-1050 BRUSSELS, BELGIUM E-mail:[email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper we present a sequent calculus for the modal propositional logic GL (the logic of provability) obtained by means of the tree-hypersequent method, a method in which the metalinguistic strength of hypersequents is improved, so that we can simulate trees shapes. We prove that this sequent calculus is sound and complete with respect to the Hilbert-style system GL, that it is contraction free and cut free and that its logical and modal rules are invertible. No explicit semantic element is used in the sequent calculus and all the results are proved in a purely syntactic way.

Type
Research Article
Information
The Review of Symbolic Logic , Volume 2 , Issue 4 , December 2009 , pp. 593 - 611
Copyright
Copyright © Association for Symbolic Logic 2009

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. (1996). The method of hypersequents in the proof theory of propositional non-classical logic. In Hodges, W., Hyland, M., Steinhorn, C., and Strauss, J., editors. Logic: From Foundations to Applications. Oxford: Oxford University Press, pp. 1–32.Google Scholar
Hill, B., & Poggiolesi, F. (2009). A contraction-free and cut-free sequent calculus for propositional dynamic logic. Studia Logica. Forthcoming.Google Scholar
Kashima, R. (1994). Cut-free sequent calculi for some tense logics. Studia Logica, 53, 119–135.CrossRefGoogle Scholar
Leivant, D. (1981). On the proof theory of the modal logic for arithmetic provability. Journal of Symbolic Logic, 46, 531–538.CrossRefGoogle Scholar
Moen, A. (2003). The proposed algorithms for eliminating cuts in the provability calculus GLS do not terminate. Nordic Workshop on Programming Theory, Norwegian Computing Center, 2001-12-10, 2001.Google Scholar
Negri, S. (2005). Proof analysis in modal logic. Journal of Philosophical Logic, 34, 507–534.CrossRefGoogle Scholar
Poggiolesi, F. (2008). Sequent calculi modal logic. PhD Thesis, pp. 1–224. Department of Philosophy, University of Florence and IHPST, Paris 1-Sorbonne.Google Scholar
Poggiolesi, F. (2009a). The method of tree-hypersequent for modal propositional logic. In Makinson, D., Malinowski, J., and Wansing, H., editors. Trends in Logic: Towards Mathematical Philosophy. Berlin: Springer, pp. 31–51.CrossRefGoogle Scholar
Poggiolesi, F. (2009b). Reflecting the semantic features of S5 at the syntactic level. SILFS Conference Proceedings. Forthcoming.Google Scholar
Sasaki, K. (2001). Löb’s axiom and cut-elimination theorem. Journal of the Nanzan Academic Society Mathematical Sciences and Information Engineering, 1, 91–98.Google Scholar
Valentini, S. (1983). The modal logic of provability: Cut-elimination. Journal of Philosophical Logic, 12, 471–476.CrossRefGoogle Scholar
Wansing, H. (1994). Sequent calculi for normal modal propositional logics. Journal of Logic and Computation, 4, 125–142.CrossRefGoogle Scholar
Wansing, H. (2002). Sequent systems for modal logics. In Gabbay, D. and Guenther, F., editors. Handbook of Philosophical Logic (second edition). Dordrecht: Kluwer, pp. 61–145.CrossRefGoogle Scholar