Recently prepositional modal logic of programs, called ‘prepositional dynamic logic’, has been developed by many authors, following the ideas of Fisher and Ladner  and Pratt . The main purpose of this paper is to present a Gentzen-type sequential formulation of this logic and to establish its semantical completeness with due regard to sequential formulation as such. In a sense our sequential formulation might be regarded as a powerful tool to establish the completeness theorem of already familiar axiomatizations of prepositional dynamic logic such as seen in Harel , Parikh  or Segerberg . Indeed our method is powerful enough in completeness proof to yield a desired structure directly without making a detour through such intermediate constructs as a ‘pseudomodel’ or a ‘nonstandard structure’, which can be seen in Parikh . We also show that our sequential system of prepositional dynamic logic does not enjoy the so-called cut-elimination theorem.
This is a preview of subscription content, log in to check access.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
Fischer, M.J., Ladner, R.E.: Propositional modal logic of programs. Proceedings 9th Annual ACM Symposium on Theory of Computing, pp. 296–294, Boulder Co, 1977
Gentzen, G.: Untersuchungen über das logische Schliessen I and II. Math. Z. 39, 176–210 and 405–431 (1935)
Harel, D., Meyer, A.R., Pratt, V.R.: Computability and completeness in logics of programs. Proceedings 9th Annual Symposium on Theory of Computing, pp. 261–268, Boulder 1977
Harel, D.: Logics of programs: Axiomatics and descriptive power. MIT, ph.D.thesis, May 1978
Hughes, G.E., Cresswell, M.J.: An introduction to modal logic. London: Methuen 1968
Manna, Z.: Mathematical theory of computation. New York: McGraw-Hill 1974
Monk, D.: Mathematical logic. Berlin-Heidelberg-New York: Springer 1976
Nishimura, H.: A study of some tense logics by Gentzen's sequential method. forthcoming in Publ. R.I.M.S.
Ohnishi, M., Matsumoto, K.: Gentzen method in modal calculi I. Osaka Math. J. 9, 113–130 (1957)
Ohnishi, M., Matsumoto, K.: Gentzen method in modal calculi II. Osaka Math. J. 11, 115–120 (1959)
Parikh, R.: The completeness of propositional dynamic logic. Lecture Notes in Computer Science, vol. 64, pp. 403–415. Berlin-Heidelberg-New York: Springer 1978
Pratt, V.R.: Semantical considerations in Floyd-Hoare logic. Proceedings 17th IEEE Symposium on Foundations of Computer Science, pp. 109–121. 1976
Prawitz, D.: Comments on Gentzen-type procedures and the classical notion of truth. Lecture Notes in Mathematics vol. 500, pp. 290–319. Berlin-Heidelberg-New York: Springer 1975
Sato, M.: A study of Kripke-type models for some modal logics by Gentzen's sequential method. Publ. Res. Inst. Math. Sci. 13, 381–468 (1977)
Segerberg, K.: A completeness theorem in the modal logic of programs. Notices of the American Mathematical Society, 24, A-552 (1977)
Takeuti, G.: Proof theory. Amsterdam: North-Holland 1975
About this article
Cite this article
Nishimura, H. Sequential method in propositional dynamic logic. Acta Informatica 12, 377–400 (1979). https://doi.org/10.1007/BF00268322
- Operating System
- Data Structure
- Communication Network
- Information Theory
- Computational Mathematic