Satisfiability in {\L}ukasiewicz logic and its unbounded relative

TL;DR

This paper investigates the computational complexity of unbounded { extL}ukasiewicz logic, establishing NP-completeness of its existential theory through a reduction to the standard MV-algebra on reals.

Contribution

It demonstrates that the existential theory of unbounded { extL}ukasiewicz logic is NP-complete, linking it to the standard MV-algebra and providing a complexity upper bound.

Findings

The existential theory of unbounded { extL}ukasiewicz logic is NP-complete.

A reduction to the existential theory of the MV-algebra on reals is established.

The work connects the logic's complexity to the standard semantics of { extL}ukasiewicz logic.

Abstract

Unbounded {\L}ukasiewicz logic is a substructural logic that combines features of infinite-valued {\L}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 {\L}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 {\L}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.