Refutation calculi for lattice-based logics: from display to tableaux

技術的概要：格子ベースの論理における反証計算体系：ディスプレイ計算体系から表構法へ

問題提起
反証計算体系（Refutation calculi）は、与えられた論理の無効な式（または反シーケント）を導出するために設計された形式的体系である。このアプローチは歴史的に表構計算体系（tableau calculi）の発展において決定的な役割を果たしてきたが、いまだにディスプレイ計算体系（display calculi）の枠組みへ成功裏に適応された例はない。ベルナップによって導入されたディスプレイ計算体系は、モダリティ論理や部分構造論理を含む多様な非古典論理に対してカットフリーな提示を提供し得る強力な演繹体系である。しかし、その標準的な応用は証明の構成（有効なシーケントの導出）に焦点を当てている。本論文は、任意の署名を持つ基本的な正規格子拡大に標準的に関連する論理の族である基本 LE-論理（basic LE-logics）の家族に対して、ディスプレイ計算体系の枠組み内で体系的な反証アプローチを開発するというギャップに取り組む。

方法論
著者らは、ディスプレイ計算体系の標準的な役割を逆転させる方法論を提案する。有効なシーケントの証明を構成する代わりに、ディスプレイ計算体系の機構を無効なシーケント（反シーケント）の導出に適合させる。

1. 基礎的枠組み：この研究は、格子拡大上で様々な論理体系（例えば、直交モジュラー論理、ランベック計算体系など）を一般化する基本正規 LE-論理の理論に基づいている。言語には命題変数と、特定の順序型に関連する 2 つの結合子集合 $F$ と $G$ が含まれる。
2. 反証ディスプレイ計算体系（$D.LE^r$）：中核的な貢献は、反証ディスプレイ計算体系 $D.LE^r$ の定義である。この体系は $\Pi \nvdash \Sigma$ の形式の反シーケントを操作する。$D.LE^r$ の規則は標準的なディスプレイ計算体系 $D.LE$ から導出されるが、無効性を導出するように適応されている。
   • 公理：この体系は、明らかな無効性を表す初期反シーケント（例：$\hat{\top} \nvdash \check{\bot}$、$p \nvdash q$）から始まる。
   • 規則：この体系は、ディスプレイ規則、構造的規則、論理的導入規則を採用する。重要なことに、これらの規則は複雑な反シーケントをより単純な反シーケントに分解するように設計されている。
   • 側条件：健全性を保証するために、特定の側条件が課される。特に、ある規則の終端シーケントにおける「残余（residuals）」（演算結合子の残余に対応する構造的結合子）の存在に関する条件である。
3. 証明分析：著者らは、標準的な計算体系 $D.LE$における導出可能なシーケントに対する証明分析を通じて、$D.LE^r$ の性質を確立する。彼らは有効性と無効性の間の対偶関係を利用する。
4. 表構法の構築：最後に、著者らは $D.LE^r$ の規則の対偶形式を採用することで、LE-論理のための終了する表構計算体系を定義する。この表構体系において、分枝は初期反シーケントを含む場合（元のシーケントの無効性を示す）に「開いている」とされ、反復なしにこれ以上規則が適用できない場合に「閉じている」とされる。

主要な貢献と結果

• $D.LE^r$ の導入：本論文は、基本正規 LE-論理に対する最初の反証ディスプレイ計算体系を導入する。これらの計算体系は反シーケントを体系的に導出し、標準的な証明論的アプローチに対する二重の視点を提供する。
• 健全性と完全性：
  • 健全性（定理 1）：著者らは、$D.LE^r$ の規則が完全な $L$-代数のクラスに関して健全であることを証明する。これは、ある反シーケントが導出可能であれば、対応するシーケントは無効であることを示すことによって実証される。証明には、シーケントの複雑性に関する詳細な帰納法と、$D.LE$ におけるカットフリー導出の分析が含まれる。
  • 完全性（定理 2 および系 1）：本論文は、シーケント $\Pi \vdash \Sigma$ が標準的な計算体系 $D.LE$で導出不可能であり（かつ残余を含まない）場合、対応する反シーケント$\Pi \nvdash \Sigma$が$D.LE^r$ で導出可能であることを証明する。これにより、反証計算体系の完全性が確立される。
• 決定可能性：$D.LE^r$ の完全性と $D.LE$ の性質から直接導かれる結果として、著者らは基本正規 LE-論理が構文的に決定可能であると結論づける。
• 終了する表構法：本論文は、$D.LE^r$ を終了する表構計算体系に変換する方法を実証する。定理 3 は、あるシーケントが有効であることと、それに対して閉じた表構木が存在することとが同値であることを確立する。終了性は、規則の結論における結合子の数の減少と、ディスプレイ規則に対する側条件によるサイクルの防止によって保証される。

意義と主張
本論文は、この研究が反証法とディスプレイ計算体系の構造的な強さを統合する上で重要な一歩であると主張する。ディスプレイ計算体系を反証のために成功裏に適応させることで、著者らは広範な格子ベースの論理における無効性を処理するための統一的な枠組みを提供する。

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

1. ディスプレイ計算体系の拡張：証明構成のためのディスプレイ計算体系の伝統的な使用法を超えて反証を含めることで、非古典論理を分析するために利用可能なツールのセットを拡大する。
2. 統一性：このアプローチは、直交モジュラー論理やランベック計算体系など多様な体系を単一の理論的傘の下に覆う、基本 LE-論理の全体に適用される。
3. 決定可能性と表構法：反証ディスプレイ計算体系から終了する表構法を導出することは、これらの論理に対する実用的な決定手続きを提供し、抽象的な証明論的性質と具体的なアルゴリズム的手法を結びつける。

著者らは、この研究が、分配性 LE-論理へのプラットフォームの拡張、公理的拡張への対応、シーケントと反シーケントの両方を含む体系における「アンチカット」除去の探求など、将来の研究の方向性を開くことに言及して結論づける。彼らは謙虚な立場を維持し、これらを分野内のすべての未解決問題に対する決定的な解決策というよりも、有望な第一歩およびさらなる調査のための潜在的な道筋として提示している。