ИСТИНА

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 Π⁰₁-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 Π¹₁. 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).