© 1997 by Oxford University Press
Nonrepresentable sequential algebras
Department of Mathematics and Applied Mathematics, University of Cape Town, 7700 Rondebosch, South Africa. Email: pjipsen@maths.uct.ac.za A1 Department of Mathematics, 400 Carver Hall, Iowa State University, Ames, Iowa 50011-2066, USA. Email: maddux@iastate.edu
The sequential calculus of von Karger and Hoare is designed for reasoning about sequential phenomena, dynamic or temporal logic, and concurrent or reactive systems. Unlike the classical calculus of relations, it has no operation for forming the converse of a relation. Sequential algebras are algebras that satisfy certain equations in the sequential calculus. One standard example of a sequential algebra is the set of relations included in a partial ordering. Nonstandard examples arise by relativizing relations algebras to elements that are antisymmetric, transitive, and reflexive. The incompleteness and non-finite-axiomatizability of the sequential calculus are examined here from a relation-algebraic point of view. New constructions of nonrepresentable relation algebras are used to prove that there is no finite axiomatization of the equational theory of antisymmetric dense locally linear sequential algebras. The constructions improve on previous examples in certain interesting respects and give yet another proof that the classical calculus of relations is not finitely axiomatizable.