CUT ELIMINATION FOR PROPOSITIONAL DYNAMIC LOGIC WITHOUT

The aim of this paper is to extend the semantic analysis of tense logic in Rescher/Urquhart 3] to propositional dynamic logic without*. For this we develop a nested sequential calculus whose axioms and rules directly reflect the steps in the semantic analysis. It is shown that this calculus, with the cut rule omitted, is complete with respect to the standard semantics. It follows that cut elimination does hold for this nested sequential calculus. MSC: 03B45.