Action Logic is Undecidable

2019/12/24 by Kuznetsov, Stepan · 1 citation
#F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #I.2.3 #Logic (math.LO) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1912.11273

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 ω-rule instead (infinitary action logic) Buszkowski and Palka (2007) have proved Π₁⁰-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, Σ₁⁰-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.

Cited by

• Undecidability of theories of semirings with fixed points

Related

• Commutative Action Logic
• Infinitary Action Logic with Exponentiation
• Algebraic Proof Theory for Infinitary Action Logic
• Reasoning from hypotheses in *-continuous action lattices
• Logics for Epistemic Actions: Completeness, Decidability, Expressivity