Unbounded Łukasiewicz logic is a substructural logic that combines features of infinite-valued Łukasiewicz logic with those of abelian logic. The logic is finitely strongly complete w.r.t.~the additive $\ell$-group on the reals expanded with a distinguished element $-1$. We show that the existential theory of this structure is NP-complete. This provides a complexity upper bound for the set of theorems and the finite consequence relation of unbounded Łukasiewicz logic. The result is obtained by reducing the problem to the existential theory of the MV-algebra on the reals, the standard semantics of Łukasiewicz logic. This provides a new connection between both logics. The result entails a translation of the existential theory of the standard MV-algebra into itself.
翻译:无界Łukasiewicz逻辑是一种子结构逻辑,它融合了无限值Łukasiewicz逻辑与阿贝尔逻辑的特征。该逻辑相对于由添加了区分元素$-1$的实数集上的加法$\ell$-群具有有限强完全性。我们证明了该结构的存在性理论是NP完全的。这一结果为无界Łukasiewicz逻辑的定理集和有限推论关系提供了复杂性上界。该结果通过将问题归约到实数上的MV代数(Łukasiewicz逻辑的标准语义)的存在性理论而获得,从而建立了两种逻辑之间的新联系。该结论还蕴含了标准MV代数存在性理论到其自身的翻译。