Penn Arts & Sciences Logo

Logic and Computation Seminar

Monday, January 25, 2016 - 3:30pm

Stepan Kuznetsov

Steklov Mathematical Institute (Moscow)

Location

University of Pennsylvania

4C8

The Lambek calculus is a variant of linear logic used to describe natural languages. Since this calculus is non-commutative, it has two implication connectives, and they are interpreted as division operations on formal languages (the pairwise concatenation of A and B is included in C iff B is included in (A \ C) iff A is included in (C / B)). Formulae of the Lambek calculus are used to describe syntactic categories of words and phrases in natural language. Thus the Lambek calculus provides a framework for syntax analysis. As a substructural logic, the Lambek calculus lacks structural rules---weakening, contraction, and permutation---except for implicit associativity. We consider extensions of the Lambek calculus with two structural modalities (unary connectives). The first one enables all three structural rules for formulae marked by this modality, and corresponds to the exponential in linear logic. The second one enables only contraction and permutation, but not weakening. This modality, that could be called subexponential, is motivated from linguistic applications. For both extensions we prove that the derivability problem is undecidable, even in the fragment with only one implication (division). To compare, the original Lambek calculus is decidable (more precisely, NP-complete).