Premium
CUT ELIMINATION FOR PROPOSITIONAL DYNAMIC LOGIC WITHOUT
Author(s) -
Bull Robert A.
Publication year - 1992
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19920380107
Subject(s) - propositional calculus , propositional variable , axiom , mathematics , zeroth order logic , calculus (dental) , propositional formula , well formed formula , intermediate logic , autoepistemic logic , proof calculus , semantics (computer science) , natural deduction , discrete mathematics , algebra over a field , algorithm , computer science , programming language , description logic , pure mathematics , multimodal logic , medicine , geometry , dentistry
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.