技術的概要：石炭代数的非整礎証明：再帰性と GTC

問題提起

循環証明を含む非整礎証明系は、モダル$\mu$計算や高次不動点論理など、(共)帰納を伴う論理において不可欠である。有限の導出木を有する有限証明とは異なり、これらの系は無限の導出木を許容する。その結果、整礎性に基づく標準的な木深さに関する構造的帰納法によって健全性を確立することはできない。代わりに、これらの系は健全性を保証するために、導出木内の無限経路に対する制約である**大域トレース条件（GTC）**を課す。

循環証明に対する様々な圏論的アプローチ（例：$\mu$-二完備圏、トレース圏）が存在するにもかかわらず、健全性を保証する GTC の圏論的特徴付けを提供することは依然として重大な課題である。主な困難点は以下の通りである：

1. 大域対局所： GTC は導出木全体に対する制約を課すため、標準的な圏論的推論の局所的かつ構成的な性質と矛盾する。
2. 無限構造： 非整礎証明は無限となりうるため、意味論的射を構成するために標準的な構造的帰納法を用いることができない。
3. 再帰的石炭代数理論の欠落： 再帰的および整礎な石炭代数は一意な解（意味論的解釈）を保証するが、非整礎証明の導出木はしばしば非整礎な石炭代数をもたらす。既存の理論は、なぜ特定の非整礎の場合（Capretta や Jeannin らの「降下列」の例など）において一意な解が存在するのかを直接的に説明していない。

手法

本論文は、非整礎証明系のための石炭代数的枠組みを開発し、導出木を石炭代数としてモデル化し、GTC をこれらの石炭代数のグラフ上の条件として定式化する。

1. 前層上の家族的関手による石炭代数

著者らは、導出木を、前層圏$\widehat{\mathcal{J}}$上の家族的関手$F$を有する石炭代数$c: C \to FC$としてモデル化する。

• 家族的関手： これらは、特定のファイブレーション性質を持つ圏の図式である多項式を通じて定義される多項式関手の一般化である。これにより、節は判断によってラベル付けされ、分岐構造は推論規則によって決定され、パラメータや文脈を自然に扱うことができる。
• 石炭代数のグラフ： 石炭代数のグラフの概念に基づき、本論文は、$\mathbf{Set}$上の自己関手から前層上の自己関手へと、石炭代数の整礎性とそれらに関連するグラフにおける無限経路の不在との等価性を拡張する（定理 1.9）。

2. 随伴と再帰的像

証明の非整礎性に対処するため、この枠組みは随伴に沿った石炭代数から代数への射の対応を利用する。

• 戦略： 元の石炭代数$c$が再帰的であることを要求する代わりに、本論文は、適切な左随伴$L$（具体的には、順序数注釈によって誘導される基底変換関手）によるその像が再帰的かどうかを調査する。
• メカニズム： $Coalg(L)(c)$が再帰的であり、かつ対象となる意味論的代数$a$が右随伴$R$の像に含まれる（すなわち$a \cong Alg(R)(a')$）場合、$c$に対して一意な石炭代数から代数への射が存在する（命題 2.4）。
• 直観： これは、随伴に沿って引き戻すことで得られる追加の次元（順序数注釈）を導出グラフに付与することに相当する。この拡張により、元のグラフが整礎でなかったとしても、グラフを整礎化しうる。

3. トレース構造と GTC

GTC はトレース構造$(pfml, prog)$を用いて形式化される：

• トレース構造： 多項式の圏（$VPoly$）における射であり、辺に沿って式（またはマークされた式）を追跡し、「進行する」辺の部分集合（通常は不動点の展開に対応する）と組み合わされる。
• GTC の定義： 前証明が GTC を満たすとは、そのラベル付きグラフにおけるすべての無限経路が、ある接尾語に沿って無限に進行するトレースを許容する場合をいう。
• 順序数注釈： この枠組みは、順序数で注釈された判断を持つ抽象的証明系$P^\gamma$を構成する。忘却関手$u_\gamma: \mathcal{J}dg^\gamma \to \mathcal{J}dg$は必要な随伴を誘導する。

主要な貢献と結果

1. 前層へのグラフ理論の拡張

本論文は、$\mathbf{Set}$上の自己関手から前層圏上の自己関手へと、グラフの整礎性と石炭代数の再帰性との等価性を拡張する（定理 1.9）。これは、家族的関手に対する石炭代数のグラフを定義し、関手が交わりと逆像を保存することを証明することによって達成される。

2. 再帰的像を通じた健全性

本論文は**健全性定理（定理 4.13）**を確立する：前証明$c$が GTC を満たすならば、$a$が順序数注釈による持ち上げられた代数の像に含まれる限り、$c$から任意の意味論的代数$a$への一意な石炭代数から代数への射が存在する。

• これは、標準的な意味で再帰的ではないが一意な解を許容する非整礎な例（降下列など）に対する石炭代数的説明を提供する。
• GTC が（順序数注釈を伴う）「拡張された」石炭代数を再帰的にすることを保証することを示す。

3. GTC と再帰性の特徴付け

本論文は、GTC と再帰性の間の双方向の特徴付けを確立する：

• GTC $\implies$ 再帰性： 前証明が GTC を満たすことは、順序数注釈関手によるその像が再帰的であることと同値である（定理 4.17）。
• 再帰性 $\implies$ GTC： 前証明が再帰的であることは、すべてのトレース構造に対して GTC を満たすことと同値である（命題 4.14）。
• これにより、GTC は本質的に、適切な随伴に沿った輸送の後に関連する石炭代数が再帰的になることを保証する条件であることが明確になる。

4. 具体的な具体化

この枠組みは、3 つの証明系を通じて実証される：

1. モダル$\mu$計算： GTC が$\nu$スレッド（最大不動点の無限展開）の存在に対応する非整礎証明系。順序数注釈は、最大不動点に対する標準的な近似に対応する。
2. 高次不動点論理（HFLN）： $\mu$と$\nu$の両方のトレースの追跡を必要とする系であり、複雑なトレース構造を処理する枠組みの能力を実証する。
3. $\mu$-二完備圏： Santocanale の循環証明系の非整礎変種であり、判断が変数割り当てに随伴的に変化する非離散な判断の圏を処理する枠組みの能力を示す。

意義と主張

本論文は、その主要な貢献として、健全性を成功裏に保証する非整礎証明の圏論的抽象化であると主張する。

• 概念的洞察： GTC は単なる操作的なチェックではなく、適切な随伴（具体的には順序数意味論に導かれた随伴）のレンズを通して見た際に石炭代数が再帰的になることを保証する構造的性質である。
• 統合： この枠組みは、家族的関手と随伴を含む単一の石炭代数的メカニズムの下で、様々な非整礎証明系の健全性の扱いを統合する。
• 理論的ギャップの埋め合わせ： 既存の再帰的石炭代数理論におけるギャップに対処し、随伴に沿った意味論の「持ち上げ」を通じて、非整礎な石炭代数に対してどのように一意な解が存在しうるかを説明する。

著者らは、この枠組みが健全性を確立する一方で、完全性、カット除去、およびこの石炭代数的設定におけるリセット条件やバウンススレッドなどの他の健全性条件に対処するためには、今後の研究が必要であると指摘している。