Full Lambek Calculus with Contraction is Undecidable

0442807 - ÚI 2017 RIV US eng J - Journal Article
Chvalovský, Karel - Horčík, Rostislav
Full Lambek Calculus with Contraction is Undecidable.
Journal of Symbolic Logic. Roč. 81, č. 2 (2016), s. 524-540. ISSN 0022-4812. E-ISSN 1943-5886
R&D Projects: GA ČR GAP202/11/1632
Institutional support: RVO:67985807
Keywords : substructural logic * full Lambek calculus * contraction rule * square-increasing residuated lattice * equational theory * decidability
Subject RIV: BA - General Mathematics
Impact factor: 0.511, year: 2016

We prove that the set of formulae provable in the full Lambek calculus with the structural rule of contraction is undecidable. In fact, we show that the positive fragment of this logic is undecidable.
Permanent Link: http://hdl.handle.net/11104/0245628