Given the universal freely generated syntactic calculus discussed above, the task of providing a categorial grammar for a particular language is reduced to specifying its lexicon: the typelogical framework, in this sense, represents the culminating point of ‘lexicalizing’ grammar formalisms.  A categorial lexicon is a relation associating each word with a finite number of types.  Given a lexicon Lex, a categorial grammar assigns type B to a string of words w1 ···  wn iff for 1 ≤ i ≤ n, (wi,Ai) ∈ Lex, and X ⊢ B is provable in the syntactic calculus where X is a product formula with yield A1 ··· An. The grammar can be considered adequate if the strings w1 ··· wn are indeed judged to be the wellformed phrases of type B.