Abstract
Propositional dynamic logic (\(\mathsf{PDL}\)) is complete but not compact. As a consequence, strong completeness (the property \(\Gamma \models \varphi \Rightarrow \Gamma \vdash \varphi\)) requires an infinitary proof system. In this paper, we present a short proof for strong completeness of \(\mathsf{PDL}\) relative to an infinitary proof system containing the rule from [α; βn]φ for all \(n \in {\mathbb{N}}\) , conclude \([\alpha;\beta^*] \varphi\) . The proof uses a universal canonical model, and it is generalized to other modal logics with infinitary proof rules, such as epistemic knowledge with common knowledge. Also, we show that the universal canonical model of \(\mathsf{PDL}\) lacks the property of modal harmony, the analogue of the Truth lemma for modal operators.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Goldblatt R. (1982). Axiomatising the logic of computer prorgamming. Lecture Notes in Computer Science, Vol. 130. Berlin: Springer-Verlag.
Goldblatt, R. (1993). Mathematics of modality. CSLI Lecture Notes, Vol. 43. Stanford: CSLI Publications.
Harel, D. (1984). Dynamic logic. In D. Gabbay, & F. Guenthner (Eds.), Handbook of philosophical logic (Vol. II, pp. 497–604). Dordrecht: D. Reidel Publishing Company.
Harel D., Kozen D., Tiuryn J. (2000). Dynamic logic. Foundation of computing. Cambrigde, MIT Press
Knijnenburg, P. M. W. (1988). On axiomatisations for propositional logics of programs. Technical report, University of Utrecht, Nov 1988. RUU-CS-88-34.
Knijnenburg P.M.W., van Leeuwen J. (1991). On models for propositional dynamic logic. Theoretical Computer Science 91, 181–203
Kooi, B. P. (2003). Knowledge, chance, and change. PhD thesis, Department of Mathematics and Computing Science, University of Groningen.
Kooi B., Renardel de Lavalette G., Verbrugge R. (2006). Hybrid logics with infinitary proof systems. Journal of Logic and Computation 16, 161–175
Kozen D., Parikh R. (1981). An elementary proof of the completeness of PDL. Theoretical Computer Science 14, 113–118
Mirkowska, G. (1981). PAL—Propositional algorithmic logic. In E. Engeler (Ed.), Logic of programs. Lecture notes in computer science, (Vol. 125, pp. 23–101). Berlin: Springer-Verlag.
Pratt, V. R. (1976). Semantical considerations on Floyd-Hoare logic. In Proceedings of the 17th IEEE Symposium on the Foundations of Computer Science, pp. 109–112.
Rasiowa H., Sikorski R. (1950). A proof of the completeness theorem of Gödel. Fundamenta Mathematicae 37, 193–200
Renardel de Lavalette, G. R., Kooi, B. P., & Verbrugge, R. (2002). Strong completeness for propositional dynamic logic. In P. Balbiani, N.-Y. Suzuki, & F. Wolter (Eds.), AiML2002—Advances in modal logic (conference proceedings) (pp. 377–393). Institut de Recherche en Informatique de Toulouse IRIT.
Salwicki A. (1970). Formalized algorithmic languages. Bulletin de l’Académie Polonaise des Sciences: Série des sciences mathématiques, astronomiques et physiques 18, 227–232
Segerberg, K. (1982). A completeness theorem in the modal logic of programs. In T. Traczyck (Ed.), Universal Algebra and Applications. Papers presented at the Seminar held at the Stefan Banach International Mathematical Center 1978, (Vol. 9, pp. 31–46). PWN, Warsaw: Banach Center Publications.
Segerberg K. (1994). A model existence theorem in infinitary propositional modal logic. Journal of Philosophical Logic 23, 337–367
Trnkova, V., & Reiterman, J. (1980). Dynamic algebras which are not Kripke structures. In P. Dembiński (Ed.), Proceedings of the 9th Symposium on Mathematical Foundations of Computer Science. Lecture notes in computer science, (Vol. 88, pp. 528–538). Berlin: Springer-Verlag.
Author information
Authors and Affiliations
Corresponding author
Additional information
An erratum to this article is available at http://dx.doi.org/10.1007/s10849-009-9083-z.
Rights and permissions
Open Access This is an open access article distributed under the terms of the Creative Commons Attribution Noncommercial License ( https://creativecommons.org/licenses/by-nc/2.0 ), which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
About this article
Cite this article
Renardel de Lavalette, G., Kooi, B. & Verbrugge, R. Strong Completeness and Limited Canonicity for PDL. J of Log Lang and Inf 17, 69–87 (2008). https://doi.org/10.1007/s10849-007-9051-4
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10849-007-9051-4