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.
Read more about this topic: Dynamic Logic (modal Logic)