Abstract
We present a novel way of using proof nets for the multimodal Lambek calculus, which provides a general treatment of both the unary and binary connectives. We also introduce a correctness criterion which is valid for a large class of structural rules and prove basic soundness, completeness and cut elimination results. Finally, we will present a correctness criterion for the original Lambek calculus Las an instance of our general correctness criterion.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Danos, V.: 1990, ‘La Logique Linéaire Appliquée à l'étude de Divers Processus de Normalisation (Principalement du λ-Calcul)'. Ph.D. thesis, University of Paris VII.
Danos, V. and L. Regnier: 1989, ‘The Structure of Multiplicatives'. Archive for Mathematical Logic 28, 181-203.
de Groote, P.: 1999, ‘An Algebraic Correctness Criterion for Intuitionistic Proof-nets'. Theoretical Computer Science 224(1–2), 115-134.
de Groote, P. and F. Lamarche: 2002, ‘Classical non-associative Lambek calculus'. Studia Logica, in this issue, 245-278.
Girard, J.-Y.: 1987, ‘Linear Logic'. Theoretical Computer Science 50, 1-102.
Girard, J.-Y.: 1996, ‘Proof-Nets: The Parallel Syntax for Proof-Theory'. In: P. Agliana and A. Ursini (eds.): Logic and Algebra. New York: Marcel Dekker.
Lafont, Y.: 1995, ‘From Proof Nets to Interaction Nets'. In: J.-Y. Girard, Y. Lafont, and L. Regnier (eds.): Advances in Linear Logic. Cambridge University Press, pp. 225-247.
Lambek, J.: 1958, ‘The Mathematics of Sentence Structure'. American Mathematical Monthly 65, 154-170.
Lambek, J.: 1961, ‘On the Calculus of Syntactic Types'. In: R. Jacobson (ed.): Structure of Language and its Mathematical Aspects, Proceedings of the Symposia in Applied Mathematics, Vol. XII. pp. 166-178, American Mathematical Society.
Moortgat, M.: 1997, ‘Categorial Type Logics'. In: J. van Benthem and A. ter Meulen (eds.): Handbook of Logic and Language. Elsevier/MIT Press, Chapt. 2.
Puite, Q.: 1998, ‘Proof Nets with Explicit Negation for Multiplicative Linear Logic'. Technical report, Department of Mathematics, Utrecht University. Preprint 1079.
Puite, Q.: 2001, ‘Sequents and Link Graphs: Contraction Criteria for Refinements of Multiplicative Linear Logic’. Ph.D. thesis, Department of Mathematics, Utrecht University.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Moot, R., Puite, Q. Proof Nets for the Multimodal Lambek Calculus. Studia Logica 71, 415–442 (2002). https://doi.org/10.1023/A:1020525032763
Issue Date:
DOI: https://doi.org/10.1023/A:1020525032763