Reasoning from hypotheses in *-continuous action lattices

TL;DR

This work analyzes the complexity of reasoning in $*$-continuous action lattices (residuated Kleene lattices) under restricted Horn-theoretic assumptions. By translating hypothesis-driven derivations into infinitary action logic with exponentiation and employing a dyadic focusing framework, the authors pin down exact complexity bounds: reasoning from $*$-free hypotheses (and from commutativity) is $\\Pi^0_1$-complete, while allowing monoidal inequations yields $\\Sigma^0_{\\omega^{\\omega}}$-complete. The results hinge on an ordinal/hyperarithmetical analysis up to $\\omega^{\\omega}$, and the approach extends Kozen’s program for Kleene algebras to the residuated (action lattice) setting. The findings reveal a sharp separation of complexity across fragments and establish a residuated counterpart to Kozen’s table, with implications for formal reasoning in substructural logics and related algebraic frameworks.

Abstract

The class of all $\ast$-continuous Kleene algebras, whose description includes an infinitary condition on the iteration operator, plays an important role in computer science. The complexity of reasoning in such algebras - ranging from the equational theory to the Horn one, with restricted fragments of the latter in between - was analyzed by Kozen (2002). This paper deals with similar problems for $\ast$-continuous residuated Kleene lattices, also called $\ast$-continuous action lattices, where the product operation is augmented by residuals. We prove that, in the presence of residuals, the fragment of the corresponding Horn theory with $\ast$-free hypotheses has the same complexity as the $ω^ω$ iteration of the halting problem, and hence is properly hyperarithmetical. We also prove that if only commutativity conditions are allowed as hypotheses, then the complexity drops down to $Π^0_1$ (i.e. the complement of the halting problem), which is the same as that for $\ast$-continuous Kleene algebras. In fact, we get stronger upper bound results: the fragments under consideration are translated into suitable fragments of infinitary action logic with exponentiation, and our upper bounds are obtained for the latter ones.

Theorems & Definitions (57)

• Definition 1.1
• Definition 1.2
• Definition 1.3
• Definition 1.4
• Definition 2.1
• Definition 2.2
• Theorem 2.3
• Theorem 2.4: see KuznetsovSperanski2022
• Corollary 2.5
• Theorem 2.6