Journal of Logic, Language and Information

, Volume 17, Issue 1, pp 69–87 | Cite as

Strong Completeness and Limited Canonicity for PDL

  • Gerard Renardel de Lavalette
  • Barteld Kooi
  • Rineke Verbrugge
Open Access


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.


Propositional dynamic logic Strong completeness Canonical model Model disharmony 


  1. Goldblatt R. (1982). Axiomatising the logic of computer prorgamming. Lecture Notes in Computer Science, Vol. 130. Berlin: Springer-Verlag.Google Scholar
  2. Goldblatt, R. (1993). Mathematics of modality. CSLI Lecture Notes, Vol. 43. Stanford: CSLI Publications.Google Scholar
  3. 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.Google Scholar
  4. Harel D., Kozen D., Tiuryn J. (2000). Dynamic logic. Foundation of computing. Cambrigde, MIT PressGoogle Scholar
  5. Knijnenburg, P. M. W. (1988). On axiomatisations for propositional logics of programs. Technical report, University of Utrecht, Nov 1988. RUU-CS-88-34.Google Scholar
  6. Knijnenburg P.M.W., van Leeuwen J. (1991). On models for propositional dynamic logic. Theoretical Computer Science 91, 181–203CrossRefGoogle Scholar
  7. Kooi, B. P. (2003). Knowledge, chance, and change. PhD thesis, Department of Mathematics and Computing Science, University of Groningen.Google Scholar
  8. Kooi B., Renardel de Lavalette G., Verbrugge R. (2006). Hybrid logics with infinitary proof systems. Journal of Logic and Computation 16, 161–175CrossRefGoogle Scholar
  9. Kozen D., Parikh R. (1981). An elementary proof of the completeness of PDL. Theoretical Computer Science 14, 113–118CrossRefGoogle Scholar
  10. 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.Google Scholar
  11. 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.Google Scholar
  12. Rasiowa H., Sikorski R. (1950). A proof of the completeness theorem of Gödel. Fundamenta Mathematicae 37, 193–200Google Scholar
  13. 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.Google Scholar
  14. 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–232Google Scholar
  15. 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.Google Scholar
  16. Segerberg K. (1994). A model existence theorem in infinitary propositional modal logic. Journal of Philosophical Logic 23, 337–367CrossRefGoogle Scholar
  17. 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.Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2007

Authors and Affiliations

  • Gerard Renardel de Lavalette
    • 1
  • Barteld Kooi
    • 2
  • Rineke Verbrugge
    • 3
  1. 1.Department of Computing ScienceUniversity of GroningenGroningenThe Netherlands
  2. 2.Faculty of PhilosophyUniversity of GroningenGroningenThe Netherlands
  3. 3.Department of Artificial IntelligenceUniversity of GroningenGroningenThe Netherlands

Personalised recommendations