On Action Logic: Equational Theories of Action Algebras

Pratt (1991, Proceedings of JELIA’90, Volume 478, pp.97–120) defines action algebras as Kleene algebras withresiduals and action logic as the equational theory of actionalgebras. In contrast to Kleene algebras, action algebras forma (finitely based) variety. Jipsen (2004, Studia Logica, 76,291–303) proposes a Gentzen-style sequent system for actionlogic but leaves it as an open question if this system admitscut-elimination and if action logic is decidable. We show thatJipsen's system does not admit cut-elimination. We prove thatthe equational theory of *-continuous action algebras and thesimple Horn theory of *-continuous Kleene algebras are not recursivelyenumerable and they possess FMP, but action logic does not possessFMP.