

Workshop on Proof Theory, Modal Logic and Reflection Principles
October 20, 2017 10:35, Moscow, Steklov Mathematical Institute






Lambek calculus extended with subexponential and bracket modalities
A. Scedrov^{} 
Video records: 

MP4 
828.7 Mb 

MP4 
226.9 Mb 
Number of views: 
This page:  30  Video files:  8 

Abstract:
The Lambek calculus (1958, 1961) is a wellknown logical formalism for modelling natural language syntax. The calculus can also be considered as a version of noncommutative intuitionistic linear logic. The Lambek calculus is a logical foundation of categorial grammar, a linguistic paradigm of grammar as logic and parsing as deduction. The original calculus covered a substantial number of intricate natural language phenomena. In order to address more subtle linguistic issues, the Lambek calculus has been extended in various ways.
For instance, an extension with socalled bracket modalities introduced by Morrill (1992) and Moortgat (1995) is capable of representing controlled nonassociativity and is suitable for the modeling of islands. The syntax is more involved than the syntax of a standard sequent calculus. Derivable objects are sequents of the form Gamma $\to$ A , where the antecedent Gamma is a structure called metaformula and the succedent A is a formula. Metaformulae are built from formulae (types) using two metasyntactic operators: comma and brackets.
Morrill and Valentin (2015) introduce a further extension with socalled exponential modality, suitable for the modeling of medial and parasitic extraction. Their extension is based on a nonstandard contraction rule for the exponential, which interacts with the bracket structure in an intricate way. The standard contraction rule for exponentials is not admissible in this calculus. In joint work with Max Kanovich and Stepan Kuznetsov we show that provability in this calculus is undecidable and we investigate restricted decidable fragments considered by Morrill and Valentin. We show that these fragments belong to NP.
Language: English

