A note on undecidability of propositional non-associative linear logics
Logic in Computer Science
2019-10-01 v1
Abstract
We introduce a non-associative and non-commutative version of propositional intuitionistic linear logic, called propositional non-associative non-commutative intuitionistic linear logic (NACILL for short). We prove that NACILL and any of its extensions by the rules of exchange and/or contraction are undecidable. Furthermore, we introduce two types of classical versions of NACILL, i.e., an involutive version of NACILL and a cyclic and involutive version of NACILL. We show that both of these logics are also undecidable.
Cite
@article{arxiv.1909.13444,
title = {A note on undecidability of propositional non-associative linear logics},
author = {Hiromi Tanaka},
journal= {arXiv preprint arXiv:1909.13444},
year = {2019}
}