The proof theory and semantics of second-order (intuitionistic) tense logic

技術的要約：二階（直観主義的）時制論理の証明論と意味論

問題と動機
本論文は、古典的および直観主義的基盤の両方における二階時制論理の基礎的な展開に取り組んでいる。二階論理は数学および計算論理学における標準的な道具であるが、そのメタ論理的基礎、特に証明論と意味論に関しては、重大な課題を投げかけてきた。直観主義的様相論理における特定の困難は、古典論理のようにボックス（$\Box$）からダイヤモンド（$\Diamond$）を定義できないため、$\Diamond$ の適切な公理化に関する合意が欠如していることである。様々な提案（例：CK, IK）が存在するが、それらはしばしば恣意的な公項の選択を伴う。

著者らは、二階量化を用いた統一的なアプローチを提案している。主要な観察として、二階直観主義論理においては、正の連結辞は負の断片から定義可能である。具体的には、本論文は、前向きおよび後ろ向きの様相（時制論理）の両方が含まれている場合、ボックス（$\Box$）と後ろ向きボックス（$\blacksquare$）のみを用いてダイヤモンド様相（およびその関連理論）を復元できることを示している。これにより、$\Diamond A$ を $\forall X(\Box(A \to \blacksquare X) \to X)$ として定義することが可能になり、恣意的な公理化を回避できる。

方法論
著者らは、三つの並行した二階時制論理の定義を開発している：

1. 公理的定義： $Kt2$（古典的）および$IKt2$（直観主義的）という体系を定義する。これらは、正規様相と時制ペアの随伴公理を備えた二階命題論理を拡張したものである。決定的なのは、非限定的な定義を可能にする完全な包括公理（comprehension axiom）を含んでいる点である。
2. 意味論的定義： 直観主義的なケースについては（双）関係意味論を、古典的なケースについては関係意味論を導入する。これらの構造には、部分順序（直観主義のため）と到達関係が含まれる。中心的な特徴は、「包括性（comprehensiveness）」の要求であり、集合のドメインにはすべての論理式の拡張が含まれ、これにより包括公理をモデル化している。著者らはまた、「述語構造」（世界は古典的様相モデルであるもの）を定義し、それらが双関係構造と等価であることを示している。
3. 証明論的定義： ラベル付きシーケント計算（$\ell Kt2$ および $\ell IKt2$）を提案する。これらの体系は、意味論を内部化するために、世界のラベルと関係原子を使用する。直観主義的なケースについては、証明探索の議論を容易にするために、中間的な多後続シーケント計算（$m\ell IKt2$）が導入されており、これが単後続バージョンに対して保守的であることが示されている。

核心となる技術的戦略は、これら三つの定義が一致することを証明することである。これは、公理的な証明可能性、意味論的な妥当性、および証明論的な導出可能性を繋ぐ「グランド・ツアー」として可視化される。完全性の証明は、非限定性（impredicativity）の障壁を克服するために、シュッテ（Schütte）のセミ・バリュエーション（semi-valuations）の概念とプラウィッツ（Prawitz）の可能値（possible values）の概念に適応させた証明探索議論に依拠している。

主要な貢献と結果

• 二階量化によるダイヤモンドの定義： 本論文は、時制様相が存在する場合、ダイヤモンド様相が二階直観主義論理において $\Diamond A \iff \forall X(\Box(A \to \blacksquare X) \to X)$ として定義可能であることを確立している。これにより、恣意的な公理の選択なしに、フィッシャー・サーヴィ（Fischer Servi）の理論およびシンプソン（Simpson）の $IK$、およびイヴァルト（Ewald）の $IKt$ を復元している。
• 健全性と完全性：
  • 直観主義的： 体系 $IKt2$ が、包括的な双関係意味論に対して健全かつ完全であることが証明されている（主要定理 3.3）。
  • 古典的： 体系 $Kt2$ が、包括的な関係意味論に対して健全かつ完全であることが証明されている（主要定理 3.14）。
• カット除去可能性（Cut-Admissibility）： 本論文は、ラベル付きシーケント計算 $\ell Kt2$ および $\ell IKt2$ におけるカット除去可能性を確立している（主要定理 4.2）。これは、失敗した証明探索から反例モデルを構成する証明探索議論を通じて達成される。
  • 古典的なケースでは、関係的反例モデルを抽出するために、シュッテのセミ・バリュエーションとプラウィッツの可能値を適応させている。
  • 直観主義的なケースでは、クリプキ・モデルの部分順序を扱うために、より複雑な、証明探索「枝（branch）」ではなく「木（tree）」を構築する必要があり、最終的に述語モデルの反例モデルが得られる。
• ラベル付き証明の公理的健全性： 論文は、ラベル付き証明から公理的証明への翻訳を提供しており（定理 7.1）、これにより等価性のサイクルを完結させている。これには、ラベル付きポリツリー・シーケントを時制論理式として解釈し、各推論規則が公理的体系において許容される規則に対応することを示すプロセスが含まれる。
• 古典的・直観主義的関係： 本論文は、ゲーデル＝ジェンツェンの翻訳と同様に、負の翻訳を通じて、古典的二階時制論理（$Kt2$）が直観主義的体系（$IKt2$）に埋め込み可能であることを確立している（定理 8.2）。

意義
本論文は、二階時制論理のための強固で統一された基礎を提供すると主張している。公理的、意味論的、および証明論的な定義が一致することを実証することで、選択された最小限の公理化を正当化している。この研究は、二階量化の表現力を活用することで、恣意的な公理なしに直観主義的な設定で正の様相を定義するという特定の課題に対処している。

方法論は、古典的および直観主義的な設定の両方に適用可能であるように提示されており、直観主義的なケースでは、非限定性とクリプキ・モデルの構造を扱うための新しい技術的な適応を必要としている。結果は、二階時制論理のメタ論理的研究において重要である。なぜなら、この領域では、完全な意味論（再帰的に列挙可能ではないもの）に制限されていた、完全な証明論的説明（カット除去を含む）を提供するからである。本論文は、関連研究でも指摘されているように、知識表現や人工知能の分野で二階様相論理を採用するために必要な理論的ツールへの貢献として位置づけられている。