Kleene algebra with commutativity conditions is undecidable

TL;DR

This paper proves that the equational theory of Kleene algebra with added commutativity conditions is undecidable, resolving a longstanding open problem and extending previous results to weaker theories without induction axioms.

Contribution

It establishes the undecidability of Kleene algebra with commutativity conditions, even for theories lacking induction axioms, thus settling a major open question.

Findings

Decidability of Kleene algebra with commutativity conditions is false.

Results hold for weaker theories without induction axioms.

Complements recent independent proofs by Kuznetsov.

Abstract

We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in the theory of Kleene algebra. While this question has also been recently solved independently by Kuznetsov, our results hold even for weaker theories that do not support the induction axioms of Kleene algebra.