  Formulae of the Lambek calculus are constructed using three binary
connectives, multiplication and two divisions. We extend it using a unary
connective, positive Kleene iteration. For this new operation, following its
natural interpretation, we present two lines of calculi. The first one is a
fragment of infinitary action logic and includes an omega-rule for introducing
iteration to the antecedent. We also consider a version with infinite (but
finitely branching) derivations and prove equivalence of these two versions. In
Kleene algebras, this line of calculi corresponds to the *-continuous case. For
the second line, we restrict our infinite derivations to cyclic (regular) ones.
We show that this system is equivalent to a variant of action logic that
corresponds to general residuated Kleene algebras, not necessarily
*-continuous. Finally, we show that, in contrast with the case without division
operations (considered by Kozen), the first system is strictly stronger than
the second one. To prove this, we use a complexity argument. Namely, we show,
using methods of Buszkowski and Palka, that the first system is $\Pi_1^0$-hard,
and therefore is not recursively enumerable and cannot be described by a
calculus with finite derivations.
