An arithmetical hierarchy in propositional dynamic logic (Q1119628)

Let \(\Sigma_ n^{PDL}\) and \(\Pi_ n^{PDL}\) denote the classes of formulas of propositional dynamic logic of the form \(<a_ 1>[a_ 2]<a_ 3>...\{a_ n\}p\) and \([a_ 1]<a_ 2>[a_ 3]...\{a_ n\}p\), respectively, where \(a_ i\) are modality-free programs, p is a modality- free formula and \(\{a_ n\}\) denotes \([a_ n]\) or \(<a_ n>\) depending on parity of n. It is shown that in some models \(\Sigma_ n^{PDL}\) and \(\Pi_ n^{PDL}\)-formulas define exactly the \(\Sigma^ 0_ n\) and \(\Pi^ 0_ n\)-sets of the Kleene-Mostowski hierarchy. It follows that alternation of modalities defines a strict hierarchy of PDL-formulas relative to their expressive power. Another corollary is the Berman- Paterson theorem: PDL with tests is strongly more expressive than PDL without tests. There are some inaccuracies in the proof but they are easily improvable.