Full Lambek Calculus with Contraction is Undecidable

Authors: Karel Chvalovský, Rostislav Horčík
Publication year: 2016
Publication type: Článek v odborném periodiku
Periodical: Journal of Symbolic Logic
Projects: Algebraic Methods in Proof Theory
Bibliographic citation: CHVALOVSKÝ, Karel, HORČÍK, Rostislav. Full Lambek Calculus with Contraction is Undecidable. Journal of Symbolic Logic. 2016, 81(2), 524-540. ISSN 0022-4812. E-ISSN 1943-5886
Dostupné z: doi:10.1017/jsl.2015.18
DOI: 10.1017/jsl.2015.18
ID: 442807

Abstract

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.