Each sequent has a distinguished category formula (underlined) on which rule applications are keyed: In the regulated calculus there is no spurious ambiguity, and provided there is no explicit or implicit antecedent product, i.e., provided .L is not needed, F ~ A is a theorem of the Lambek calculus iff F ~ A is a theorem of the regulated calculus.
apart from the issue regarding .L, there is a general cause for dissatisfaction with this approach: it assumes the initial presence of the entire sequent to be proved, i.e., it is in principle nonincremental; on the other hand, allowing incrementality on the basis of Cut would reinstate with a vengeance the problem of spurious ambiguity, for then what are to be the Cut formulas?