Four intuitionistic modal connectives

技術的要約：4つの直観主義的様相連結辞

問題提起
本論文は、直観主義様相論理（IML）の基礎的な意味論と公理化を取り上げている。伝統的に、IMLは関係構造 $(W, \leq, R, V)$（ここで $\leq$ は前順序であり、$R$ は二項関係である）の中で様相連結辞を解釈する。ここには、可能性演算子に関する2つの主要な学派の間で中心的な対立が存在する：

1. フィッシャー・セルヴィ（Fischer Servi）のアプローチ： 可能性（$\diamond_{FS}$）を、「$s \models \diamond_{FS} A$ であるとは、$sRt$かつ$t \models A$となる$t$が存在する」と定義する。このアプローチは通常、継承特性（$\leq$ に関する単調性）を満たすために、フレームのクラスを「前方および後方合流的（forward and backward confluent）」なモデルに制限する必要がある。
2. ウィジェセーラ（Wijesekera）のアプローチ： 可能性（$\diamond_{W}$）を、「$s \models \diamond_{W} A$ であるとは、すべての $t \geq s$ に対して、$tRu$かつ$u \models A$となる$u$ が存在する」と定義する。このアプローチは、継承特性を保持するために合流性を厳格に要求しない。

著者らは、合流的なモデルに議論を限定することは、ある種の直観主義一階述語論理のバリエーションを特権化する恣意的な選択であると主張している。さらに、IMLを一階論理へ標準的に翻訳する場合、合流的なモデルのみに制限されると、意図された意味論を捉え損ねることが多いとも指摘している。したがって、本論文は、フレームのクラスを事前に制限することなく、4つの異なる様相連結辞を組み込んだ統一的な枠組みを構築し、直観主義的様相の全容を探求することを目指している。

方法論
著者らは、関係意味論、対応理論、代数的証明系、およびモデル論的手法を厳密に組み合わせている：

1. 構文と意味論：

   • 標準的な直観主義的連結辞（$\to, \top, \bot, \lor, \land$）および双対含意／共含意（$\leftarrow$）を含む言語を導入する。
   • 4つの様相演算子を定義する：
     • $\Diamond$ （プレノーシル（Přenosil）型の可能性）：$s \models \Diamond A$ であるとは、$\exists t \leq s, \exists u (tRu \land u \models A)$ である。
     • $\Box$ （フィッシャー・セルヴィ型の必然性）：$s \models \Box A$ であるとは、$\forall t \geq s, \forall u (tRu \to u \models A)$ である。
     • $\Diamond$ （ウィジェセーラ型の可能性）：$s \models \Diamond A$ であるとは、$\forall t \geq s, \exists u (tRu \land u \models A)$ である。
     • $\blacksquare$ （双対必然性）：$s \models \blacksquare A$ であるとは、$\exists t \leq s, \forall u (tRu \to u \models A)$ である。
   • 意味論は、すべてのフレームのクラス（合流性の制限なし）上で定義される。そして、これらすべての定義において継承特性が保持されることが証明されている。

2. 対応理論：

   • 基本的なフレームのクラス（直列、反射的、対称的、推移的、合流的など）の様相的定義可能性を調査する。
   • 符号付き論理式と推論規則を用いて、フレームの性質を特徴付ける。
   • 特定のフレームクラスに対する様相的定義可能性問題の決定不能性を証明するために、モデル論における「相対化特性（Relativization Property）」を用いる。

3. 公理化と完全性：

   • 符号付き論理式（正および負）を用い、一様置換および特定の推論規則（双対含意や様相間の相互作用に関する規則を含む）によって閉じられたヒルベルト型の体系を提示する。
   • 著者らは、「バランスの取れたクリップ（balanced clips）」（素なフィルター、素なイデアル、および補助的な論理式のトリプルからなるもの）を用いて**標準モデル（Canonical Model）**を構築する。この構成は、4つの様相と双対含意の複雑な相互作用を扱うために必要である。
   • 最小論理、および特定のフレームクラスに対応するその拡張に対する完全性定理を証明する。

4. 決定可能性：

   • 決定可能性を証明するために、最小IMLを古典的一階論理の**単項二変数ガード付き断片（Monadic Two-Variable Guarded Fragment）**へと埋め込む。
   • 直観主義的論理式をガード付き一階論理式へと写像する翻訳関数を定義し、ガード付き断片の既知の決定可能性を利用する。

主な貢献と結果

• 統一的枠組み： 本論文は、4つの異なる様相連結辞（$\Diamond, \Box, \Diamond, \blacksquare$）を単一の直観主義的枠組みの中に統合することに成功し、それらが全フレームのクラスにおいて相互定義可能ではないことを示した。
• 除去可能性の分析： 前方および下方合流的なフレームのクラス（$C_{fd}$）上では、4つの連結辞すべてが除去可能（相互定義可能）であることが示される。しかし、$C_{bdu}$ のようなより広いクラスにおいては、それらは区別される。
• 対応結果：
  • 前方合流的（$C_f$）および下方合流的（$C_d$）なフレームのクラスは、正に定義可能である。
  • 反射的（$C_{ref}$）、対称的（$C_{sym}$）、推移的（$C_{tra}$）、ユークリッド的（$C_{Euc}$）、および決定論的（$C_{det}$）なフレームのクラスは、全フレームのクラス（または $C_{fbdu}$ のような特定のサブクラス）に対して、様相的に定義可能ではない。
  • 後方合流的（$C_b$）および上方合流的（$C_u$）なフレームのクラスは、$C_{fd}$ に対して様相的に定義可能ではない。
• 公理化： 最小論理（$L_{min}$）および反射性、直列性、合流性の性質に対応するその拡張に対する完全な公理化を提供する。最小論理は、すべてのフレームの論理であることが示されている。
• 決定可能性： 最小直観主義様相論理（$L_{min}$）およびそのいくつかの拡張（反射的、直列的、合流的）のメンバーシップ問題が決定可能であることを証明する。これは、問題を単項二変数ガード付き断片の充足可能性問題へと還元することによって達成される。
• 定義可能性の決定不能性： 基本的なフレームのクラスが、様相的、正、あるいは負に定義可能であるかどうかを判定する決定問題が決定不能であることを証明する。

意義と主張
著者らは、合流的なモデルへの恣意的な制限を回避することで、より自然で制約の少ないIMLの基礎を提供していると主張している。双対含意と4つの様相を導入することにより、直観主義的な様相挙動の全範囲を捉える、対称的かつ包括的な言語を提供している。

本論文は、最小論理の決定可能性は確立されているものの、この問題の計算量クラスは依然として未解決の問いであることを謙虚に記している。また、完全性の証明において特定の推論規則（具体的には $R8+$ および $R8-$）が使用されたが、これらの規則が有限個の公理の集合に置き換えられるかどうかは現時点では不明であることも強調している。さらに、対称的および推移的なフレームに対応する論理の有限公理化に関する未解決問題や、この設定に濾過（filtration）の手法を適応できる可能性についても問いを投げかけている。

本研究は、従来のフィッシャー・セルヴィとウィジェセーラの二分法を超えて、異なる直観主義的様相意味論とそれに対応するフレームの性質との相互作用を理解するための基礎的な一歩となるものである。