Full Lambek Calculus with Contraction is Undecidable

Autoři: Karel Chvalovský
Rostislav Horčík
Rok vydání: 2016
Typ publikace: Článek v odborném periodiku
Periodikum: Journal of Symbolic Logic
Projekty: Algebraické metody v teorii důkazů
Bibliografická citace: 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

Abstrakt

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.