Lindström Maximality for Fitting's Finite Heyting-Valued Modal Logic with Exact Truth Tests

技术摘要：针对具有精确真值测试的 Fitting 有限海廷值模态逻辑的 Lindström 最大性

问题陈述
本文探讨了多值模态逻辑（特别是针对固定有限海廷代数 $L$ 的 Fitting 模态逻辑）的表达能力特征。尽管经典模态逻辑和针对有限 MTL 链（线性序代数）的多值逻辑已存在 Lindström 式的最大性定理，但对于非线性情况，相应的结论仍然缺失。Badia 和 Olkhovikov 的前人工作通过利用顶元素 (1) 的唯一直接前驱来分离指定值与非指定值，从而在有限 MTL 链上建立了最大性。然而，这种方法对于任意有限海丁代数是失效的，因为这些代数可能缺乏线性，且在 1 以下没有唯一的衣帽元素（coatom）。核心问题在于：在不假设代数为链的情况下，Maruyama 对 Fitting 逻辑的呈现方式（即使用一元精确真值测试 $T_\ell$ 而非所有值的原始真值常量）是否仍能保持其在抽象扩张中的最大性。

方法论
作者采用了一种从经典及多值 Lindström 定理中改编而来的模型论方法。该方法包括：

1. 定义基础逻辑： 利用 Maruyama 版的基于清晰 Kripke 框架的 Fitting 逻辑 ($FML_L$)，其中公式取值于有限海廷代数 $L$。该语言包含精确真值测试 $T_\ell$，使得 $T_\ell \phi$ 当且仅当 $\phi$ 的值为 $\ell$ 时评估为 1。
2. 引入派生布尔算子： 为了取代依赖于链的隔离机制，作者定义了布尔值测试：
   • $D\phi := T_1\phi$ （当 $\phi$ 为指定值/等于 1 时为真）。
   • $N\phi := T_0(T_1\phi)$ （当 $\phi$ 为非指定值/不等于 1 时为真）。
   • 一个派生的存在模态 $\Diamond_1 \phi := T_0(\Box N\phi)$，它表达了存在一个可达状态，在该状态下 $\phi$ 的值为 1。
3. 抽象扩张： 本文考虑了满足三个模型论性质的 $FML_L$ 的抽象扩张 $\mathcal{L}$：紧致性（Compactness）、Tarski 合并性质（Tarski Union Property）以及对双模拟（bisimulation）的强不变性。
4. 饱和与展开： 证明过程通过展开技术构建了饱和的初等扩张。它利用派生模态 $\Diamond_1$ 来定义“后继类型”，并利用紧致性和 Tarski 合并性质来构建实现这些类型的模型。
5. 判定引理（Decision Lemma）： 关键步骤涉及一个“判定引理”，该引理使用对 $(D\psi, N\psi)$ 来分离任何假设中的新公式与基础逻辑。这取代了在基于链的证明中所使用的“1 的直接前驱”论证。

主要贡献与结果

• Lindström 最大性定理： 主要结果（定理 1）指出，对于任何固定的有限海廷代数 $L$，Maruyama 版的 Fitting 模态逻辑在其所有满足紧致性、具有 Tarski 合并性质且对双模拟具有强不变性的抽象扩张中，对于 1-表达能力是最大的。
• 移除线性假设： 本文成功地将最大性结果从线性序代数（MTL 链）推广到任意有限海廷代数。证明表明，精确真值测试提供了足够的隔离能力，而无需要求线性序或特定的衣帽元素。
• 精确值可定义性： 作为最大性定理的推论（推论 1），本文证明了对于扩展 $\mathcal{L}$ 中的任何公式 $\phi$ 及任何值 $\ell \in L$，由 $\phi$ 取精确值 $\ell$ 的指向模型集合可以用基础逻辑中的公式来定义。具体而言，“精确值纤维”（exact-value fibre）是可定义的，尽管论文指出这并不一定意味着存在单个 $FML_L$ 中的公式能重现 $\phi$ 的完整 $L$ 值语义。
• 饱和模型的 Hennessy-Milner 性质： 本文确立了对于 $FML_L$-饱和模型，模态等价蕴含双模拟，将标准的 Hennessy-Milner 现象扩展到了这种多值设定中。

意义与主张
本文声称解决了文献中关于非线性代数上多值模态逻辑表达极限的空白。通过论证由精确真值测试 ($T_\ell$) 派生的布尔决策对 $(D\phi, N\phi)$ 能够分离指定值与非指定值，作者表明底层代数的结构约束（特别是线性）对于 Lindström 最大性并非必要。

其意义在于：

1. 泛化： 将 Lindström 定理的适用范围从受限的有限链环境扩展到了更广泛的有限海廷代数类。
2. 机制识别： 确定了由精确真值测试派生的布尔值测试是处理非线性设定下的值隔离与饱和论证的关键机制。
3. 可定义性： 确立了基础逻辑具有足够的表达能力，能够定义任何“合理”扩张中公式的精确值纤维，从而强化了 Maruyama 呈现方式的鲁棒性。

作者对未来的研究方向保持谦逊，并指出了开放性问题，例如 Tarski 合并性质是否可以被削弱、如何处理 $L$ 值的（模糊）可达关系，以及能否将独立的精确值定义统一为一个重现完整语义的单一公式。