One can not only multiply formal languages by pairwise concatenation A dot B, but also divide them in such a way that A dot B is included in C iff B is included in (A \ C) and A is included in (C / B). Since concatenation is non-commutative, we have two division operations. The Lambek calculus was designed to describe all universally true statements of the form "A is included in B", where A and B are formulas built using the three connectives (multiplication and two divisions). The completeness theorem was proved by Pentus (1995). It looks natural to consider also other well-known operations on formal languages, and one of these operations is the Kleene star, or iteration. Though this operation is very standard, the problem of enriching the Lambek calculus with this new unary connective in a proper way appears to be quite hard. We present two lines of calculi. The first one uses omega-rules or derivation trees with infinite branches, and we prove cut-elimination and completeness of the product-free fragment, but, as the derivations are infinite, we do not get any algorithmic properties, even recursive enumerability. The second approach is to formalize the Kleene star in an inductive manner. We present a Hilbert-style axiomatization and also a Gentzen system with cyclic derivations. This system is sound with respect to the intended interpretation, and completeness, in other words, whether the system with omega-rules is stronger than the inductive one, remains an open question.
Logic and Computation Seminar
Monday, June 1, 2015 - 3:00pm
Stepan L. Kuznetsov
Moscow State University