Predicative proof theory of PDL and basic applications

Propositional dynamic logic (PDL) is presented in Sch"{u}tte-style mode as one-sided semiformal tree-like sequent calculus Seq${}_{\omega }^{\text{pdl}}$ with standard cut rule and the omega-rule with principal formulas $\left[ P^{\ast }\right] !A$\mathrm{.}Theomega-rule-freederivationsinSeq${\omega }^{$\text{pdl}$}$ are finite (trees) and sequents deducible by these finite derivations are valid in PDL. Moreover the cut-elimination theorem for Seq${}_{\omega }^{\text{pdl}}$ is provable in Peano Arithmetic (PA)extended by transfinite induction up to Veblen’s ordinal ${\phi }_{\omega }\left(0\right)$. Hence (by the cutfree subformula property) such predicative extension of PA proves that any given $\left[P^{\ast }\right]$-free sequent is valid in PDL iff it is deducible in Seq${}_{\omega }^{\text{pdl}}$ by a finite cut- and omega-rule-free derivation, while PDL-validity of arbitrary star-free sequents is decidable in polynomial space. The former also implies standard Herbrand-style conclusions, which eventually leads to PSPACE-decidability of PDL-validity of $S$, provided that $P$ is atomic and $A$ is in a suitable \emph{basic conjunctive normal form}. Furthermore we consider star-free formulas $A$ in dual \emph{basic disjunctive normal form}, and corresponding expansions $S=\left\langle P^{\ast }\right\rangle !A\vee Z$ whose PDL-validity problem is known to be EXPTIME-complete. We show that cutfree-derivability in Seq${}_{\omega }^{\text{pdl}}$ (hence PDL-validity) of such $S$\ is equivalent to plain validity of a suitable “transparent” quantified boolean formula $\widehat{S}$. The whole proof can be formalized in PA extended by transfinite induction along ${\phi }_{\omega }\left(0\right)$ – actually in the corresponding primitive recursive weakening, $$\mathbf{P}\mathbf{R}\mathbf{A}${\varphi_{\omega }\left( 0\right)}$.