Propositional modal logic of programs has been introduced by Fischer and Ladner [1], following ideas of Pratt [4]. We shall call it propositional dynamic logic (PDL) following the terminology of Harel, Meyer and Pratt. In the following we prove the completeness of a rather natural set of axioms for this logic and for an extension of it obtained by allowing the inverse operation which converts a program into its inverse.

The following is a brief sketch of the plan of the proof. We introduce two auxiliary notions, that of pseudomodel and that of nonstandard model. Pseudomodels are highly syntactic objects and merely represent partial attempts to spell out a model. Thus an inconsistent formula may have a pseudomodel but every attempt to spell out the complete details of a model corresponding to the pseudomodel will, for an inconsistent formula, run into obstacles. A nonstandard model is like a model but we do …