Action Logic is Undecidable

TL;DR

This paper proves that the core action logic, involving residuated Kleene lattices, is undecidable, settling an open question and establishing its precise computational complexity as  0complete.

Contribution

It demonstrates that action logic is undecidable and determines its exact complexity class,  0complete, also extending results to related logics and fragments.

Findings

Action logic is  0complete.

Decidability of action logic is refuted.

Complexity results apply to related and extended logics.

Abstract

Action logic is the algebraic logic (inequational theory) of residuated Kleene lattices. This logic involves Kleene star, axiomatized by an induction scheme. For a stronger system which uses an $\omega$-rule instead (infinitary action logic) Buszkowski and Palka (2007) have proved $\Pi_1^0$-completeness (thus, undecidability). Decidability of action logic itself was an open question, raised by D. Kozen in 1994. In this article, we show that it is undecidable, more precisely, $\Sigma_1^0$-complete. We also prove the same complexity results for all recursively enumerable logics between action logic and infinitary action logic; for fragments of those only one of the two lattice (additive) connectives; for action logic extended with the law of distributivity.