Abstract
We consider residuated semigroups, i.e., partially ordered semigroups with division operations, enriched with the positive iteration operation (
an analog of Kleene star, but with the non-emptiness condition). There are two ways for defining iteration: by induction and by *-continuity;
a standard example for the second approach is the powerset of the free semigroup a.k.a. the algebra of formal languages (without the empty word).
We show that the atomic inequational theories for these two approaches differ. Note that for the non-residuated case the situation is different: as shown by
Kozen, equational theories of Kleene algebras and the subclass of *-continuous Kleene algebras coincide. The proof is non-constructive and is based on
complexity considerations: we show that the calculus for the *-continuous case, which is the Lambek calculus extended with infinitary rules for the iteration,
has a \(\Pi_1^0\)-complete derivability problem (we show it using methods by Buszkowski and Palka), and for the inductive system we have a circular proof system,
which is definitely recursively enumerable. We also consider the Lambek calculus extended both with iteration and the (sub)exponential modality allowing the
contraction rule (in the non-local form) and show that the complexity there is at least \(\Pi_1^1\). Finally, we raise some open questions for future research,
both technical (probably easy to solve, like translating the results from semigroups with positive iteration to monoids with Kleene iteration etc.) and significant
(most importantly, completeness w.r.t. models on formal languages).