Comments on Herman Hendriks “Lambek Semantics”

Johan van Benthem (University of Amsterdam) Grisha Mints (Stanford University)

This Report presents three interesting contributions to the proof theory of categorial logics. First, there is an extended ’annotated’ version of the directed Lambek Calculus which provides unique derivations for each expressible typetheoretic meaning (improving on work by Konig and Hepple), then the author provides a useful cleaned-up version of other proposed categorial proof formats (in particular, Roorda’s proof nets), and finally, he proves an embedding from general Lambek Calculus into its one-variable fragment (improving an earlier result by Ponse).

These results are connected with general mathematical logic in various ways. Hendriks’ paper is not optimally informative in this respect, because of its discursive style and at times idiosyncratic notation, with various crucial logical facts remaining hidden in footnotes. Here are some examples of what we have in mind.

(1) The proof-search strategy producing unique normal form derivations proposed here coincides with the strategies found in Andreoli & Pareschi 1990 and Mints 1993. Moreover, it is what would result from translating natural deduction trees into sequent derivations in the manner of Prawitz 1965. Note that normalized natural deductions have the required uniqueness property directly, which might even produce an argument in their favour for categorial purposes (cf. van Benthem 1991). Next, Hendriks’ starred Lambek Calculus demonstrates a proof-theoretic device of general utility, namely, the explicit encoding of proof-search strategies in sequents via special notation. Similar devices have been proposed independently in the proof-theoretic literature (some recent examples are Mints 1993, Kanazawa 1993), be it with respect to antecedent types only.

(2) The embedding into the one-variable fragment seems related to the complexity analysis in Kanovich 1993, who shows that the satisfiability problem for one-variable fragments of various subsystems of linear logic has equal complexity to that for the full language. Are the two methods of encoding related?

(3) There are several connections with previous work in category theory. For instance, earlier work by Lambek and McLane (1971, 1982) on the ’coherence problem’ for Cartesian-closed categories seems relevant (cf. also Lambek & Scott 1986). These problems concern the uniqueness of categorial diagrams between given sets of source and target objects. What McLane proved, amongst others, is that all provable ’balanced sequents’ (in which each propositional variable occurs exactly twice) have a unique derivation in Lambek Calculus.

(4) Also, there are direct connections with standard topics in typed lambda calculus. For instance, h-normal forms were studied by Mints in various publications (cf. Mints 1992) and their connection with unique normalized sequent proofs was noted. In fact, it seems quite possible to prove the author’s main result on uniqueness of his special derivations by direct analysis of such lambda forms.

(5) It would be of interest to see how far these various ideas can be extended to languages with a richer repertoire of type-forming operators (such as various products). Finally, some conclusions in the Report might be stated more explicitly by its author. For instance, it seems that the analysis provided here refutes an earlier DYANA ’working hypothesis’: proof nets are no longer the preferred format for categorial derivation without ’spurious ambiguity’.

The above list of comments suggests a number of routes via which the work in this Report could be linked up with more mainstream themes in mathematical logic. Even in its present state, however, it seems a substantial contribution of broader interest.

References

Andreoli & R. Pareschi, 1990, ”Linear Objects: Logical Processes with Built-In Inheritance”, New Generation Computing, special issue, Selected papers of ICLP’90. J. van Benthem, 1991, Language in Action, North-Holland, Amsterdam. M. Kanazawa, 1993, ”Natural Deduction and Decidability for the Mixed Style of Inference”, CSLI, Stanford University. M. Kanovich, 1993, ”The Expressive Power of Initial Fragments of Linear Logic and the Lambek Calculus”, Russian Humanitarian State University, Moscow. J. Lambek & P. Scott, 1986, Introduction to Higher-Order Categorical Logic, Cambridge University Press, Cambridge. S. McLane, 1971, Categories for the Working Mathematician, Springer Verlag, New York. S. McLane, 1982, ’Why Commutative Diagrams Coincide with Equivalent Proofs’, Contemporary Mathematics 13, 387-401. G. Mints, 1992, Selected Papers in Proof Theory, Bibliopolis North-Holland, Naples & Amsterdam. G. Mints, 1992, ”A Normal Form for Sequent Derivations”, Department of Philosophy, Stanford University. D. Prawitz, 1965, Natural Deduction, Almqvist & Wiksell, Stockholm. W. Sieg, 1992, ’Mechanisms and Search’, Department of Philosophy, Carnegie Mellon University, Pittsburgh, AILA Preprint 14. Institute for Logic, Language and Computation, ILLC University of Amsterdam, 30 Juni 1993