循環証明体系(帰納的定義付き一階述語論理)
概要
循環証明体系(帰納的定義付き一階述語論理)（cyclic proof system for first-order logic with inductive definitions）とは、有限導出木の未閉鎖葉を同じシークエントの節点へ戻し、有限グラフで証明を表す体系である。帰納的定義付き一階述語論理の $\mathtt{CLKID}^{\omega}$ では、展開した導出木の任意の無限道に、case子孫への移行を無限回行うtraceを要求する。この条件が順序数の無限降下を排除して標準意味論での健全性を保証する。有限前証明の条件検査は判定可能である。
定義
本記事では 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$ を示す具体的な循環証明を与える。
例えば、通常の単項述語 $P,Q$ に対するシークエント $P(x)\vdash Q(x)$ を根とし、恒等代入規則の前提として同じシークエントの bud を置き、その bud を根へ戻す。これは有限の循環前証明である。展開した無限道では左辺に帰納的原子が一つもないので、どの末尾にも trace が存在せず、大域 trace 条件を満たさない。さらに、一元の標準モデルで $P$ を全域、$Q$ を空集合と解釈すると根シークエントは偽である。これは
$$\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 8.3）。したがって一般の FOLID では
$$\operatorname{Thm}(\mathtt{LKID})\subsetneq\operatorname{Thm}(\mathtt{CLKID}^{\omega})$$
である。
trace 条件の量化順序
大域 trace 条件には三つの選択がある。まず無限道を任意に取り、その道の有限な先頭部分を捨て、その後に進行を無限回行う trace を選ぶ。論理的な順序は
$$
\forall\text{ 無限道 }\pi\;\exists\text{ 末尾の開始点 }k\;
\exists\text{ trace }\tau\;\forall m\;\exists i\ge m\;
(i\text{ は progress 点})
$$
である。道ごとに trace の開始点や追う原子が異なっていてよい。最初からすべての道に共通する一つの原子を追わなければならないという条件ではない。一方、一つだけ良い無限道を見つけても、すべての道についての条件は得られない。
case 規則に出会った回数と、trace が進行した回数も区別される。case 規則の主論理式とは別の帰納的原子を追って、そのまま引き継ぐ場合は progress 点ではない。ある道で case 規則が無限回使われても、同じ trace がその主論理式から子孫へ無限回移ることを示す必要がある。意味論で階数を真に下げるのは、追跡中の原子についてのこの移行だからである。
順序数列 $(\alpha_i)_{i\ge k}$ がすべての $i$ で $\alpha_{i+1}\le\alpha_i$ を満たすとする。真に減少する添字が無限個あることはない。
値の集合 $\{\alpha_i\mid i\ge k\}$ は空でない順序数の集合なので最小元 $\beta$ をもつ。ある $j\ge k$ に対し $\alpha_j=\beta$ となる。非増加性から $i\ge j$ では $\alpha_i\le\beta$ であるが、$\beta$ の最小性から $\beta\le\alpha_i$ でもある。従って $i\ge j$ のすべての値は $\beta$ に等しい。真に減少する添字は $j$ より前の有限個に限られる。$\square$
健全性では、反例を保つ道を先に作り、その道に大域 trace 条件を適用する。BS11 Lemma 5.7 が、追跡中の原子の最小近似段階を順序数列として与える。すべての推論段で非増加となり、progress 点では真に減少する。前の命題によりそのような progress 点は有限個しかありえない。しかし大域条件は無限個を要求するので矛盾する。有限グラフの形だけから健全性が出るのでなく、局所的な推論規則、反例を保つ道、近似段階、無限道を覆う trace 条件を順に組み合わせている。
相互帰納的な述語を追う
偶数述語 $E$ と奇数述語 $O$ の例では、同じ述語名をずっと追うとは限らない。$E(sx)$ の case 展開で $O(x)$ を選び、次に $O(sy)$ の展開で $E(y)$ を選べる。二つの述語を相互に移っても、どちらも生成規則の帰納的前提から来る case 子孫なので、各移行は progress 点になる。
BS11 Figure 4 の循環では、$Ex\vdash Nx$ と $Ox\vdash Nx$ が互いを呼び出す。$E$ の零の場合は $E0$ から $N0$ へ進む有限の枝で閉じる。後続者の場合は $x=sy,Oy$ を得て、$Oy\vdash Ny$ の側へ移り、$Ny$ から $N(sy)$ を導く。$O$ の側では $Ey$ の case 子孫へ移る。この往復を展開した無限道では、$E,O,E,O,\ldots$ と交互に追跡しつつ progress が繰り返される。述語の名前が変わっても、相互帰納的な定義を同じ単調作用素の成分として扱うことによって階数の減少を比較できる。
有限表現と証明探索の違い
有限前証明が与えられた後の検査では、グラフの道を受理するオートマトンと、末尾に進行する trace が存在する道を受理するオートマトンを比較する。後者に受理されない無限道が前者には存在するかを調べ、そのような道がなければ大域条件を満たす。この順序では、既に与えられた節点、推論規則、bud と companion の対応が有限データであることを使う（BS11 Proposition 7.4）。
一方、あるシークエントから有限循環証明を探す場合、どれだけ大きいグラフまで探索すればよいかはこの判定結果からは得られない。また、無限体系の完全性により無限証明が存在しても、その証明が正則とは限らない。相異なる部分木が無限に現れる導出木は、有限な companion の表だけでは表せない。この点が、無限証明の存在、有限表現の存在、既存の有限表現の検査という三つの問題を分ける。
Berardi–Tatsuta の反例は、この区別を意味論からも示している。2-Hydra 文は標準モデルでは成立するが、適切な Henkin モデルでは成立しない。明示的帰納法の体系は Henkin モデルについて健全なので、その体系では当該文を証明できない。他方、循環体系には具体的な有限循環証明がある（BT19 Theorem 4.7, Theorem 8.3）。ここで帰納法の体系に別の帰納的述語や追加の公理を加えれば、証明可能性が変わりうる。従って比較の際には、同じ言語と同じ帰納的定義系を固定することが必要である。
反例の条件と結論
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| 大域 trace 条件（有限循環前証明であることは保つ） | 通常の $P,Q$ に対する $P(x)\vdash Q(x)$ の恒等代入ループ（rem-cyclic-proof-bad-loop）。 | 標準意味論での妥当性。一元モデルで $P$ を全域、$Q$ を空集合とすると根は偽である。 |
関連項目
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
