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.
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
Axiom A1 makes the empty promise that when BLOCK terminates,
(Thus BLOCK abstracts the essence of the action of hell freezing over.)
An example instance of such a derived rule in dynamic logic is that if kicking a broken TV once can't possibly fix it, then repeatedly kicking it can't possibly fix it either.
for the proposition that the TV is broken, dynamic logic expresses this inference as
But this could happen in any situation where the TV is broken but can be revived with two kicks.
is an expression built from constants and variables with whatever operations are provided by the language, such as addition and multiplication.
in the usual manner of first-order logic to obtain Peano's celebrated axiom
The importance of keeping this typing information straight becomes apparent if
had been of type integer, or even real, for any of which A6 is perfectly valid as an axiom.
is a natural number, then the antecedent of the main implication of A6 holds, but then
is not a natural number, then the antecedent is false and so A6 remains true regardless of the truth of the consequent.
acts as a NOP, changing nothing while allowing the action to move on.
is true the performer of the action can only take the left branch, and when
Dijkstra claimed to show the impossibility of a program that sets the value of variable
can be set to an arbitrary positive integer with the dynamic logic program
Hence we must either reject Dijkstra's argument or hold that the * operator is not effective.
Modal logic is most commonly interpreted in terms of possible world semantics or Kripke structures.
This semantics carries over naturally to dynamic logic by interpreting worlds as states of a computer in the application to program verification, or states of our environment in applications to linguistics, AI, etc.
One role for possible world semantics is to formalize the intuitive notions of truth and validity, which in turn permit the notions of soundness and completeness to be defined for axiom systems.
Ordinary or first-order logic has two types of terms, respectively assertions and data.
As can be seen from the examples above, dynamic logic adds a third type of term denoting actions.
PDL blends the ideas behind propositional logic and dynamic logic by adding actions while omitting data; hence the terms of PDL are actions and propositions.
Fischer and Ladner showed in their 1977 paper that PDL satisfiability was of computational complexity at most nondeterministic exponential time, and at least deterministic exponential time in the worst case.
This gap was closed in 1978 by Vaughan Pratt who showed that PDL was decidable in deterministic exponential time.
Dynamic logic was developed by Vaughan Pratt in 1974 in notes for a class on program verification as an approach to assigning meaning to Hoare logic by expressing the Hoare formula
By this Pnueli meant that temporal logic assertions are interpreted within a universal behavioral framework in which a single global situation changes with the passage of time, whereas the assertions of the other logics are made externally to the multiple actions about which they speak.
The advantage of the endogenous approach is that it makes no fundamental assumptions about what causes what as the environment changes with time.
The simplicity of this approach to concurrency has resulted in temporal logic being the modal logic of choice for reasoning about concurrent systems with its aspects of synchronization, interference, independence, deadlock, livelock, fairness, etc.