Undecidability of Consequence Relation in Full Non-associative Lambek Calculus

Authors: Karel Chvalovský
Publication year: 2015
Publication type: Článek v odborném periodiku
Periodical: Journal of Symbolic Logic
Projects: Mathematical Fuzzy Logic in Computer Science
Bibliographic citation: CHVALOVSKÝ, Karel. Undecidability of Consequence Relation in Full Non-associative Lambek Calculus. Journal of Symbolic Logic. 2015, 80(2), 567-586. ISSN 0022-4812. E-ISSN 1943-5886
Dostupné z: doi:10.1017/jsl.2014.39
DOI: 10.1017/jsl.2014.39
ID: 435915

Abstract

We prove that the consequence relation in the Full Non-associative Lambek Calculus is undecidable. An encoding of the halting problem for 2-tag systems using finitely many sequents in the language {., V} is presented. Therefore already the consequence relation in this fragment is undecidable. Moreover, the construction works even when the structural rules of exchange and contraction are added.