Sequential method in propositional dynamic logic

Summary 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.