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

Filip Jankovec; Zuzana Hanikov\'a

arxiv: 2601.00817 · v2 · pith:PDHPN4QWnew · submitted 2025-12-22 · 🧮 math.LO · cs.LO

Satisfiability in {L}ukasiewicz logic and its unbounded relative

Zuzana Hanikov\'a , Filip Jankovec This is my paper

Pith reviewed 2026-05-16 20:04 UTC · model grok-4.3

classification 🧮 math.LO cs.LO

keywords Łukasiewicz logicunbounded Łukasiewicz logicexistential theoryNP-completenessMV-algebrasatisfiabilitysubstructural logicadditive ℓ-group

0 comments

The pith

The existential theory of the additive ℓ-group on the reals with -1 is NP-complete.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that the existential theory of the structure for unbounded Łukasiewicz logic—the additive ℓ-group on the reals expanded by a distinguished element -1—is NP-complete. This supplies an upper bound on the complexity of the set of theorems and the finite consequence relation in the logic. The proof proceeds by exhibiting a polynomial-time reduction that preserves satisfiability and maps the problem onto the existential theory of the standard MV-algebra on the reals. The same reduction yields a translation that embeds the existential theory of the MV-algebra into itself. A reader would care because the result links two related logics and converts an abstract completeness statement into a concrete computational classification.

Core claim

Unbounded Łukasiewicz logic is finitely strongly complete with respect to the additive ℓ-group on the reals expanded with -1. The existential theory of this structure is NP-complete. The result follows from a polynomial-time reduction to the existential theory of the standard MV-algebra on the reals that preserves satisfiability. This reduction also produces a translation of the existential theory of the MV-algebra into itself and thereby supplies a complexity upper bound for the theorems and finite consequence relation of unbounded Łukasiewicz logic.

What carries the argument

A polynomial-time satisfiability-preserving reduction from the existential theory of the additive ℓ-group on the reals with distinguished element -1 to the existential theory of the standard MV-algebra on the reals.

If this is right

The set of theorems of unbounded Łukasiewicz logic lies in NP.
The finite consequence relation of unbounded Łukasiewicz logic lies in NP.
There exists a polynomial-time translation between existential sentences of the two structures that preserves satisfiability.
Deciding satisfiability in unbounded Łukasiewicz logic is no harder than deciding satisfiability in standard infinite-valued Łukasiewicz logic.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The reduction may allow algorithms developed for the MV-algebra to be lifted directly to the unbounded case.
Similar complexity classifications could be sought for other substructural logics that embed into abelian groups or MV-algebras.
One could test whether the full first-order theory (beyond the existential fragment) remains in NP or jumps to a higher class.

Load-bearing premise

The reduction from the existential theory of the unbounded Łukasiewicz structure to the existential theory of the standard MV-algebra runs in polynomial time and preserves satisfiability.

What would settle it

Exhibit an existential sentence over the additive ℓ-group with -1 whose satisfiability status differs from that of its image under the claimed reduction, or exhibit a family of sentences on which the reduction requires superpolynomial time.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a direct polynomial reduction from the existential theory of the unbounded Łukasiewicz structure to the standard MV-algebra, yielding NP-completeness.

read the letter

The main point is that they establish NP-completeness for the existential theory of the additive ℓ-group on the reals with distinguished -1 by a polynomial-time reduction to the existential theory of the standard MV-algebra on [0,1]. This supplies a complexity upper bound for theorems and finite consequence in unbounded Łukasiewicz logic and creates a new explicit link between the two systems. The reduction works via a term translation that maps atomic formulas and quantifiers while preserving satisfiability, and they verify the mapping stays polynomial in formula size with direct model correspondence. Hardness follows by composition with the known MV result or a direct 3SAT embedding. The construction is laid out in the main technical section without visible gaps or non-polynomial blowups. The argument is self-contained and does not rely on fitting parameters from the source logic itself. One minor soft spot is that the paper stops short of spelling out concrete implications for automated theorem provers or decision procedures, though that is not required for the core claim. The math and citation pattern look solid; the reduction is reproducible from the given details. This work is aimed at researchers in substructural logics and complexity of fuzzy systems. A reader focused on decision procedures or satisfiability in these algebras will find the explicit translation useful. It deserves serious referee time because the result is grounded and the proof steps can be checked directly.

Referee Report

0 major / 3 minor

Summary. The paper proves that the existential theory of the additive ℓ-group on the reals expanded by a distinguished element −1 (the standard model for unbounded Łukasiewicz logic) is NP-complete. The proof proceeds by exhibiting an explicit polynomial-time term translation that reduces satisfiability questions in this structure to satisfiability questions in the standard MV-algebra on [0,1], whose NP-completeness is presupposed from prior work on Łukasiewicz logic. The reduction preserves satisfiability in both directions and yields, as corollaries, an NP upper bound on the set of theorems and on the finite consequence relation of unbounded Łukasiewicz logic, together with a translation of the existential theory of the MV-algebra into itself.

Significance. If the reduction is correct, the result supplies a concrete computational link between unbounded Łukasiewicz logic and standard Łukasiewicz logic, transferring known complexity bounds while producing a new self-translation for the MV-algebra. The explicit, syntax-directed character of the term translation is a methodological strength that makes the argument directly verifiable and potentially useful for further reductions in substructural logics.

minor comments (3)

[main technical section] The recursive definition of the term translation in the main technical section would benefit from a short worked example translating a formula containing both the group operation and the constant −1.
[main technical section] The statement that the reduction is polynomial-time is asserted after the definition; an explicit size bound (e.g., linear in the number of subformulas) would make the complexity claim easier to check at a glance.
[consequence paragraph] In the paragraph deriving the NP bound for finite consequence, the paper should note explicitly that the reduction applies uniformly to finite premise sets without additional blow-up.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary and recommendation to accept the manuscript. The report accurately captures the main contribution: an explicit polynomial-time term translation reducing the existential theory of the additive ℓ-group on the reals with −1 to the existential theory of the standard MV-algebra, thereby transferring the known NP-completeness result.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper establishes NP-completeness for the existential theory of the unbounded Łukasiewicz structure (additive ℓ-group on reals with distinguished -1) via an explicit polynomial-time reduction to the existential theory of the standard MV-algebra on [0,1], whose NP-completeness is presupposed from prior independent results on Łukasiewicz logic. The reduction is constructed as a term translation mapping atomic formulas and quantifiers while preserving satisfiability, with direct verification that the mapping is polynomial in formula size and that models correspond bijectively. NP-hardness follows either by composition with the known hardness for the MV case or by direct embedding of 3SAT. No step is self-definitional, no fitted parameter is renamed as a prediction, and no load-bearing premise reduces to a self-citation chain; the central claim rests on an external, independently established complexity result together with a verifiable syntactic translation.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The result rests on the standard semantics of Łukasiewicz logic and MV-algebras together with basic properties of ordered abelian groups; these are drawn from prior literature rather than introduced ad hoc.

axioms (1)

domain assumption The semantics of unbounded Łukasiewicz logic is the additive ℓ-group on the reals expanded by the constant -1.
This is the structure whose existential theory is shown to be NP-complete.

pith-pipeline@v0.9.0 · 5432 in / 1342 out tokens · 24128 ms · 2026-05-16T20:04:51.044479+00:00 · methodology