Dialectica Categories for the Lambek Calculus
We revisit the old work of de Paiva on the models of the Lambek Calculus in dialectica models making sure that the syntactic details that were sketchy on the first version got completed and verified. We extend the Lambek Calculus with a \(\kappa \) modality, inspired by Yetter’s work, which makes the calculus commutative. Then we add the of-course modality !, as Girard did, to re-introduce weakening and contraction for all formulas and get back the full power of intuitionistic and classical logic. We also present the categorical semantics, proved sound and complete. Finally we show the traditional properties of type systems, like subject reduction, the Church-Rosser theorem and normalization for the calculi of extended modalities, which we did not have before.
KeywordsLambek calculus Dialectica models Categorical semantics Type theory Structural rules Non-commutative Linear logic
The authors would like to thank the anonymous reviewers for their feedback which did make this a better paper. The second author was partially supported by the NSF grant #1565557.
- 4.Bierman, G.M.: On Intuitionistic Linear Logic. PhD thesis, Wolfson College, Cambridge, December 1993Google Scholar
- 9.de Paiva, V.: The dialectica categories. PhD thesis, Computer Laboratory, University of Cambridge, PhD Thesis, 1990. Computer Laboratory, University of Cambridge, PhD Thesis (1990)Google Scholar
- 10.de Paiva, V.: A Dialectica model of the Lambek calculus. In: 8th Amsterdam Logic Colloquium (1991)Google Scholar
- 13.Greco, G., Palmigiano, A.: Linear Logic Properly Displayed. ArXiv e-prints, November 2016Google Scholar
- 16.Barry Jay, C.: Coherence in category theory and the Church-Rosser property. Notre Dame J. Formal Logic 33(1), 140–143 (1991). 12Google Scholar
- 17.Lafont, Y., Streicher, T.: Games semantics for linear logic. In: Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science, 1991, LICS 1991, pp. 43–50. IEEE (1991)Google Scholar
- 18.Lamarche, F., Retoré, C.: Proof nets for the Lambek calculus - an overview. In: Proceedings of the Third Roma Workshop. Proofs and Linguistic Categories, pp. 241–262 (1996)Google Scholar
- 19.Lambek, J.: The mathematics of sentence structure. In: American Mathematical Monthly, pp. 154–170 (1958)Google Scholar
- 20.Moortgat, M.: Typelogical grammar. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy, Spring 2014 edition (2014)Google Scholar
- 21.Polakow, J.: Ordered linear logic and applications. PhD thesis, Carnegie Mellon University (2001)Google Scholar
- 24.Szabo, M.E.: Algebra of Proofs. Studies in Logic and the Foundations of Mathematics, vol. 88, North-Holland (1978, 1979)Google Scholar