  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$. The omega-rule-free derivations in Seq$_{\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 $\varphi_\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 $\varphi_\omega\left( 0\right)$ -- actually in the
corresponding primitive recursive weakening, $\mathbf{PRA}_{\varphi_{\omega
}\left( 0\right)}$.
