All known structural extensions of the substructural logic $\mathsf{FL_e}$, Full Lambek calculus with exchange/commutativity, (corresponding to subvarieties of commutative residuated lattices axiomatized by $\{\vee, \cdot, 1\}$-equations) have decidable theoremhood; in particular all the ones defined by knotted axioms enjoy strong decidability properties (such as the finite embeddability property). We provide infinitely many such extensions that have undecidable theoremhood, by encoding machines with undecidable halting problem. An even bigger class of extensions is shown to have undecidable deducibility problem (the corresponding varieties of residuated lattices have undecidable word problem); actually with very few exceptions, such as the knotted axioms and the other prespinal axioms, we prove that undecidability is ubiquitous. Known undecidability results for non-commutative extensions use an encoding that fails in the presence of commutativity, so and-branching counter machines are employed. Even these machines provide encodings that fail to capture proper extensions of commutativity, therefore we introduce a new variant that works on an exponential scale. The correctness of the encoding is established by employing the theory of residuated frames.
The Tsinghua-UvA JRC for Logic, Department of Philosophy, Tsinghua University（清华大学哲学系清华-阿姆斯特丹逻辑联合研究中心）；Institute for Logic, Language and Computation, University of Amsterdam（阿姆斯特丹大学逻辑语言与计算研究所）
Undecidable problems for propositional calculi with implication
本文利用肯定前件和替换规则研究了包含经典蕴涵$\to$的签名上的命题演算。对于这些演算，我们考虑一些识别问题，如识别导子，扩展，完备性和公理化。本文的主要结果是证明了对于任何命题演算，扩张的识别问题都是不可判定的;对于包含公式$x \to ( y \to x )$的命题演算，公理化和完备性的识别问题都是不可判定的。作为推论，固定公式$A$的可导性问题对于所有$A$也是不可判定的。此外，我们给出了相关成果的历史回顾。
Institute for Logic, Language and Computation, Universiteit van Amsterdam（逻辑、语言与计算研究所，阿姆斯特丹大学）；Department of Mathematics, Université du Luxembourg（数学系，卢森堡大学）
