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代数的可判定性理论到其自身的翻译。