Propositional dynamic logic (PDL) is tailored to modeling and reasoning about evolving universes, such as computer programs whose states change during their execution. It is based on modal operators, such as in the formula [P]F, which states that by execution of program P, a state is constructed in which formula F holds. Thus, dynamic logic involves two kinds of syntactic phrases, programs and formulas, which are mutually recursively related.

This paper proposes sequential dynamic logic (SDL) as a simpler alternative. The core idea is to return to formulas as the only kind of syntactic phrases: rather than extending the syntax of classical logic by modal operators, the semantics of connectives is generalized to capture both static propositions and dynamic transitions. In particular, the implication F1 => F2 states that after (the transition described by) formula F1, a state is reached in which (the condition described by) formula F2 holds. With bi-directional translation, it is shown that SDL is as expressive as PDL without iteration. For a correspondingly defined sequent calculus, completeness is proved. Finally, SDL is extended by an iteration connective (which makes it as expressive as full PDL) and completeness for finite models is shown.

The paper provides an interesting new perspective on the field, showing that the naive natural language interpretation of connectives (implication as “if-then”) can be formalized in such a way that connectives describe dynamic relationships as precisely as modal operators. The resulting formalism is elegant and provides big potential for further developments.