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 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 .
Read more about this topic: Dynamic Logic (modal Logic)
Famous quotes containing the word axioms:
““I tell you the solemn truth that the doctrine of the Trinity is not so difficult to accept for a working proposition as any one of the axioms of physics.””
—Henry Brooks Adams (1838–1918)
“The axioms of physics translate the laws of ethics. Thus, “the whole is greater than its part;” “reaction is equal to action;” “the smallest weight may be made to lift the greatest, the difference of weight being compensated by time;” and many the like propositions, which have an ethical as well as physical sense. These propositions have a much more extensive and universal sense when applied to human life, than when confined to technical use.”
—Ralph Waldo Emerson (1803–1882)