Wojciech Buszkowski Comments

on the paper “The Cut-Elimination Theorem for the Second Order Lambek Calculus”, by Martin Emms and Hans Leiss.

The paper is concerned with the product-free Lambek Calculus extended by propositional quantification. Systems of that kind are not typical in logical literature: their genealogy goes back to protothetic of Stanislaw Lesniewski. There are also interesting results of D. Gabbay (quoted by the authors) establishing undecidability of intuitionistic logic with propositional quantification. Several problems for the Lambek Calculus with Unification and Unification Categorial Grammar (see van Benthem (1991 )) can be translated into derivability problems in the authors’ system, but the two versions of the Lambek Calculus are not the same.

The authors’ main result is a Cut-Elimination Theorem for their system (actually, for several, slightly different versions of this system). And here I have some critical remarks at the very beginning. The authors’ proof is long and sophisticated, because they want to obtain lemmas 2 and 3 (p. 8) which yield a bound for the size of cut-free derivations (understood as the number of nodes in the derivation). It is not the case that they really need these size bound lemmas to get cut-elimination, as they try to persuade the reader on pp. 4-5. As a matter of fact, cut-elimination can be proven quite easily by induction on pairs (m, n) arranged in the lexicographic ordering, where m is the number of nodes in the cut-free derivation of the left premise of the cut-rule, and n means the same for the right premise. Then, one need not know substitution preserve size of derivations, since the size of the derivation of the right premise does not count for the crucial case. Of course, the latter induction is a bit less constructive than the authors’ one, hence they also obtain a stronger result: not merely cut-elimination, but a clear bound for the size of cut-free derivations (depending on the size of an original derivation with cuts). I would like to see a clear explanation of that in the Introduction (and even the abstract should stress the matter of size).

I see no problems with extending the main result to richer systems, as e.g. the Lambek Calculus with Product or with Booleans, etc. I suggest at least a guide in this direction should appear in the paper.

I have also objections to the authors’ justification of their research. On p. 3 they justify the need of cut-elimination by referring to “categorisation” which means the terminal type assignment procedure for categorial grammars. Now, their description of this procedure does not agree with its standard definition. Categorial grammars are “lexical” grammars in the sense that the total grammatical information characteristic of the particular language is stored in the initial type assignment, hence the terminal type assignment is defined, as follows: a string v_{1} … v_{n} is assigned a type a, if there are types a_{1}, …, a_{n} initially assigned to atoms v_{1}, …, v_{n}, respectively, such that the sequent a_{1} … a_{n} → a is derivable in the system of the grammar. Instead, the authors assume the initial type can be transformed into other types by the system, and then the latter take the part of the former ones in the derivable sequent, which is nonstandard (and introduces the cut-rule through “back door”). According to the standard definition, “categorisation” always reduces to the derivability in the system, no matter if the cut-rule is admissible in this system or not. Consequently, the authors’ justification of their research heavily relies on their strange definition of “categorisation”. Fortunately, I believe the Cut-Elimination Theorem does not require any justification of that kind, and the authors’ results can defend themselves without that.

On p. 4 (the long remark in parentheses at the bottom) we find a false inequality: clearly, substitution can make the complexity of the formula much greater than quantification, unless one assumes quantification be of infinite complexity. Accordingly, the whole passage is not sound.

These are all critical comments. The remainder is quite good, and the authors should simply take into account the above remarks, while preparing a final draft for publication.

July 14, 1993

Prof. Dr. Wojciech Buszkowski Institute of Mathematics Adam Mickiewicz University Matejki 48/49 60-769 Poznan, Poland