The article presents a calculus of syntactic types which differs from the calculi L and NL of J. Lambek in that, in its Gentzen-like form, sequent antecedents are neither strings nor phrase structures but functor-argument structures. The product-free part of the calculus is shown to be equivalent to the system AB due to Ajdukiewicz and Bar-Hillel. However, if the empty sequent antecedent is admitted, the resulting product-free calculus is not finitely cut-rule axiomatizable.

This paper studies the relation between some extensions of the non-associative Lambek Calculus NL and their interpretation in tree models (free groupoids). We give various examples of sequents that are valid in tree models, but not derivable in NL. We argue why tree models may not be axiomatizable if we add finitely many derivation rules to NL, and proceed to consider labeled calculi instead.We define two labeled categorial calculi, and prove soundness and completeness for interpretations that are almost the intended (...) one, namely for tree models where some branches of some trees may be resp. all branches of all trees must be infinitely extending. Extrapolating from the experiences in our quite simple systems, we briefly discuss some problems involved with the introduction of labels in categorial grammar, and argue that many of the basic questions are not yet understood. (shrink)