Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Sequential method in propositional dynamic logic

  • 61 Accesses

  • 23 Citations


Recently prepositional modal logic of programs, called ‘prepositional dynamic logic’, has been developed by many authors, following the ideas of Fisher and Ladner [1] and Pratt [12]. 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 [4], Parikh [11] or Segerberg [15]. 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 [11]. 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.


  1. 1.

    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

  2. 2.

    Gentzen, G.: Untersuchungen über das logische Schliessen I and II. Math. Z. 39, 176–210 and 405–431 (1935)

  3. 3.

    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

  4. 4.

    Harel, D.: Logics of programs: Axiomatics and descriptive power. MIT, ph.D.thesis, May 1978

  5. 5.

    Hughes, G.E., Cresswell, M.J.: An introduction to modal logic. London: Methuen 1968

  6. 6.

    Manna, Z.: Mathematical theory of computation. New York: McGraw-Hill 1974

  7. 7.

    Monk, D.: Mathematical logic. Berlin-Heidelberg-New York: Springer 1976

  8. 8.

    Nishimura, H.: A study of some tense logics by Gentzen's sequential method. forthcoming in Publ. R.I.M.S.

  9. 9.

    Ohnishi, M., Matsumoto, K.: Gentzen method in modal calculi I. Osaka Math. J. 9, 113–130 (1957)

  10. 10.

    Ohnishi, M., Matsumoto, K.: Gentzen method in modal calculi II. Osaka Math. J. 11, 115–120 (1959)

  11. 11.

    Parikh, R.: The completeness of propositional dynamic logic. Lecture Notes in Computer Science, vol. 64, pp. 403–415. Berlin-Heidelberg-New York: Springer 1978

  12. 12.

    Pratt, V.R.: Semantical considerations in Floyd-Hoare logic. Proceedings 17th IEEE Symposium on Foundations of Computer Science, pp. 109–121. 1976

  13. 13.

    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

  14. 14.

    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)

  15. 15.

    Segerberg, K.: A completeness theorem in the modal logic of programs. Notices of the American Mathematical Society, 24, A-552 (1977)

  16. 16.

    Takeuti, G.: Proof theory. Amsterdam: North-Holland 1975

Download references

Author information

Rights and permissions

Reprints and Permissions

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

Download citation


  • Operating System
  • Data Structure
  • Communication Network
  • Information Theory
  • Computational Mathematic