We propose a method to axiomatize by equations the least prefixed point of an order preserving function. We discuss its domain of application and show that the Boolean modal μ-calculus has a complete equational axiomatization. The method relies on the existence of a “closed structure” and its relationship to the equational axiomatization of Action Logic is made explicit. The implication operation of a closed structure is not monotonic in one of its variables; we show that the existence of such a term that does not preserve the order is an essential condition for defining by equations the least prefixed point. We stress the interplay between closed structures and fixed point operators by showing that the theory of Boolean modal μ-algebras is not a conservative extension of the theory of modal μ-algebras. The latter is shown to lack the finite model property.
Theoretical Computer Science, 2003, Vol 295, Issue 1, p. 341-371
Semantics and logics of programs; Least fixed point; Fixed point calculi; Temporal logic