循環証明体系（帰納的定義付き一階述語論理）
概要
循環証明体系（cyclic proof system）とは、帰納的定義付き一階述語論理において、有限導出木の未閉鎖葉を同じシークエントをもつ節点へ戻し、有限グラフで証明を表す体系である。Brotherston–SimpsonのCLKIDωでは、グラフを展開して得られるすべての無限道に、帰納的原子を真のcase子孫へ無限回移すtraceが存在するという大域trace条件を課す。この条件が順序数による無限降下を保証し、標準意味論に対する健全性を与える。条件の検査は判定可能であり、明示的帰納法の体系LKIDの証明を含むが、一般にはそれより真に強い。
前提知識: 一階述語論理, シークエント計算, 帰納的定義, 整礎関係, 有限オートマトン
定義
本記事では Brotherston–Simpson の記法に従い、帰納的定義付き古典一階述語論理を FOLID、その無限降下型の無限証明体系を $\mathtt{LKID}^{\omega}$、有限グラフで表現できる循環部分体系を $\mathtt{CLKID}^{\omega}$ と書く。$\omega$ は証明そのものが有限グラフでないという意味ではなく、そのグラフを展開して得る導出木が無限になりうることを表す。
一階言語 $\Sigma$ の述語記号のうち有限個 $P_1,\dots,P_n$ を帰納的述語として指定する。帰納的定義集合 $\Phi$ は、次の形の有限個の生成規則からなる。
$$
\frac{Q_1\mathbf u_1(\mathbf x),\dots,Q_h\mathbf u_h(\mathbf x),
P_{j_1}\mathbf t_1(\mathbf x),\dots,P_{j_m}\mathbf t_m(\mathbf x)}
{P_i\mathbf t(\mathbf x)}.
$$
ここで $Q_1,\dots,Q_h$ は通常の述語、$P_{j_1},\dots,P_{j_m},P_i$ は帰納的述語で、各項ベクトルの長さは対応する述語の項数に一致する。標準意味論では $P_1,\dots,P_n$ を、$\Phi$ が定める単調作用素の最小前固定点として解釈する。
生成規則には、結論の帰納的原子を右辺へ導入する規則が対応する。また $\mathtt{LKID}^{\omega}$ では、帰納的原子を左辺で展開するために次の case 規則を用いる。結論が $\Gamma,P_i\mathbf u\vdash\Delta$ のとき、結論が $P_i\mathbf t(\mathbf x)$ である各生成規則について
$$
\Gamma,\mathbf u=\mathbf t(\mathbf y),
Q_1\mathbf u_1(\mathbf y),\dots,Q_h\mathbf u_h(\mathbf y),
P_{j_1}\mathbf t_1(\mathbf y),\dots,P_{j_m}\mathbf t_m(\mathbf y)
\vdash\Delta
$$
を前提に取る。$\mathbf y$ は結論に現れない相異なる新変数のベクトルである。この前提に現れる $P_{j_r}\mathbf t_r(\mathbf y)$ を、主論理式 $P_i\mathbf u$ のcase 子孫という。通常の論理規則、構造規則、等号規則、代入規則も併用する（BS11 §§2, 5）。
シークエント $\Gamma\vdash\Delta$ の $\mathtt{LKID}^{\omega}$ 前証明とは、$\mathtt{LKID}^{\omega}$ の推論規則で作られた、根が $\Gamma\vdash\Delta$ で、bud をもたない有限または無限の導出木である。ここで bud とは、零前提規則の結論ではないのに、それ以上前提へ展開されていない節点をいう。
前証明であるだけでは証明にならない。例えば同じシークエントへ無意味な構造規則や cut を無限に適用しても前証明は作れるが、それは妥当性を保証しない。無限降下を本当に表していることを、次の trace で検査する。
導出木の道
$$S_0,S_1,S_2,\dots,\qquad S_i=(\Gamma_i\vdash\Delta_i)$$
に沿う trace とは、各 $i$ で $\Gamma_i$ に属する帰納的原子 $\tau_i$ を選んだ列で、推論規則を横切るとき次を満たすものである。
- 代入規則では、$\tau_i$ と $\tau_{i+1}$ はその代入を介して対応する。
- 等号左規則では、$\tau_i$ と $\tau_{i+1}$ は同じ式の等号による置換前後である。
- case 規則では、$\tau_i$ が主論理式で $\tau_{i+1}$ がその case 子孫であるか、同一の帰納的原子がそのまま引き継がれる。前者の添字 $i$ を progress 点という。
- その他の規則では同じ帰納的原子を追跡する。
progress 点を無限個もつ trace を無限に進行する traceという。
$\mathtt{LKID}^{\omega}$ 前証明が 大域 trace 条件を満たすとは、導出木の任意の無限道に対し、その道のある末尾に沿う無限に進行する trace が存在することをいう。この条件を満たす前証明を $\mathtt{LKID}^{\omega}$ 証明という。
シークエント $S$ の $\mathtt{CLKID}^{\omega}$ 循環前証明とは、次の組 $(\mathcal D,R)$ である。
- $\mathcal D$ は根が $S$ である有限の $\mathtt{LKID}^{\omega}$ 導出木である。
- $R$ は $\mathcal D$ の各 bud $B$ に、$B$ と同じシークエントで標識された非 bud 節点 $R(B)$ を割り当てる。$R(B)$ を $B$ の companion という。
各 bud を companion へ戻す辺で結んだ有限有向グラフを証明グラフという。証明グラフを繰り返し展開して得られる無限導出木が大域 trace 条件を満たすとき、$(\mathcal D,R)$ を $\mathtt{CLKID}^{\omega}$ 循環証明という。
直感
通常の帰納法では、最初に帰納法の不変量や帰納法仮定を一つの論理式として選ぶ。循環証明では、証明探索が以前と同じシークエントへ戻ったとき、そこを companion へ結んで有限グラフにする。見かけ上は結論を自分自身の証明に使うため、そのままでは循環論法である。
大域 trace 条件は、この循環を無限降下へ変える。無限に同じループを回るどの道でも、ある帰納的原子を case 規則で真の子孫へ無限回移さなければならない。標準意味論では帰納的述語の成員には最小前固定点の近似段階による順序数階数を割り当てられ、progress 点ではその階数が真に下がる。順序数に無限降下列はないため、反例を保ったまま無限に道を進むことはできない。これが健全性証明の核である（BS11 Lemma 5.7, Proposition 5.8）。
重要なのは、単に「グラフに閉路がある」ことではなく、すべての無限道に対して進行する trace があることである。一つの良い閉路があっても、別の閉路が帰納的原子を一度も展開しないなら証明全体は失格になる。
例
定数 $0$、単項関数 $s$、単項帰納的述語 $N$ をもち、
$$\frac{}{N0},\qquad\frac{Nx}{N(sx)}$$
を生成規則とする。標準意味論で $N$ は $0,s0,s^20,\dots$ からなる最小集合である。$N(t)$ に case 規則を施すと、$t=0$ の場合と、新変数 $x$ に対する $t=sx,Nx$ の場合に分かれる。後者で $Nx$ は $N(t)$ の case 子孫なので、trace を $N(t)$ から $Nx$ へ移す箇所が progress 点になる。
帰納的述語 $E,O$ を
$$\frac{}{E0},\qquad\frac{Ox}{E(sx)},\qquad\frac{Ex}{O(sx)}$$
で定めると、$E$ と $O$ の case 展開は互いを呼び出す。有限導出木の bud を同じシークエントの companion へ戻して $E$ と $O$ の間を巡回させても、各周回で追跡中の原子が case 子孫へ移れば大域 trace 条件を満たしうる。BS11 Figure 4 は、この仕組みにより $Ex\lor Ox\vdash Nx$ を示す具体的な循環証明を与える。
ある bud を同じシークエントの companion へ結んで有限グラフを作っても、その閉路上で追跡する帰納的原子が一度も case 子孫へ移らないなら、対応する無限道に progress 点はない。したがってそのグラフは循環前証明ではあっても循環証明ではない。これは
$$\text{有限な循環導出グラフ}\Longrightarrow\text{健全な証明}$$
という誤った含意を破る。大域 trace 条件は付加的な装飾ではなく、循環論法を排除する本体である。
性質
$\mathtt{CLKID}^{\omega}$ 循環前証明を展開して得られる $\mathtt{LKID}^{\omega}$ 前証明は正則、すなわち相異なる部分木を有限個しかもたない。逆に、正則な $\mathtt{LKID}^{\omega}$ 前証明は有限グラフとして表現できる。
有限証明グラフの節点は有限個である。展開木の任意の節点以下の部分木は、その節点が証明グラフのどの節点から来たかだけで決まる。したがって部分木の同型型は証明グラフの節点数以下しかなく、展開木は正則である。
逆に正則な導出木 $T$ を取る。$T$ に現れる部分木を根付き標識木としての同型で分類すると、同型類は有限個である。各同型類から代表の根を一つ選び、根の直下の推論規則に対応する有限個の辺を残す。同じ同型類が再び現れた箇所を bud とし、選んだ代表根を companion に指定すれば有限グラフを得る。このグラフの展開は $T$ と同型である。$\square$
すべての $\mathtt{CLKID}^{\omega}$ 循環証明は、展開により同じ根シークエントの $\mathtt{LKID}^{\omega}$ 証明を与える。
循環前証明を展開すると、各 bud は companion を根とする導出の新しいコピーで置き換わる。この操作を無限に繰り返すと bud のない $\mathtt{LKID}^{\omega}$ 前証明が得られる。循環証明の定義は、この展開木が大域 trace 条件を満たすことにほかならない。したがって展開木は $\mathtt{LKID}^{\omega}$ 証明である。$\square$
$\mathtt{CLKID}^{\omega}$ で証明可能なシークエントは、帰納的述語を生成規則の最小前固定点として解釈する FOLID のすべての標準モデルで妥当である。
BS11 Proposition 5.8 は $\mathtt{LKID}^{\omega}$ の健全性を標準モデルについて証明する。prop-cyclic-proof-embedding により循環証明はその特殊な正則証明なので、同じ健全性が従う。これは任意の Henkin モデルに対する健全性の主張ではない。証明では、反例を保つ無限道に沿って trace の近似段階が非増加となり、progress 点で真に減少することと、順序数の整礎性を用いる（BS11 Lemma 5.7）。
BS11 Theorem 5.9 によれば、$\mathtt{LKID}^{\omega}$ は標準意味論について cut なしで完全であり、したがって同体系では cut が除去可能である。一方、正則証明だけに制限した $\mathtt{CLKID}^{\omega}$ にこの完全性を移してはならない。$\mathtt{CLKID}^{\omega}$ は $\mathtt{LKID}^{\omega}$ の正則証明からなる、有限表現可能な部分体系である。
有限な循環前証明が大域 trace 条件を満たすかどうかは判定可能である。
BS11 Proposition 7.4 は、有限証明グラフ上の道と無限に進行する trace を Büchi オートマトンで表し、補集合・共通部分・空性判定へ帰着する。ここで判定可能なのは、与えられた有限前証明が証明であるかであって、任意の妥当なシークエントに循環証明が存在するかではない。
同じ帰納的定義系に対し、明示的帰納法の体系 $\mathtt{LKID}$ で証明可能なら $\mathtt{CLKID}^{\omega}$ でも証明可能である（BS11 Theorem 7.6）。逆は一般には成り立たない。Berardi–Tatsuta は 2-Hydra 文が $\mathtt{CLKID}^{\omega}$ では証明可能だが、対応する $\mathtt{LKID}$ では証明不可能である例を構成した（BT19 Theorem 15）。したがって一般の FOLID では
$$\operatorname{Thm}(\mathtt{LKID})\subsetneq\operatorname{Thm}(\mathtt{CLKID}^{\omega})$$
である。
関連項目
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
