Given that there is quite a lot of vocabulary which is introduced
throughout the different sections of this tutorial, this section lists
the different terms and their alternatives.
L is short for Lambek's syntactic calculus (Lambek 1958), also called the
Lambek calculus. Lambek added the right rules for the implications to
AB and proved basic results like cut elimination and decidability for
the calculus.
Linear logic is a logic discovered by Girard (1987). It rejects global use of the rules of contraction and weakening and is therefore more suited than classical logic for dealing with resources. Lambek calculi can be seen as even more restricted in their resource management than linear logic in that global use of the commutativity (and associativity in the case of NL) are rejected as well.
The term par comes from linear logic where it is the multiplicative disjunction. Therefore, par links in proof structures correspond to a type of logical or. For example, the par links for NL are the product link for formulas A • B when it occurs in a negative position (as a hypothesis) and the links for the implications when they occur in positive (conclusion) positions. Using the definition of implication in terms of disjunction and negation and the de Morgan rule for the distribution of negation over conjunction, we see that both these cases correspond to a logical or as follows.