MOST SIMPLE EXTENSIONS OF FLe ARE UNDECIDABLE
JOURNAL OF SYMBOLIC LOGIC(2022)
摘要
All known structural extensions of the substructural logic FLe, the Full Lambek calculus with exchange/commutativity (corresponding to subvarieties of commutative residuated lattices axiomatized by {V, center dot, 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.
更多查看译文
关键词
substructural logic,full Lambek calculus,simple extensions,residuated lattice,equational theory,word problem,decidability
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要