Abstract

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.