Heyting 代数上模糊多模态逻辑的亨氏-米尔ner 类型定理

在最近的论文中，我们引入了两种类型的模糊模拟 (前向和后向) 以及五种类型的模糊双态 (前向、后向、前向-后向、后向-前向和 regular)，用于 complete linearly ordered Heyting 代数上的模糊多模态逻辑的 Kripke 模型之间。本文中，对于给定的非空模态公式集合 $\Psi$，我们引入概念 weak bisimulation，用于表达两个世界 $w$ 和 $w'$ 中对 $\Psi$ 中有效模糊公式集合的等价程度，即以 $\Psi$ 中的公式衡量世界 $w$ 和 $w'$ 之间的模态等价程度。我们证明了多个亨氏-米尔ner 类型定理。第一个定理确定，针对 plus-formulae 集合，image-finite Kripke 模型之间最大 weak bisimulation 等于最大 forward bisimulation。第二个定理确定，针对 minus-formulae 集合，domain-finite Kripke 模型之间最大 weak bisimulation 等于最大 backward bisimulation。第三个定理确定，针对所有模态公式集合，degree-finite Kripke 模型之间最大 weak bisimulation 等于最大 regular bisimulation。