Dynamic logic (modal logic)

In logic, philosophy, and theoretical computer science, dynamic logic is an extension of modal logic capable of encoding properties of computer programs.

A simple example of a statement in dynamic logic is

which states that if the ground is currently dry and it rains, then afterwards the ground will be wet.

The syntax of dynamic logic contains a language of propositions (like "the ground is dry") and a language of actions (like "it rains"). The core modal constructs are ${\displaystyle [a]p}$, which states that after performing action a the proposition p should hold, and ${\displaystyle \langle a\rangle p}$, which states that after performing action a it is possible that p holds. The action language supports operations ${\displaystyle a\mathbin {;} b}$ (doing one action followed by another), ${\displaystyle a\cup b}$ (doing one action or another), and iteration ${\displaystyle a{*}}$ (doing one action zero or more times). The proposition language supports Boolean operations (and, or, and not). The action logic is expressive enough to encode programs. For an arbitrary program ${\displaystyle P}$, precondition ${\displaystyle \varphi }$, and postcondition ${\displaystyle \varphi '}$, the dynamic logic statement ${\displaystyle \varphi \to [P]\varphi '}$ encodes the correctness of the program, making dynamic logic more general than Hoare logic.

Beyond its use in formal verification of programs, dynamic logic has been applied to describe complex behaviors arising in linguistics, philosophy, AI, and other fields.

Modal logic is characterized by the modal operators ${\displaystyle \Box p}$ (box p) asserting that ${\displaystyle p\,\!}$ is necessarily the case, and ${\displaystyle \Diamond p}$ (diamond p) asserting that ${\displaystyle p\,\!}$ is possibly the case. Dynamic logic extends this by associating to every action ${\displaystyle a\,\!}$ the modal operators ${\displaystyle [a]\,\!}$ and ${\displaystyle \langle a\rangle \,\!}$, thereby making it a multimodal logic. The meaning of ${\displaystyle [a]p\,\!}$ is that after performing action ${\displaystyle a\,\!}$ it is necessarily the case that ${\displaystyle p\,\!}$ holds, that is, ${\displaystyle a\,\!}$ must bring about ${\displaystyle p\,\!}$. The meaning of ${\displaystyle \langle a\rangle p\,\!}$ is that after performing ${\displaystyle a\,\!}$ it is possible that ${\displaystyle p\,\!}$ holds, that is, ${\displaystyle a\,\!}$ might bring about ${\displaystyle p\,\!}$. These operators dual to each other, which means they are related by ${\displaystyle [a]p\leftrightarrow \neg \langle a\rangle \neg p\,\!}$ and ${\displaystyle \langle a\rangle p\leftrightarrow \neg [a]\neg p\,\!}$, analogously to the relationship between the universal (${\displaystyle \forall \,\!}$) and existential (${\displaystyle \exists \,\!}$) quantifiers.

Dynamic logic permits compound actions built up from smaller actions. While the basic control operators of any programming language could be used for this purpose, Kleene's regular expression operators are a good match to modal logic. Given actions ${\displaystyle a\,\!}$ and ${\displaystyle b\,\!}$, the compound action ${\displaystyle a\cup b\,\!}$, choice, also written ${\displaystyle a+b\,\!}$ or ${\displaystyle a|b\,\!}$, is performed by performing one of ${\displaystyle a\,\!}$ or ${\displaystyle b\,\!}$. The compound action ${\displaystyle a{\mathbin {;}}b\,\!}$, sequence, is performed by performing first ${\displaystyle a\,\!}$ and then ${\displaystyle b\,\!}$. The compound action ${\displaystyle a{*}\,\!}$, iteration, is performed by performing ${\displaystyle a\,\!}$ zero or more times, sequentially. The constant action ${\displaystyle 0\,\!}$ or BLOCK does nothing and does not terminate, whereas the constant action ${\displaystyle 1\,\!}$ or SKIP or NOP, definable as ${\displaystyle 0{*}\,\!}$, does nothing but does terminate.

These operators can be axiomatized in dynamic logic as follows, taking as already given a suitable axiomatization of modal logic including such axioms for modal operators as the above-mentioned axiom ${\displaystyle [a]p\leftrightarrow \neg \langle a\rangle \neg p\,\!}$ and the two inference rules modus ponens (${\displaystyle \vdash p}$ and ${\displaystyle \vdash p\to q}$ implies ${\displaystyle \vdash q\,}$) and necessitation (${\displaystyle \vdash p}$ implies ${\displaystyle \vdash [a]p\,}$).