More on looping vs. repeating in dynamic logic (Q2265813)

Two types of divergence in computation are referred to in a paper of \textit{D. Harel} and \textit{V. R. Pratt} [5th ACM Symp. on Principles of Programming Languages, 203-213 (1978)] as global and local looping respectively. These notions give a repeat and loop constructs, whose expressive power has been investigated in different versions of dynamic logic. This paper shows that QDL, the first-order version of dynamic logic, is more expressive with repeat than with loop. The authors show also that the validity problems for formulas of the form \(\phi \supset \neg loop(\alpha)\) and \(\phi \supset \neg repeat(\alpha)\) are \(\Sigma^ 0_ 1\)-complete and \(\Pi^ 1_ 1\)-complete, respectively.