A syntactic calculus for a categorial type language is a deductive system producing statements of the form A ⊢ B (‘B is derivable from A’).  A statement A ⊢ B holds in a model (‘M ⊨ A ⊢ B’) if V(A) ⊆ V(B); it is valid (‘⊨ A ⊢ B’) if it holds in all models. For the minimal grammar logic, the set of derivations in the syntactic calculus is freely generated from the axiom and rules of inference below. This minimal system, for historical reasons, is known as NL (for ‘Non-associative Lambek calculus’).  The first line states that derivability is a reflexive, transitive relation, i.e., a preorder.  The bidirectional (‘if and only if’) inference rules of the second line characterize the product and division operations as a residuated triple as it is known in residuation theory. (Galatos et al. 2007 provides good background reading.) The syntactic calculus, so defined, precisely fits the intended interpretation of the type language, in the sense of the soundness and completeness result below.