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.