Undecidability of consequence relation in full non-associative Lambek calculus. (English) Zbl 1373.03025
Summary: 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 \(\{\cdot,\vee\}\) 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.
MSC:
| 03B47 | Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) |
| 03B25 | Decidability of theories and sets of sentences |
Keywords:
substructural logics; consequence relation; undecidability; tag systems; word problem; rewriting systemsReferences:
| [1] | DOI: 10.1016/j.apal.2010.01.003 · Zbl 1245.03027 · doi:10.1016/j.apal.2010.01.003 |
| [2] | Languages: From formal to natural pp 45– (2009) |
| [3] | Reports on Mathematical Logic 43 pp 25– (2008) |
| [4] | DOI: 10.1007/BF00671566 · Zbl 0671.03018 · doi:10.1007/BF00671566 |
| [5] | DOI: 10.1145/321203.321206 · Zbl 0149.12405 · doi:10.1145/321203.321206 |
| [6] | DOI: 10.2307/2371809 · Zbl 0063.06327 · doi:10.2307/2371809 |
| [7] | Language and grammar: Studies in mathematical linguistics and natural language pp 77– (2005) · Zbl 1137.03300 |
| [8] | Theories of types and proofs 2 pp 207– (1998) |
| [9] | DOI: 10.1002/malq.19820283308 · Zbl 0499.03010 · doi:10.1002/malq.19820283308 |
| [10] | Structure of language and its mathematical aspects pp 166– (1961) |
| [11] | Transactions of the American Mathematical Society 357 pp 4141– (2004) |
| [12] | DOI: 10.2307/2310058 · Zbl 0080.00702 · doi:10.2307/2310058 |
| [13] | DOI: 10.1305/ndjfl/1094061862 · Zbl 0812.03008 · doi:10.1305/ndjfl/1094061862 |
| [14] | DOI: 10.1007/s00012-014-0284-1 · Zbl 1305.06012 · doi:10.1007/s00012-014-0284-1 |
| [15] | Lattice theory: Foundation (2011) |
| [16] | Residuated lattices: An algebraic glimpse at substructural logics 151 (2007) · Zbl 1171.03001 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
