Abstract
In this paper we answer the question what implicit proof assertions in the provability logic GL can be realized by explicit proof terms. In particular we show that the fragment of GL which can be realized by generalized proof terms of GLA is exactly S4 ∩ GL and equals the fragment that can be realized by proof-terms of LP. In the final sections of this paper we establish the disjunction property for GLA and give an axiomatization for GL ∩ S4.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Artemov, S.N.: Operational modal logic. Technical Report MSI 95-29, Cornell University (1995)
Artemov, S.N.: Explicit provability and constructive semantics. Bulletin of Symbolic Logic 7(1), 1–36 (2001)
Artemov, S.N., Beklemishev, L.D.: Provability logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 13, 2nd edn., pp. 229–403. Kluwer Academic Publishers, Dordrecht (2004)
Artemov, S.N., Nogina, E.: Logic of knowledge with justifications from the provability perspective. Technical Report TR-2004011, CUNY Ph.D. Program in Computer Science (2004)
Artemov, S.N., Straßen, T.: The basic logic of proofs. In: Martini, S., Börger, E., Kleine Büning, H., Jäger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 14–28. Springer, Heidelberg (1993)
Beklemishev, L.D., Visser, A.: Problems in the logic of provability. Technical Report Logic Group Preprint Series 235, Department of Philosophy of Utrecht University, Utrecht (2005)
Blackburn, P., de Rijke, M., Venema, Y.: Modal logic. Cambridge University Press, New York (2001)
Boolos, G.: The Logic of Provability. Cambridge University Press, Cambridge (1993)
Goris, E.: Logic of proofs for bounded arithmetic. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 191–201. Springer, Heidelberg (2006)
Goris, E.: Explicit proofs in formal provability logic. Technical Report TR-2006003, CUNY Ph.D. Program in Computer Science (2006)
Krupski, N.V.: On the complexity of the reflected logic of proofs. Technical Report TR-2003007, CUNY Ph.D. Program in Computer Science (2003)
Nogina, E.: On logic of proofs and provability. Bulletin of Symbolic Logic 12, 2005 Summer Meeting of the ASL (2006)
Schumm, G.F.: Some failures of interpolation in modal logic. Notre Dame Journal of Formal Logic 27(1), 108–110 (1986)
Segerberg, K.: Post completeness in modal logic. Journal of Symbolic Logic 37, 711–715 (1972)
Solovay, R.M.: Provability interpretations of modal logic. Israel Journal of Mathematics 25, 287–304 (1976)
Yavorskaya-Sidon, T.L.: Logic of proofs and provability. Annals of Pure and Applied Logic 113(1–3), 345–372 (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Goris, E. (2007). Explicit Proofs in Formal Provability Logic. In: Artemov, S.N., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2007. Lecture Notes in Computer Science, vol 4514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72734-7_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-72734-7_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72732-3
Online ISBN: 978-3-540-72734-7
eBook Packages: Computer ScienceComputer Science (R0)