Commutative Action Logic

TL;DR

This paper establishes the undecidability and precise arithmetical hierarchy classification of commutative action logic and its infinitary variant, using encoding of counter machine computations.

Contribution

It provides the first complexity classification for commutative action logic, showing it is $\Sigma_1^0$-complete and $\Pi_1^0$-complete, similar to non-commutative cases, with novel encoding methods.

Findings

Commutative action logic is $\Sigma_1^0$-complete.

Infinitary commutative action logic is $\Pi_1^0$-complete.

Methods involve encoding infinite counter machine computations.

Abstract

We prove undecidability and pinpoint the place in the arithmetical hierarchy for commutative action logic, that is, the equational theory of commutative residuated Kleene lattices (action lattices), and infinitary commutative action logic, the equational theory of *-continuous action lattices. Namely, we prove that the former is $\Sigma_1^0$-complete and the latter is $\Pi_1^0$-complete. Thus, the situation is the same as in the more well-studied non-commutative case. The methods used, however, are different: we encode infinite and circular computations of counter (Minsky) machines.