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. 基礎となる論理の定義： crispなクリプキ・フレーム上のMaruyama版Fittingの論理（$FML_L$）を利用する。ここで、論理式は有限ヘイティング代数 $L$ の値を取る。言語には、$\phi$ が $\ell$ の値を取るとき、かつそのときに限り $T_\ell \phi$ が1となるような、正確な真理テスト $T_\ell$ が含まれる。
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. 抽象的拡張： 本論文では、コンパクト性、タルスキ和の性質、および双模倣（bisimulation）に対する強い不変性の3つのモデル論的性質を満たす抽象的な拡張 $\mathcal{L}$ を検討する。
4. 飽和とアンラベリング： 証明は、アンラベリング技法を用いて飽和的な初等拡張を構成する。著者は、「後続タイプ（successor types）」を定義するために派生された様相 $\Diamond_1$ を活用し、これらのタイプが実現されるモデルを構築するためにコンパクト性とタルスキ和の性質を利用する。
5. 決定補題（Decision Lemma）： 決定的なステップとして、$(D\psi, N\psi)$ を用いて、基礎となる論理におけるいかなる仮説的な新しい論理式をも分離する「決定補題」がある。これは、鎖ベースの証明で使用された「1の直前の前置要素」という議論を置き換えるものである。

主要な貢献と結果

• Lindström極大性定理： 主要な結果（定理1）は、任意の固定された有限ヘイティング代数 $L$ に対して、Maruyama版のFittingの様相論理は、コンパクトであり、タルスキ和の性質を持ち、双模倣に対して強く不変であるすべての抽象的拡張の中で、1-表現力の観点から極大であることを述べている。
• 線形性の仮定の除去： 本論文は、線形に順序付けられた代数（MTL鎖）から任意の有限ヘイティング代数へと、極大性の結果を成功裏に一般化した。証明は、正確な真理テストが、線形性や特定の余原子を必要とせずに、十分な分離能力を提供することを実証している。
• 正確な値の定義可能性： 極大性定理の帰結として（系1）、本論文は、拡張 $\mathcal{L}$ における任意の論理式 $\phi$ と任意の値 $\ell \in L$ について、$\phi$ が正確に値 $\ell$ を取る点付きモデルの集合が、基礎となる論理の論理式によって定義可能であることを証明している。具体的には、「正確な値のファイバー（exact-value fibre）」は定義可能であるが、これは必ずしも $\phi$ の完全な $L$ 値の意味論を再現する単一の論理式 $FML_L$ が存在することを意味しないことを論文は注記している。
• 飽和モデルにおけるヘンネシー・ミレナー特性： 本論文は、$FML_L$-飽和モデルにおいて、様相的同値が双模倣を意味することを確立し、標準的なヘンネシー・ミレナー現象をこの多値の設定へと拡張している。

意義と主張
本論文は、非線形な代数上の多値様相論理に関する文献の空白を解消することを主張している。正確な真理テスト（$T_\ell$）が、指定値と非指定値を分離できるブール値の決定ペア（$D\phi, N\phi$）を生み出すことを示すことにより、著者は、Lindströmの極大性において、基礎となる代数の構造的制約（具体的には線形性）は必要ではないことを示している。

その意義は以下の点にある：

1. 一般化： 線形な鎖という限定的な設定を超えて、Lindströmの定理の範囲を有限ヘイティング代数というより広いクラスへと拡張したこと。
2. メカニズムの特定： 正確な真理テストから派生したブール値テストが、非線形な設定における値の分離と飽和の議論のための決定的なメカニズムであることを特定したこと。
3. 定義可能性： 基礎となる論理が、「妥当な」拡張における任意の論理式の正確な値のファイバーを定義するのに十分な表現力を持っており、Maruyamaの提示の堅牢性を強化していることを確立したこと。

著者は今後の方向性について謙虚な姿勢を保っており、タルスキ和の性質を弱めることができるか、どのように $L$ 値（ファジー）の到達関係を扱うか、また個別の正確な値の定義を、完全な意味論を再現する単一の論理式へと統合できるかといった未解決の問いを挙げている。