a*. Defining a to be reflexive when 1 ≤ a and transitive when a•a ≤ a by abstraction from binary relations, the first two of those equations force a* to be reflexive and transitive while the third forces a* to be greater or equal to a. The next axiom asserts that star is monotone. The last axiom can be written equivalently as a•(a → a)* ≤ a, a form which makes its role as induction more apparent. These two axioms in conjunction with the axioms for a residuated semilattice force a* to be the least reflexive transitive element of the semilattice of elements greater or equal to a. Taking that as the definition of reflexive transitive closure of a, we then have that for every element a of any action algebra, a* is the reflexive transitive closure of a. Properties The equational theory of the implication-free fragment of action algebras, those equations not containing → or ←, can be shown to coincide with the equational theory of Kleene algebras, also known as the regular expression equations. In that sense the above axioms constitute a finite axiomatization of regular expressions. Redko showed in 1967 that the regular expression equations had no finite axiomatization, for which John Horton Conway gave a shorter proof in 1971. Arto Salomaa gave an equation schema axiomatizing this theory which Dexter Kozen subsequently reformulated as a finite axiomatization using quasiequations, or implications between equations, the crucial quasiequations being those of induction: if x•a ≤ x then x•a* ≤ x, and if a•x ≤ x then a*•x ≤ x. Kozen defined a Kleene algebra to be any model of this finite axiomatization. Conway showed that the equational theory of regular expressions admit models in which a* was not the reflexive transitive closure of a, by giving a four-element model 0 ≤ 1 ≤ a ≤ a* in which a•a = a. In Conway's model, a is reflexive and transitive, whence its reflexive transitive closure should be a. However the regular expressions do not enforce this, allowing a* to be strictly greater than a. Such anomalous behavior is not possible in an action algebra, which forces a* to be the least transitive reflexive element. Examples Any Heyting algebra (and hence any Boolean algebra) is made an action algebra by taking • to be ∧ and a* = 1. This is necessary and sufficient for star because the top element