Cut. Specifically, given a context-free grammar as above, define a categorial grammar where , and . Let there be an axiom for every symbol , an axiom for every production rule , a lexicon entry for every terminal symbol , and Cut for the only rule. This categorial grammar generates the same language as the given CFG. Of course, this is not a basic categorial grammar, since it has special axioms that depend upon the language; i.e. it is not lexicalized. Also, it makes no use at all of non-primitive types. To show that any context-free language can be generated by a basic categorial grammar, recall that any context-free language can be generated by a context-free grammar in Greibach normal form. The grammar is in Greibach normal form if every production rule is of the form , where capital letters are variables, , and , that is, the right side of the production is a single terminal symbol followed by zero or more (non-terminal) variables. Now given a CFG in Greibach normal form, define a basic categorial grammar with a primitive type for each non-terminal variable , and with an entry in the lexicon , for each production rule . It is fairly easy to see that this basic categorial grammar generates the same language as the original CFG. Note that the lexicon of this grammar will generally assign multiple types to each symbol. The same construction works for Lambek grammars, since they are an extension of basic categorial grammars. It is necessary to verify that the extra inference rules do not change the generated language. This can be done and shows that every context-free language is generated by some Lambek grammar. To show the converse, that every language generated by a Lambek grammar is context-free, is much more difficult. It was an open problem for nearly thirty years, from the early 1960s until about 1991 when it was proven by Pentus. The basic idea is, given a Lambek grammar, construct a context-free grammar with the same set of terminal symbols, the same start symbol, with variables some (not all) types , and with a production rule for each entry in the lexicon, and production rules for certain sequents that are derivable in the Lambek calculus. Of course, there are infinitely many types and infinitely many derivable sequents, so in order to make a finite grammar it is necessary put