Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations

技術要約：ゲーデル・レーブ証明可能論理のためのシーケント体系の統一

問題提起
本論文は、ゲーデル・レーブ（GL）証明可能論理の証明論における重大な空白に対処している。GLは多様で豊かな無カット・シーケント形式を備えているが、それらの間の関係性は完全には確立されていなかった。具体的には、先行研究において以下の対応関係が確立されていた：

1. 構造的体系： Negriのラベル付きシーケント体系（$G3KGL$）とPoggiolesiのツリー・ハイパーシーケント体系（$CSGL^*$）の間（GoréおよびRamanayakeによる）。
2. 証明構造の一般化： SambinとValentiniのGentzen体系（$GL_{seq}$）、Shamkanovの非整列体系（$GL_\infty$）、およびShamkanovの循環的体系（$GL_{circ}$）の間（Shamkanovによる）。

しかし、構造的体系（$G3KGL$, $CSGL^*$）と証明構造の一般化（$GL_{seq}$, $GL_\infty$, $GL_{circ}$）の間の相互翻訳可能性は、未解決の問題として残されていた。固有の困難さは、複雑な構造的シーケント（Gentzenシーケントのグラフやツリー）を利用する証明を、標準的なGentzenシーケントを使用する証明へと変換するプロセスにあり、これにはこの余分な構造的データの「脱ぎ捨て」が必要となる。

手法
著者であるTim S. Lyonは、これらの異なる形式主義の間の溝を埋める、一連の構文的証明変換を構築することで、この未解決問題を解決する。手法は主に以下の3つのフェーズで進行する：

1. エンドアクティブ形式への再構成： 本論文では、まずツリー・ハイパーシーケント体系 $CSGL^*$ の証明を「エンドアクティブ（end-active）」形式へと再構成する方法を示す。エンドアクティブな証明では、推論規則の主式および補助式は、ツリー・シーケントの（前）葉（leaf）においてのみ現れる。これは、$CSGL^*$ における規則の高さ保存的な可逆性を利用して、非エンドアクティブな規則を証明木の下方へと置換することによって達成される。

2. 線形化（Linearization）： 新しい「線形化テクニック」を導入し、これらのエンドアクティブなツリー・シーケント証明を**線形入れ子シーケント（linear nested sequents）**を用いた証明へと変換する。このテクニックは、ツリー・シーケント内の根（root）から葉（leaf）に至る特定のパスを特定し、サブツリーを「刈り取る（pruning）」ことを含み、実質的にツリー構造をGentzenシーケントの線形な列へと崩壊させる。このプロセスにより、新しい計算体系である LNGL（GLのための線形入れ子シーケント計算）が得られる。

3. 標準形とGentzenへの翻訳： 本論文は、LNGLにおける証明が特定の標準形へと変換可能であることを示す。この形式では、証明は反復的な段階に従って進行する：局所的な規則、それに続く伝播規則（$4L$ および $\Box L$）、そして最後に様相規則（$\Box R$）である。この構造化された証明は、その後、SambinとValentiniのGentzen体系（$GL_{seq}$）へと翻訳される。最終的に、標準的な変換を用いて $GL_{seq}$ の証明を $G3KGL$および循環的／非整列体系（$GL_{circ}$, $GL_\infty$）へと写像する。

主な貢献

• 新計算体系 (LNGL)： 本論文は、ゲーデル・レーブ論理のための初のカットフリー線形入れ子シーケント計算である LNGL を導入する。この体系は、Gentzenシーケントの列に基づいて動作し、可逆性とカット除去可能性といった基本的な性質を保持している。
• 斬新な線形化テクニック： 著者は、ツリー・ハイパーシーケント体系から線形入れ子シーケント体系を抽出するための一般的な手法を提示している。このテクニックは、他の様相論理や関連する論理から新しい線形入れ子体系を生成するために適用可能であると推測されている。
• 完全な証明論的対応： 本論文は、以下の体系間の完全な六方向の構文的対応関係を確立している：$G3KGL$, $CSGL^*$, $LNGL$, $GL_{seq}$, $GL_\infty$, $GL_{circ}$。
• 構成的な写像： 本研究は、構造的体系（ラベル付き、ツリー・ハイパーシーケント、線形入れ子）と循環的証明体系（$GL_{circ}$）の間の初の構成的な証明写像を提供している。

結果
主要な結果は、GLにおける6つの主要なシーケント体系のいずれの証明も、他のいずれかの証明へと構文的に変換できることを示すことである。具体的には：

• $CSGL^*$ の証明は、エンドアクティブな証明へと変換され、次いでLNGLへと線形化される。
• LNGL の証明は、標準化され、$GL_{seq}$ へと変換される。
• $GL_{seq}$ の証明は、$G3KGL$および循環的体系（$GL_{circ}$, $GL_\infty$）へと変換される。
• 本論文は、$LNGL$ がGLに対して健全かつ完全であることを確認し、また $LNGL$ の証明が、様相規則と局所規則の適用が段階的に繰り返される標準形に置けることを示している。

意義
本論文は、ゲーデル・レーブ論理の証明論的対応関係の「絵を完成させる」と主張している。これらの構文的変換を確立することで、本研究は、各形式主義において独立した証明を必要とせずに、結果（補間特性や複雑度の境界など）を体系間で転送することを可能にする。さらに、LNGLの導入は、複雑度の最適性を備えた証明探索のための新しいツールを提供すると同時に、線形化テクニックは他の論理のための線形入れ子体系を生成するための潜在的な経路を提供する。また、本研究は、構造的体系と循環的証明の間の初の構成的な写像を提供し、様相論理における帰納的／共帰的推論の扱いに関する異なるアプローチ間の溝を埋めている。