Craig’s trick and a non-sequential system for the Lambek calculus and its fragments. (English) Zbl 1515.03114

Kuznetsov, Stepan; Lugovaya, Valentina; Ryzhova, Anastasiia

Log. J. IGPL 27, No. 3, 252-266 (2019).

Summary: We show that Craig’s trick is not valid for the Lambek calculus, i.e. there exists such a recursively enumerable theory (set of sequents) over the Lambek calculus, which does not have a decidable axiomatization. We show that Lambek’s non-emptiness restriction (the constraint that left-hand sides of all sequents should be non-empty) and an infinite set of variables are crucial for the failure of Craig’s trick. We also present a non-sequential formulation of the product-free fragment of the Lambek calculus and show its equivalence to the sequential one.

MSC:

03B47	Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03F52	Proof-theoretic aspects of linear logic and other substructural logics

Keywords:

Craig’s trick; Lambek calculus; non-sequential calculus; substructural logic; Lambek’s restriction