More About The Axiomatics Of The Lambek Calculus
Wojciech Zielonka · 1997
In Zielonka (1981) and (1989), I have found an axiomatics for the product-free calculus L of Lambek whose only rule is the cut rule. Following Buszkowski (1987), we shall call such an axiomatics linear. It has been proved that there is no finite axiomatics of that kind. In Lambek's original version of the calculus (cf. Lambek 1958), sequent antecedents are nonempty. By dropping this restriction, we obtain the variant L0 of L. This modification, introduced in the early 1980's, (see, e. g., Buszkowski 1985) and Zielonka 1981a), did not gain much popularity initially; a more common use of Lo has only occurred within the last few years (cf. Roorda 1991, p. 29). In (1988), I have established analogous results for the restriction of Lo to formulas without left (or, equivalently, right) division. Here, I present a similar (cut-rule) axiomatics for the whole of L0.