Defining logics and refining structures: on type reduction systems underlying categorial grammars
Maciej Kandulski (Adam Mickiewicz University, Poznań)
The term categorial grammar (CG) was associated with a system introduced by Ajdukiewicz in  for many years. Ajdukiewicz proposed to divide a vocabulary into classes containing words playing the same syntactic role in a language and associate with each class a formal index called a type. The solution of the problem of syntactic coherence of a string of words was then reduced to execution of a sequence of transformations of a string of types according to a rule called a cancellation scheme. The procedure had to result in assigning to the string a single type which establishes the syntactic role of the string as a whole. A rather uncomplicated form of cancellation schemes as well as the fact that Ajdukiewicz grammars turned out to generate precisely the class of CF-languages, cf. , established the opinion that they are rather a variant of CF-grammars. A logician or a logically-oriented grammarian however could observe that cancellation schemes x/y x → x and y y\x → x are in fact directional versions of familiar modus ponens rule in Hilbert-style axiomatizations of logical systems, or of the rule of elimination of implication in their another, natural deduction setting. The désintéressement concerning CGs remained unchanged even after introducing by Lambek  a calculus extending that of Ajdukiewicz by (directional) rules of introduction of implication, thus bringing the grammars even more to logic: Chomsky conjectured that Lambek grammars still do not go beyond CF-languages (the authors of  even announced the proof of the fact) and formal linguists placed their interests in other generating systems. Chomsky’s conjecture turned out much difficult to prove than the authors of  probably could suspect and it took more than thirty years to present a correct proof (Pentus ). In this period however the nature of systems of logic underlying categorical grammars was examined and their usefulness in linguistics was well established. Right now, known also as type logical grammars, they offer to linguists a flexible and formally rigid tool to analyze both syntactic and semantic phenomena in natural languages, being on the other hand an object of formal investigations as well.
Any formal system which aims at a description of linguistic
phenomena must be able to reflect the material rather then ideal status
of linguistic objects such as words, phrases, trees, or others. Those
objects in general can not be freely multiplicated, deleted or
permuted, and if they are, such operations must be performed in a
controlled rather than global way. Traditional logic, examining
properties of true and false statements, makes use of three structural
rules of weakening, contraction and permutation. Systems of logic
underlying CGs do not employ the whole collection of structural rules
and belong thus to the class of so-called substructural logics. A
selection of structural rules in CGs induces a structure on the string
of types, therefore also on the strings of words, turning them into
phrase structures (trees) or product-functorial structures. The
formalism of CGs can be further refined by using modal operators which,
if used in types assigned to vocabulary items, allow licensed access to
structural rules. Syntactic phenomena such as coordination, right/left
node raising, relative clause constructions can be handled within the
framework of CGs, cf. . Logical and computational properties of
categorial grammars over different type reduction systems (i.e.
employing different systems of logic) as well as properties of
reduction system themselves are also examined. The most important
issues in this area of research, see the survey , are
axiomatizability and decidability problems, generative power (both in
the scope of string and tree languages) and relations to other
language-generating formalisms, model-theoretical investigations and
 Ajdukiewicz Kazimierz : Die syntaktische Konnexität. Studia Philosophica 1(1935), 1-27.
 Bar-Hillel Yehoshua, C. Gaifman, and E. Shamir: On categorical and phrase structure grammars. Bulletin of the Research Council of Israel F(9) (1960), 1-16.
 Buszkowski Wojciech: Mathematical linguistics and proof theory. [In:] Johan van Benthem and A. ter Meulen (eds.): Handbook of Logic and Language. Elsevier, MIT Press 1997, 683-736.
 Lambek Joachim: The mathematics of sentence structure. American Mathematical Monthly 65 (1958), 154-170.
Moortgat Michael: Categorial type logics. [In:] Johan van Benthem and A. ter Meulen (eds.): Handbook of Logic and Language. Elsevier, MIT Press 1997, 93-178.
 Pentus Mati: Lambek grammars are context-free. [In:] Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science, Montreal 1993.