论文标题
$ \ mathsf {fl_e} $的最简单的扩展是不确定的
Most simple extensions of $\mathsf{FL_e}$ are undecidable
论文作者
论文摘要
亚逻辑$ \ Mathsf {fl_e} $的所有已知结构扩展，具有交换/交换性的完整Lambek微积分（对应于$ \ {\ vee，\ cdot，\ cdot，1 \} $ -EQUITACH，1 \} $ -EQUITACTION $ \ {特别是所有由打结的公理定义的均具有强大的可判性性能（例如有限的嵌入性属性）。我们通过编码具有无法确定的停止问题的机器来提供许多具有不可决定的理论的扩展。显示出更大的扩展名显示出不可证明的可得性问题（残留晶格的相应品种存在不可确定的单词问题）；实际上，除少数例外，例如打结的公理和其他前公理，我们证明不可证明性无处不在。非交通扩展的已知不确定性结果使用的编码在有换向性的情况下失败，因此采用了分支机构的计算机。甚至这些机器也提供了无法捕获通勤性的适当扩展的编码，因此我们引入了一种以指数级为准的新变体。编码的正确性是通过采用残留框架理论来确定的。
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.
