带有精确真值测试的Fitting有限Heyting值模态逻辑的Lindström极大性
A Lindström Theorem for Fitting's Modal Logic over a Finite Heyting Algebra
AI总结：
该研究针对Maruyama提出的带精确真值测试的Fitting有限Heyting值模态逻辑，建立Lindström极大性定理，证明满足紧致性、Tarski并性质及互模拟强不变的抽象扩展与原逻辑表达等价，且扩展公式的精确值纤维可被定义。
AI中文摘要：
我们为Maruyama提出的、基于固定有限Heyting代数和清晰Kripke框架的Fitting模态逻辑的精确真值测试表示，建立了一个Lindström风格的极大性定理。与现有在有限MTL链上的刻画不同，该表示不假设线性性或特定的 coatom。精确真值测试产生针对指定值和非指定值的布尔测试，以及一个派生的存在模态，足以用于饱和论证。我们证明，每个紧致、具有Tarski并性质且在互模拟下强不变的抽象扩展，都与Maruyama版本的Fitting Heyting值模态逻辑具有1-表达等价性。由此，扩展公式的每个精确值纤维都可在Maruyama的精确真值测试模态语言中定义。
英文摘要：
We establish a Lindström-style maximality theorem for Maruyama's exact-truth-test presentation of Fitting's modal logic over a fixed finite Heyting algebra and crisp Kripke frames. Unlike the existing characterization over finite MTL-chains, no linearity or distinguished coatom is assumed. Exact truth tests yield Boolean tests for designated and non-designated values and a derived existential modality sufficient for the saturation argument. We prove that every abstract extension which is compact, has the Tarski Union Property, and is strongly invariant under bisimulation is $1$-expressively equivalent to Maruyama's version of Fitting's Heyting-valued modal logic. As a consequence, every exact-value fibre of an extension formula is definable in Maruyama's exact-truth-test modal language.
