Strong completeness and limited canonicity for PDL. (English) Zbl 1159.03020
J. Logic Lang. Inf. 17, No. 1, 69-87 (2008); errata ibid. 18, No. 2, 291-292 (2009).
Summary: 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 \([\alpha ; \beta ^{n }]\varphi\) 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.
MSC:
| 03B70 | Logic in computer science |
| 03B42 | Logics of knowledge and belief (including belief change) |
| 03B45 | Modal logic (including the logic of norms) |
References:
| [1] | Goldblatt R. (1982). Axiomatising the logic of computer prorgamming. Lecture Notes in Computer Science, Vol. 130. Berlin: Springer-Verlag. · Zbl 0474.68045 |
| [2] | Goldblatt, R. (1993). Mathematics of modality. CSLI Lecture Notes, Vol. 43. Stanford: CSLI Publications. · Zbl 0942.03516 |
| [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. · Zbl 0875.03076 |
| [4] | Harel D., Kozen D., Tiuryn J. (2000). Dynamic logic. Foundation of computing. Cambrigde, MIT Press · Zbl 0976.68108 |
| [5] | Knijnenburg, P. M. W. (1988). On axiomatisations for propositional logics of programs. Technical report, University of Utrecht, Nov 1988. RUU-CS-88-34. |
| [6] | Knijnenburg P.M.W., van Leeuwen J. (1991). On models for propositional dynamic logic. Theoretical Computer Science 91, 181-203 · Zbl 0753.68061 · doi:10.1016/0304-3975(91)90083-E |
| [7] | Kooi, B. P. (2003). Knowledge, chance, and change. PhD thesis, Department of Mathematics and Computing Science, University of Groningen. · Zbl 0753.68061 |
| [8] | Kooi B., Renardel de Lavalette G., Verbrugge R. (2006). Hybrid logics with infinitary proof systems. Journal of Logic and Computation 16, 161-175 · Zbl 1102.03017 · doi:10.1093/logcom/exi086 |
| [9] | Kozen D., Parikh R. (1981). An elementary proof of the completeness of PDL. Theoretical Computer Science 14, 113-118 · Zbl 0451.03006 · doi:10.1016/0304-3975(81)90019-0 |
| [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. · Zbl 0487.03012 |
| [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. · Zbl 0811.03011 |
| [12] | Rasiowa H., Sikorski R. (1950). A proof of the completeness theorem of Gödel. Fundamenta Mathematicae 37, 193-200 · Zbl 0040.29303 |
| [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. |
| [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-232 · Zbl 0198.02801 |
| [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. · Zbl 0546.03011 |
| [16] | Segerberg K. (1994). A model existence theorem in infinitary propositional modal logic. Journal of Philosophical Logic 23, 337-367 · Zbl 0811.03011 · doi:10.1007/BF01048686 |
| [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. · Zbl 0451.03004 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
