Computation by infinite descent made explicit

問題と動機
$\mu$-計算の文脈に端を発する非整列（non-wellfounded）証明論は、帰納的および共帰的な推論を表現するために無限の証明木を許容する。中心となる課題は、有効な証明と無効な導出木の区別となる正当性基準を定義することである。従来の基準、例えば「トレース（trace）」や「進行スレッド（progressing thread）」条件は、証明木のすべての無限枝が、最小不動点が左側で、あるいは最大不動点が右側で無限に展開される特定の論理式のシーケンスを含むことを要求する。

しかし、近年の研究 [BDKS22] は、トレースに基づく条件の限界、特に構成性に関する問題を特定した。彼らは、カットによってトレースが分断されるケースを扱うために「バウンシング・スレッド（bouncing threads）」を導入したが、この条件は決定不能であり、証明系の構造規則と相性が悪いことも指摘している。さらに、カリー＝ハワード対応が証明をプログラムと見なす一方で、これらの複雑な妥当性条件の下で、非整列な証明が計算可能な関数（正規化）を表現していることを確立することは容易ではない。

本論文は、明示的な順序数変数を用いた証明系の探索を通じて、非整列な証明の構成性と計算的内容という問題に取り組む。このアプローチは、Dam, Gurov, および Sprenger [DG02, SD03a] によって先駆的に行われたもので、不動点論理式に順序数の近似値を表す変数を注釈として付与するものである。本論文は、この枠組みが、標準的なトレース条件が捉えきれない証明を捉えつつ、決定可能であり、かつ堅牢なカリー＝ハワード解釈をサポートする、より透明性の高い正当性基準を提供できるかどうかを調査する。

方法論
著者である Sebastian Enqvist は、帰納的（$\mu$）および共帰的（$\nu$）定義が拡張された直観主義命題論理のための非整列証明系を開発する。核心となる手法は以下の通りである：

1. 構文の拡張： 言語は明示的な順序数変数と制約を用いて拡張される。$\mu X. A$ のような論理式は $\mu_\alpha X. A$ と注釈され、ここで $\alpha$ は順序数項（変数 $a, b, \dots$ または定数 $\infty$）である。シーケントには、これらの順序数項間の不等式を表す制約木 $O$ が含まれる。
2. 妥当性基準： 導出は、すべての無限枝に対して、順序数変数の無限降下鎖（$a_0 > a_1 > a_2 > \dots$）が最終的にその枝において成立する場合に**妥当（valid）**であると定義される。これにより、帰納的推論の健全性の中心となる「無限降下」の議論が、構文の中に明示的に組み込まれる。
3. 計算可能性意味論： 閉じた導出に対する**計算可能性（computability）**の概念を定義する。証明は、論理結合子および不動点に対応する特定の帰納的節へと簡約される場合、計算可能である。例えば、最小不動点 $\mu_\infty X. A$ の証明は、ある順序数 $\xi$ に対して近似形 $\mu_\xi X. A$ の証明へと簡約されるとき、計算可能である。
4. カット簡約： 証明の計算的振る舞いを定義するために、一連の書き換え規則（カット簡約および置換規則）を導入する。この系は、これらの特定の規則の下で単一性を持ち、正規化の明確な概念を可能にするよう設計されている。
5. 圏論的モデリング： 閉じた論理式を対象とし、証明の同値類を射とする証明の圏を構築する。著者は、この圏がそれぞれの不動点論理式に対する初期代数および終末余代ルの構造をサポートすることを証明する。

主要な貢献と結果

• 妥当な証明の計算可能性： 主要な結果（定理 4.9）は、すべての妥当な証明（無限降下鎖条件を満たすもの）が計算可能であることを確立する。これは、もし証明が計算不可能であれば、順序数の降下鎖を持たない無限枝を構成できてしまい、妥当性条件に矛盾することを示すことで証明される。
• 有限論理式の正規化： この計算可能性の結果として、本論文は「有限論理式」（$\top, \land, \lor, \mu$ から構成され $\nu$ を含まない論理式）の証明が常に一意な正規形に正規化されることを証明する（定理 4.11）。
• 関数の表現： 本システムは、$N, \dots, N \vdash N$（ここで $N$ は自然数を表す）という形式のシーケントの証明に関する正規化結果をもたらす。そのような証明は、自然数上の一意な全単射関数を表現する（定理 4.12）。
• 「バウンシング」ケースの処理： 本論文は、順序数変数の枠組みが、標準的な進行スレッド条件では失敗するが「バウンシング・スレッド」条件の下では妥当とされる証明を捉えられることを示す。例として、カットが標準的なトレースを中断するが、カット論理式内の明示的な順序数変数が降下論証を保持することで、その証明が本システムにおいて妥当となるケースが挙げられている。
• 圏論的意味論： 最小不動点が初期代数に、最大不動点が終末余代数に対応する圏論的モデルを構築する（セクション 5.2 および 5.3）。これにより、計算可能性の意味論が、帰納的および共帰的型に対する標準的な圏論的解釈と一致することが確認される。
• 決定可能性： バウンシング・スレッド条件とは異なり、順序数変数に基づく妥当性基準は決定可能であることが知られている [SD03a]。

意義と主張
本論文は、Baelde ら [BDKS22] によって開始された、標準的なトレース条件を超えた、非整列な証明のための自然な妥当性基準を見出すというプロジェクトへの寄与となるパイロット研究として位置づけられている。著者は、明示的な順序数変数を用いる Dam-Gurov-Sprenger の枠組みが、この目的のための適切な候補であることを主張している。

その意義は、主に以下の2つの観察にある：

1. 表現力： この妥当性条件は、標準的な進行スレッド条件では妥当と認識されない証明（特に「バウンシング」挙動を持つもの）を捉える。
2. 計算的意味： 計算可能性の意味論を提供することで、本論文は、このシステムにおけるすべての妥当な証明が、明確に定義された計算可能なプログラムを表現していることを示している。これは、構文的な妥当性条件と、停止性／計算可能性という意味論的要件との間の溝を埋めるものである。

著者は、本論文が論理に対する完全なカット除去定理（これには追加の置換規則が必要となる）を提供しているわけではなく、また、順序数変数システムがバウンシング・スレッド条件と同等の能力を持つという決定的な証明も提供していないことを控えめに述べている。代わりに、すべてのバウンシング・スレッド妥当な証明が順序変数を用いて表現可能であるかという問いは、今後の研究に向けた未解決問題として残されている。本研究は、カリー＝ハワードの観点から順序変数のさらなる探求を動機付けるものである。