技术摘要：卢卡西维茨逻辑及其无界相对的可满足性

问题陈述

本文探讨了无界卢卡西维茨逻辑（$L_u$）的存在理论（可满足性问题）的计算复杂性。$L_u$ 是一种亚结构逻辑，结合了无限值卢卡西维茨逻辑（$L$）与阿贝尔逻辑的特征。其预期语义是实数上的点化阿贝尔全序加法群，记为 $\mathbb{R}_{-1}$，其中定义域为 $\mathbb{R}$，且一个区分常数 $-1$ 代表假。

虽然标准卢卡西维茨逻辑（$L$）的复杂性已得到充分确立——具体而言，标准 MV-代数 $[0, 1]_L$ 中项的可满足性是 NP-完全的（Mundici [35]）——但在归约到标准卢卡西维茨逻辑的语境下，$L_u$（及其底层代数 $\mathbb{R}_{-1}$）的存在理论的复杂性此前并未被明确确定。作者旨在通过建立 $\mathbb{R}_{-1}$ 的存在理论与 $[0, 1]_L$ 的存在理论之间的多项式时间归约，为 $L_u$ 提供复杂性估计。

方法论

本文采用了一种包含代数归约和有界模型分析的双重方法论：

1. 满足赋值的有界性

作者首先确立，如果一个存在语句在 $\mathbb{R}_{-1}$ 中成立，则它在一个特定的、多项式有界的区间内拥有一个满足赋值。

• 引理 3.2（有界赋值）：对于点化 $\ell$-群语言（$L_{pAb}$）中的任何开公式 $\Phi$，如果 $\mathbb{R}_{-1} \models \exists \bar{x} \Phi$，则存在一个有理赋值 $\bar{a}$ 使得 $\Phi(\bar{a})$ 成立，其中 $\bar{a}$ 中值的二进制表示大小是 $\Phi$ 大小的多项式。
• 该结果依赖于将可满足性问题归约为一组线性不等式，并应用源自克拉默法则的界限（引理 3.1），确保解位于区间 $[-2^M, 2^M]$ 内，其中 $M$ 与公式大小呈多项式关系。

2. 通过线性映射的多项式时间归约

方法论的核心是从 $\mathbb{R}_{-1}$ 的存在理论到标准 MV-代数 $[0, 1]_L$ 的存在理论的多项式时间归约。

• 映射构造：作者定义了一个从 $L_{Ab}$（阿贝尔 $\ell$-群）中的项到 $L_{MV}[1/2]$（带有常数 $1/2$ 的 MV-代数）中的项的映射 $\tau$。该映射利用线性变换 $r_{M,k}(a) = \frac{a}{2^{M+k+1}} + \frac{1}{2}$，将 $\mathbb{R}$ 中有界区间 $[-2^M, 2^M]$ 映射到 $[0, 1]$ 的一个子区间。
• 项翻译：在此线性映射下，翻译 $\tau$ 保留了项的语义结构（加法、否定、格运算），前提是项的深度是有界的。
• 处理复杂性：为了防止项大小出现指数级膨胀（这在嵌套加法的朴素翻译中会发生），作者采用了 Tseitin 变换。这为子项引入了新变量，将复杂公式转换为等可满足的多项式大小公式，其中项的深度至多为 1。
• 编码常数：$\mathbb{R}_{-1}$ 中的常数 $-1$ 在 MV-代数中使用辅助变量（$z_i, q, r$）进行编码，这些变量受特定方程约束（例如 $z_1 = \neg z_1$，$z_{i+1} \oplus z_{i+1} = z_i$），从而在标准语义中强制特定的有理数值（$1/2$ 的幂）。

3. 卢卡西维茨逻辑的自归约

本文还研究了从 $[0, 1]_L$ 到 $\mathbb{R}_{-1}$ 的归约（在先前工作 [12] 中确立）与从 $\mathbb{R}_{-1}$ 到 $[0, 1]_L$ 的新归约的组合。

• 作者定义了一个复合翻译 $\sigma_q$，直接将 $L_{MV}$ 的项映射到 $L_{MV}[1/2]$ 的项。
• 他们证明，这种组合产生了一个多项式大小的翻译，实际上提供了 $[0, 1]_L$ 的存在理论到其自身的非平凡归约。

主要结果

1. $L_u$ 存在理论的 NP-完全性：$\mathbb{R}_{-1}$ 的存在理论（因此也是无界卢卡西维茨逻辑的定理集和有限后承关系）是 NP-完全的。

   • 上界：该问题属于 NP，因为满足赋值可以在多项式有界区间内找到（引理 3.2），且到 $[0, 1]_L$ 的归约（已知为 NP-完全）是多项式时间的（定理 4.6）。
   • 下界：其难度源于 $[0, 1]_L$ 中项可满足性的已知 NP-完全性（Mundici [35]）以及从 $[0, 1]_L$ 到 $\mathbb{R}_{-1}$ 的多项式时间归约的存在（来自 [12]）。

2. 全称片段的 CoNP-完全性：因此，$\mathbb{R}_{-1}$ 的全称理论、等式理论和拟等式理论是 CoNP-完全的。

3. $[0, 1]_L$ 的自翻译：本文展示了标准 MV-代数 $[0, 1]_L$ 的存在理论到其自身的多项式时间归约（定理 5.6）。这是通过组合到 $\mathbb{R}_{-1}$ 的归约和回到 $[0, 1]_L$ 的归约实现的。

意义与主张

作者声称，这项工作的主要贡献在于归约方法，而非复杂性结果本身，鉴于相关结构的已知复杂性，后者可能已被预料到。

• 新联系：该归约建立了无界卢卡西维茨逻辑（$L_u$）与标准卢卡西维茨逻辑（$L$）之间新的、明确的联系。它表明，无界逻辑的可满足性问题可以通过将 0 的足够大邻域线性映射到区间 $[0, 1]$，有效地翻译为标准逻辑。
• 显式归约：与可能依赖抽象存在性或不同逻辑框架（例如 Marchioni 和 Montagna [31] 将实闭域归约到 $L_{\Pi 1/2}$）的先前方法不同，本文提供了一个显式的、多项式时间的归约，该归约能很好地扩展到语言片段。
• 理论洞察：该结果涉及标准 MV-代数存在理论到其自身的翻译。作者指出，这引发了与其他逻辑归约的比较，但强调他们的方法依赖于加法结构和线性映射，避免了其他框架所需的乘法函数符号。

本文得出结论：尽管该逻辑具有无限值的性质，$L_u$ 的可满足性问题仍是可判定的，并且与其经典命题对应物处于相同的复杂性类（NP-完全）。