Dynamic Logic (modal Logic) - Assignment

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.

One subtlety we glossed over here is that should be understood as ranging over the natural numbers, where is the superscript in the expansion of as the union of over all natural numbers . 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. As a case in point, if is a real variable and is the predicate is a natural number, then axiom A6 after the first two substitutions, that is, is just as valid, that is, true in every state regardless of the value of in that state, as when is of type natural number. If in a given state is a natural number, then the antecedent of the main implication of A6 holds, but then is also a natural number so the consequent also holds. If is not a natural number, then the antecedent is false and so A6 remains true regardless of the truth of the consequent. We could strengthen A6 to an equivalence without impacting any of this, the other direction being provable from A5, from which we see that if the antecedent of A6 does happen to be false somewhere, then the consequent must be false.