Predicative proof theory of PDL and basic applications

Lev Gordeev

Propositional dynamic logic (PDL) is presented in Schütte-style mode as one-sided semiformal tree-like sequent calculus Seq${}_{\omega }^{\text{pdl}}$ with standard cut rule and the omega-ru…