Action Logic is Undecidable

Publication date 24 December 2019

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

o m e g a

-rule instead (infinitary action logic) Buszkowski and Palka (2007) have proved

P i_{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,

S i g m a_{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.

This page was built for publication: Action Logic is Undecidable

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6331740)