AI 中文总结
针对菲廷有限海廷值模态逻辑，采用关系双拓扑表示法获得有限状态归约，构造受模态深度约束的有限树状精确值证书，实现保留精确真值的极小满射归约与有界归约反例。
AI 中文摘要
菲廷有限海廷值模态逻辑在有限海廷代数上解释模态公式。我们使用关系双拓扑表示来获得有限状态归约。对于有限模型和有限词汇，由原子赋值生成的模态子代数决定了状态-赋值映射。我们证明，观测商在双拓扑对偶中同构于其有限像，且商关系是典范对偶关系的限制。因此，该词汇上的每个公式都保留其精确真值，且该商是所有生成观测可分解的满射归约中的极小者。此外，对于任意公式和状态，我们构造了一个有限树状精确值证书，其深度受模态深度约束，分支数仅取决于真值值代数的高度和 boxed 子公式的数量。因此，失败的公式允许保留其精确失败值的有界归约反例。
英文摘要
Fitting's finite Heyting-valued modal logic interprets modal formulas over a finite Heyting algebra. We use a relational bitopological representation to obtain a finite-state reduction. For a finite model and a finite vocabulary, the modal subalgebra generated by the atomic valuations determines a state-evaluation map. We prove that the observational quotient is isomorphic to its finite image in the bitopological dual and that the quotient relation is the restriction of the canonical dual relation. Hence every formula over the vocabulary preserves its exact truth value, and the quotient is minimal among surjective reductions through which all generated observations factor. In addition, for any formula and state, we construct a finite tree-like exact-value certificate whose depth is bounded by modal depth and whose branching depends only on the height of the truth-value algebra and the number of boxed subformulas. Failed formulas therefore admit bounded reduced counterexamples preserving their precise failure values.
