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 , which states that after performing action a the proposition p should hold, and , which states that after performing action a it is possible that p holds. The action language supports operations (doing one action followed by another), (doing one action or another), and iteration (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 , precondition , and postcondition , the dynamic logic statement 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.
Language
Modal logic is characterized by the modal operators (box p) asserting that is necessarily the case, and (diamond p) asserting that is possibly the case. Dynamic logic extends this by associating to every action the modal operators and , thereby making it a multimodal logic. The meaning of is that after performing action it is necessarily the case that holds, that is, must bring about . The meaning of is that after performing it is possible that holds, that is, might bring about . These operators are dual to each other, which means they are related by and , analogously to the relationship between the universal () and existential () 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 and , the compound action , choice, also written or , is performed by performing one of or . The compound action , sequence, is performed by performing first and then . The compound action , iteration, is performed by performing zero or more times, sequentially. The constant action or BLOCK does nothing and does not terminate, whereas the constant action or SKIP or NOP, definable as , does nothing but does terminate.
Axioms
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 and the two inference rules modus ponens ( and implies ) and necessitation ( implies ).
A1.
A2.
A3.
A4.
A5.
A6.
Axiom A1 makes the empty promise that when BLOCK terminates, will hold, even if is the proposition false. (Thus BLOCK abstracts the essence of the action of hell freezing over.) A2 says that NOP acts as the identity function on propositions, that is, it transforms into itself. A3 says that if doing one of or must bring about , then must bring about and likewise for , and conversely. A4 says that if doing and then must bring about , then must bring about a situation in which must bring about . A5 is the evident result of applying A2, A3 and A4 to the equation of Kleene algebra. A6 asserts that if holds now, and no matter how often we perform it remains the case that the truth of after that performance entails its truth after one more performance of , then must remain true no matter how often we perform . A6 is recognizable as mathematical induction with the action n := n+1 of incrementing n generalized to arbitrary actions .
Derivations
The modal logic axiom permits the derivation of the following six theorems corresponding to the above:
T1.
T2.
T3.
T4.
T5.
T6.
T1 asserts the impossibility of bringing anything about by performing BLOCK. T2 notes again that NOP changes nothing, bearing in mind that NOP is both deterministic and terminating whence and have the same force. T3 says that if the choice of or could bring about , then either or alone could bring about . T4 is just like A4. T5 is explained as for A5. T6 asserts that if it is possible to bring about by performing sufficiently often, then either is true now or it is possible to perform repeatedly to bring about a situation where is (still) false but one more performance of could bring about .
Box and diamond are entirely symmetric with regard to which one takes as primitive. An alternative axiomatization would have been to take the theorems T1–T6 as axioms, from which we could then have derived A1–A6 as theorems.
The difference between implication and inference is the same in dynamic logic as in any other logic: whereas the implication asserts that if is true then so is , the inference asserts that if is valid then so is . However the dynamic nature of dynamic logic moves this distinction out of the realm of abstract axiomatics into the common-sense experience of situations in flux. The inference rule , for example, is sound because its premise asserts that holds at all times, whence no matter where might take us, will be true there. The implication is not valid, however, because the truth of at the present moment is no guarantee of its truth after performing . For example, will be true in any situation where is false, or in any situation where is true, but the assertion is false in any situation where has value 1, and therefore is not valid.
Derived rules of inference
As for modal logic, the inference rules modus ponens and necessitation suffice also for dynamic logic as the only primitive rules it needs, as noted above. However, as usual in logic, many more rules can be derived from these with the help of the axioms. 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. Writing for the action of kicking the TV, and for the proposition that the TV is broken, dynamic logic expresses this inference as , having as premise and as conclusion . The meaning of is that it is guaranteed that after kicking the TV, it is broken. Hence the premise means that if the TV is broken, then after kicking it once it will still be broken. denotes the action of kicking the TV zero or more times. Hence the conclusion means that if the TV is broken, then after kicking it zero or more times it will still be broken. For if not, then after the second-to-last kick the TV would be in a state where kicking it once more would fix it, which the premise claims can never happen under any circumstances.
The inference is sound. However the implication is not valid because we can easily find situations in which holds but does not. In any such counterexample situation, must hold but must be false, while however must be true. But this could happen in any situation where the TV is broken but can be revived with two kicks. The implication fails (is not valid) because it only requires that hold now, whereas the inference succeeds (is sound) because it requires that hold in all situations, not just the present one.
An example of a valid implication is the proposition . This says that if is greater or equal to 3, then after incrementing , must be greater or equal to 4. In the case of deterministic actions that are guaranteed to terminate, such as , must and might have the same force, that is, and have the same meaning. Hence the above proposition is equivalent to asserting that if is greater or equal to 3 then after performing , might be greater or equal to 4.
Assignment
The general form of an assignment statement is where is a variable and is an expression built from constants and variables with whatever operations are provided by the language, such as addition and multiplication. The Hoare axiom for assignment is not given as a single axiom but rather as an axiom schema.
A7.
This is a schema in the sense that can be instantiated with any formula containing zero or more instances of a variable . The meaning of is with those occurrences of that occur free in , i.e. not bound by some quantifier as in , replaced by . For example, we may instantiate A7 with , or with . Such an axiom schema allows infinitely many axioms having a common form to be written as a finite expression connoting that form.
The instance of A7 allows us to calculate mechanically that the example encountered a few paragraphs ago is equivalent to , which in turn is equivalent to by elementary algebra.
An example illustrating assignment in combination with is the proposition . This asserts that it is possible, by incrementing sufficiently often, to make equal to 7. This of course is not always true, e.g. if is 8 to begin with, or 6.5, whence this proposition is not a theorem of dynamic logic. If is of type integer however, then this proposition is true if and only if is at most 7 to begin with, that is, it is just a roundabout way of saying .
Mathematical induction can be obtained as the instance of A6 in which the proposition is instantiated as , the action as , and as . The first two of these three instantiations are straightforward, converting A6 to . However, the ostensibly simple substitution of for is not so simple as it brings out the so-called referential opacity of modal logic in the case when a modality can interfere with a substitution.
When we substituted for , we were thinking of the proposition symbol as a rigid designator with respect to the modality , meaning that it is the same proposition after incrementing as before, even though incrementing may impact its truth. Likewise, the action is still the same action after incrementing , even though incrementing will result in its executing in a different environment. However, itself is not a rigid designator with respect to the modality ; if it denotes 3 before incrementing , it denotes 4 after. So we can't just substitute for everywhere in A6.
One way of dealing with the opacity of modalities is to eliminate them. To this end, expand as the infinite conjunction , that is, the conjunction over all of . Now apply A4 to turn into , having modalities. Then apply Hoare's axiom times to this to produce , then simplify this infinite conjunction to . This whole reduction should be applied to both instances of in A6, yielding . The remaining modality can now be eliminated with one more use of Hoare's axiom to give .
With the opaque modalities now out of the way, we can safely substitute for in the usual manner of first-order logic to obtain Peano's celebrated axiom , namely mathematical induction.