Abstract
We compare the Lambek-Grishin Calculus (LG) as defined by Moortgat [9, 10] with the non-associative classical Lambek calculus (CNL) introduced by de Groote and Lamarche [4]. We provide a translation of LG into CNL, which allows CNL to be seen as a non-conservative extension of LG. We then introduce a bimodal version of CNL that we call 2-CNL. This allows us to define a faithful translation of LG into 2-CNL. Finally, we show how to accomodate Grishin’s interaction principles by using an appropriate notion of polarity. From this, we derive a new one-sided sequent calculus for LG.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
As pointed out by an anonymous referee, this can be readily seen at the semantic level of the relational models of Kurtonina and Moortgat [7], where the two families of connectives are interpreted through distinct ternary relations.
References
Abrusci, V.M., Casadio, C. (eds.): New perspectives in logic and formal linguistics. In: Proceedings of the 5th Roma Workshop. Bulzoni Editore, Roma (2002)
Bastenhof, A.: Focalization and phase models for classical extensions of non-associative Lambek calculus. CoRR, abs/1106.0399, 2011
Bastenhof, A.: Categorial symmetry. Ph.D. thesis Utrecht University (2013)
de Groote, P., Lamarche, F.: Classical non-associative Lambek calculus. Stud. Logica. 71, 355–388 (2002)
Girard, J.-Y.: Linear logic. Theoret. Comput. Sci. 50, 1–102 (1987)
Grishin, V.N.: On a generalization of the Ajdukiewicz-Lambek system. In: Mikhailov, A.I. (ed.) Studies in Non-classical Logics and Formal Systems, pp. 315–334, Moscow, Nauka (1983)(In Russian. English translation in [1, pp. 9–27])
Kurtonina, N., Moortgat, M.: Relational semantics for the Lambek-Grishin calculus. In: Ebert, C., Jäger, G., Michaelis, J. (eds.) MOL 10. LNCS, vol. 6149, pp. 210–222. Springer, Heidelberg (2010)
Lambek, J.: On the calculus of syntactic types. In: Proceedings of the 12th Symposium Applied Mathematics Studies of Language and its Mathematical Aspects, pp. 166–178, Providence (1961)
Moortgat, M.: Symmetries in natural language syntax and semantics: the Lambek-Grishin calculus. In: Leivant, D., de Queiroz, R. (eds.) WoLLIC 2007. LNCS, vol. 4576, pp. 264–284. Springer, Heidelberg (2007)
Moortgat, M.: Symmetric categorial grammar. J. Philos. Logic 38(6), 681–710 (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendices
Proof of Proposition 1
We show that a derivation containing a single cut may be transformed in a cut-free derivation. Then, the general case follows by a simple induction on the number of cuts.
The proof proceeds by case analysis and by induction on the structure of the cut formula. One distinguishes four cases.
Case 1 : the cut formula in the left premise of the cut rule is introduced by an axiom.
In this case, the derivation may be transformed as follows:
where Derivation (1’) is obtained from Derivation (1) by replacing each occurrence of the cut formula by the structure \(\varDelta \).
Case 2 : the cut formula in the right premise of the cut rule is introduced by an axiom.
This case is symmetric to Case 1:
Case 3 : the cut formula is of the form 
, and is introduced by introduction rules in both the left and right premises of the cut rule.
This case corresponds to the following derivation schemes:
It can be transformed into the following derivation:
where the two new cuts are eliminable by induction hypothesis.
Case 4 : the cut formula is of the form \(A \mathbin {\otimes }B\), and is introduced by introduction rules in both the left and right premises of the cut rule.
This case, which is symmetric to Case 3, corresponds to the following derivation scheme:
It can be transformed as follows:
Proof of Proposition 2
We show that the translations of the algebraic laws of LG \(_{\varnothing }\) hold in CNL.
Preorder Laws. Let A be an LG-formula. It is easy to show that \(A^- = (A^+)^{\bot }\). Consequently, the translations of the preorder laws correspond to the identity rules (Id and Cut).
Residuation Laws. The two following derivation schemes show that the first residuation law holds.
The case of the second residuation law is similar.
Co-Residuation Laws. This case is symmetric to the case of the residuation laws, and it is handled in a similar way.
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Groote, P. (2015). Proof-Theoretic Aspects of the Lambek-Grishin Calculus. In: de Paiva, V., de Queiroz, R., Moss, L., Leivant, D., de Oliveira, A. (eds) Logic, Language, Information, and Computation. WoLLIC 2015. Lecture Notes in Computer Science(), vol 9160. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-47709-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-662-47709-0_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-47708-3
Online ISBN: 978-3-662-47709-0
eBook Packages: Computer ScienceComputer Science (R0)