Logic Without Structural Rules (Another Look at Cut Elimination)
Joachim Lambek · 1993
Abstract In [L 1958], Gentzen’s sequent calculus was extended from intuitionistic logic to what I then called the ‘syntactic calculus’, a form of bidirectional categorial grammar, now also seen to be the intuitionistic fragment of a non-symmetric version of Girard’s [1987] linear logic, and the cut-elimination theorem was proved in this generality. In [L 1969], this proof was lifted to the categorical level, where the sequents were interpreted as multilinear operations. Here we shall take another look at this proof and see that it becomes more transparent if in place of the operations we consider terms in an inductively defined language [L 1989].