証明論的順序数

証明論的順序数 (proof-theoretic ordinal) は，順序数解析 (ordinal analysis) において使われる概念で，十分に強い算術を含む理論に対して，理論の強さを測るために割り当てられる不変量としての順序数である．証明論的順序数の定義は，さまざまな種類があるが，一番標準的なものは，整列性が証明可能な計算可能全順序の順序型として定義される．この記事では証明論的順序数及び順序数解析全般について解説する．

歴史[]

証明論の創始[]

証明論 (proof theory) の歴史は 無矛盾性証明 (consistency proof) の歴史と密接に関係する。特に実数論に対する無矛盾性証明はダフィット・ヒルベルトのヒルベルトの23の問題として1900年の国際数学者会議によって第2問題として発表された．この次の1904年の国際数学者会議，ハイデルベルグに於いてヒルベルトは「数学に於ける証明は単なる記号列の書き換えである」という考えかたの兆しが与えられヒルベルトによって証明に関する構造帰納法による無矛盾性証明のアプローチが展開された^[1]．

ヒルベルトは1904年の思想を後に徹底させ，1920年代には形式化された証明を数学的対象として研究するという証明論 (独:beweistheorie) という言葉がゲッティンゲンのヒルベルトによる数理論理学の講義にて用いられたという^[1]^[2]．ヒルベルトは無矛盾性が信頼できる有限の立場 (finite standpoint) というメタ理論から形式化された数学の無矛盾性を示そうという試み，ヒルベルト計画 (Hilbert's program) を考えたが，有限の立場が何を意味するのかは当時相当ぶれがあった^[3]．厳密に有限の立場が形式化されたのはスコーレム^[4]の原始再帰算術 (primitive recursive arithmetic) であり^[5]，このようなことからヒルベルト計画の全貌が明らかになったのはヒルベルト・ベルナイスによる『数学の基礎^[6]』以降である^[1]．

順序数解析の創始[]

証明論的順序数のアイデアの萌芽はゲルハルト・ゲンツェンによるペアノ算術の無矛盾性証明にて，ε₀までの超限帰納法が用いられた^{[注 1]}ことによる^[8]^[9]．そしてゲンツェンは就職論文^[10]にてそのアイデアを精緻化し，現代的に言えば，ペアノ算術の証明論的順序数を求めたとよって良いだろう．しかし，ゲンツェンによって求められた証明論的順序数は現代的なものとは異なることに留意されたい．

現代的な定義がいつから用いられたのかは良く分からない．同時代の教科書や，また現代的な教科書でさえ，証明論的順序数の定義が異なり，また標準的な定義と同値でないものが存在する．しかし後述するナイーブな証明論的順序数が良く振る舞わないことを表す結果によって，そのことについて意識が向けられてきたと推測される．

定義[]

証明論的順序数の定義は算術と集合論では異なるため分けて紹介する．どちらにせよ理論\(T\)に対し証明論的順序数を\(\|T\|\)と表す．

算術[]

理論\(T\)を一階，あるいは二階の算術の言語上の初等関数算術\(\mathsf{EFA}\)を含む必ずしも計算可能とは限らない（すなわち公理のゲーデル数全体の集合が\(\mathbb{N}\)の再帰的部分集合とは限らない）理論とする．しかし一階述語論理，二階述語論理によらず言語には二階の集合変数\(X\)が含まれていると仮定する．これは一変数述語記号と考えても問題ない．以下，整列順序\(\prec\)に対し，\(\mathrm{otyp}(\prec)\)で\(\prec\)の順序型，すなわち\(\prec\)と同型になる最小の順序数を表し，論理式\(\varphi\)に対し\(T\vdash\varphi\)で\(T\)から\(\varphi\)が証明可能であることを表すとする．全域とは限らない計算可能関数\(\mathbb{N}^2 \to \{0,1\}\)全体の集合を\(R\)と置き，

\(\begin{align*}\|T\|:=\sup\{\mathrm{otyp}(\prec)\mid \prec \in R \land T\vdash\mathsf{WO}(\prec)\}\end{align*}\)

と定める．ここで

\(\mathsf{WO}(\prec)\)は \(\begin{align*}&(\forall x)[\lnot x\prec x]\land\\ &(\forall x)(\forall y)[x\prec y\lor x=y\lor y\prec x]\land\\ &(\forall x)(\forall y)(\forall z)[x\prec y\land y\prec z\to x\prec z]\land\\ &(\forall x)[(\forall y\prec x)[y\in X]\to x\in X]\to(\forall x)[x\in X]\end{align*}\)

の省略とする．これは\(\prec\)が整列順序であることを表している．\(\prec\)自体は\(T\)の述語ではないので\(\prec\)を含む論理式\(\mathsf{WO}(\prec)\)の\(T\)における証明可能性は一見定義されないように見えるが，\(T\vdash\mathsf{WO}(\prec)\)はより正確には「コード\(e\)の定めるチューリングマシンが計算する全域とは限らない計算可能関数\(\prec_e \colon \mathbb{N}^2 \to \{0,1\}\)が\(\prec\)と一致する」および「『コード\(e\)の定めるチューリングマシンが計算する全域とは限らない計算可能関数\(\prec_e \colon \mathbb{N}^2 \to \{0,1\}\)が\(\mathsf{WO}(\prec_e)\)を満たし，\(\prec_e\)の定義域が計算可能である』という算術文が\(T\)で証明可能である」という３条件を満たす自然数\(e\)が存在する，という論理式である．言語に二階の集合変数\(X\)が含まれていない一階算術\(T\)に対しては，人工的な方法で言語に二階の集合変数\(X\)が含まれる理論\(T'\)に拡大し，\(\|T\| := \|T'\|\)と定める．例えばペアノ算術であれば，\(\varphi(u)\)で添字付けられた公理図式である数学的帰納法\(\varphi(\underline{0})\land(\forall x)(\varphi(x) \to \varphi(S(x)))) \to \forall x\varphi(x)\)の\(\varphi\)が\(X\)が含む言語に拡大すればよい．

集合論[]

十分に強い集合論の理論\(T\)に対し，

\(\begin{align*}\|T\|:=\sup\{\mathrm{otyp}(\prec)\mid\prec\subseteq\mathbb{N}^2\land\prec\in\Delta_0\land T\vdash\mathsf{WO}'(\prec)\}\end{align*}\)

とする．ここで\(\Delta_0\)は非有界な量化を含まない，すなわち\(\Delta_0\)-論理式で定義可能な集合全体である．また\(\mathsf{WO}'(\prec)\)は

\(\begin{align*}&(\forall x)[\lnot x\prec x]\land\\ &(\forall x)(\forall y)[x\prec y\lor x=y\lor y\prec x]\land\\ &(\forall x)(\forall y)(\forall z)[x\prec y\land y\prec z\to x\prec z]\land\\ &(\forall X\subseteq \mathbb{N})[(\forall x)[(\forall y\prec x)[y\in X]\to x\in X]\to(\forall x)[x\in X]]\end{align*}\)

である．この定義は\(\mathbb{N}\)が定義できないような集合論，例えば\(\mathsf{ZF}-(\mathsf{Inf})\)などには定義されないことに気をつけるべきである．

また集合論に順序数解析では\(\Sigma_1^{L_{\omega_1^\mathrm{CK}}}\)-順序数 (\(\Sigma_1^{L_{\omega_1^\mathrm{CK}}}\)-ordinal) や\(\Sigma_1\)-順序数 (\(\Sigma_1\)-ordinal) という指標が考えられることが多い．理論\(T\)，論理式の集合\(\Gamma\)に対して\(\Gamma\)-順序数 (\(\Gamma\)-ordinal) ，\(\|T\|_\Gamma\)は以下のように定義される．

\(\begin{align*}\|T\|_\Gamma:=\min\{\xi\mid \varphi\in\Gamma\land T\vdash\varphi\implies L_\xi\models\varphi\}\end{align*}\)

とする．ここで\(L_\xi\)は構成可能階層である．この順序数が定義されるとき\(\|T\|\leq \|T\|_{\Sigma_1^{L_{\omega_1^\mathrm{CK}}}}\leq \|T\|_{\Sigma_1}\)であり，特に\(T\)が\(\omega_1^\mathrm{CK}\)の存在を示せるとき，\(\|T\|=\|T\|_{\Sigma_1^{L_{\omega_1^\mathrm{CK}}}}\)である．

ナイーブな定義[]

言語に二階の集合変数\(X\)が含まれていない一階算術\(T\)の証明論的順序数を，人工的な方法で言語に二階の集合変数\(X\)が含まれる理論\(T'\)に拡大するのではなくナイーブに\(T\)のままの証明能力や無矛盾性を用いて定義してしまうと望ましい性質が得られないことがKreiselの反例によって示されている^[11]^[12]．

基本的な性質[]

木に関する基本的な事実[]

定義3.1.1
自然数の有限列の集合を\(\mathbb{N}^{<\omega}\)と表す．有限列に対していくつか定義を行う． \(s,t\in \mathbb{N}^{<\omega}\)に対し\(s\subseteq t\)で\(s\)は\(t\)の始切片であることを表す^{[注 2]}． \(s,t\in \mathbb{N}^{<\omega}\)に対し\(s^\frown t\)で\(s\)と\(t\)の連結 (concatenation) を表す．すなわち\(s=\langle s_0,\ldots,s_n\rangle,t=\langle t_0,\ldots,t_m\rangle\)とすれば\(s^\frown t=\langle s_0,\ldots,s_n,t_0,\ldots,t_m\rangle\)である． \(s\in\mathbb{N}^{<\omega}\)に対し\(\mathrm{lh}(s)\)で\(s\)の列としての長さを返す．すなわち\(s=\langle s_0,\ldots,s_n\rangle\)とすれば\(\mathrm{lh}(s)=n+1\)である． \(s\in\mathbb{N}^{<\omega}\)に対し\(k<\mathrm{lh}(s)\)に対し\((s)_k\)で\(s\)の\(0\)から数えて\(k\)番目の要素を表す．すなわち\(s=\langle s_0,\ldots,s_n\rangle\)とすれば\((s)_k=s_k\)である． \(\mathbb{N}^{<\omega}\)の空でない部分集合\(T\)が木 (tree) であるとは，始切片を取る操作に閉じていることを言う．つまり\(\langle s_0,\ldots,s_n\rangle\in T\)なら任意の\(k<n\)対して\(\langle s_0,\ldots,s_k\rangle\in T\)である．また一般に半順序集合\(\langle A,\leq_A\rangle\)が最小元を持ち，かつ任意の\(a\in A\)に対し\(\{x\in A\mid x\leq_A a\}\)が\(\leq_A\)で全順序付けられるとき，木であるという．数学の慣習に則り，誤解を招かない際，木\(\langle A,\leq_A\rangle\)とその台集合\(A\)を同一視する．前者の木\(T\subseteq\mathbb{N}^{<\omega}\)は\(\langle T,\subseteq\rangle\)と見たとき後者の意味で木になる．木に関していくつか定義を行う．木に存在する最小元のことを根 (root) という．特に\(T\subseteq\mathbb{N}^{<\omega}\)の根は空列\(\langle\rangle\)である．木の元を節 (node) という．木\(T\)において節\(s\)が自身より大きい節が存在しないとき葉 (leaf) であるという．木\(T\)の部分集合\(S\)が\(\leq_T\)で全順序で\((\forall s\in S)(\forall t\in T)[t\leq_T s\to t\in S]\)であるとき枝 (branch)であるという．木\(T\subseteq\mathbb{N}^{<\omega}\)の無限枝\(S\)を\(S=\{\langle\rangle\}\cup\{\langle f(0),\ldots,f(m-1)\rangle\mid m\in\mathbb{N}\}\)を満たす関数\(f:\mathbb{N}\to\mathbb{N}\)と同一視する．木\(T\)の任意の節\(s\)に対して\(s\)の後者がたかだか\(n\)個であるとき\(n\)-分岐 (\(n\)-branching) であるといい，たかだか有限であるとき有限分岐 (finitely branching) であるという．木が有限であるとは台集合が有限であることである．木\(T\subseteq\mathbb{N}^{<\omega}\)，節\(s\in T\)に対し\(T_s:=\{t\mid s^\frown t\in T\}\)を\(s\)上の\(T\)の部分木 (subtree) という．木\(T\)が無限枝を持たないとき，整礎であるという．整礎木に対する整礎帰納法をバー帰納法 (bar induction) といい，再帰的定義をバー再帰 (bar recursion) という．整礎木\(T\subseteq \mathbb{N}^{<\omega}\)に対しバー再帰で\(\mathrm{otyp}_T(s):=\sup\{\mathrm{otyp}_T(s^\frown\langle x\rangle)+1\mid s^\frown\langle x\rangle\}\)とし，\(\mathrm{otyp}(T):=\mathrm{otyp}_T(\langle\rangle)\)とする．ここで\(\mathrm{otyp}(T)\)を木\(T\)の順序型という． \(T\subseteq\mathbb{N}^{<\omega}\)に対してクリーネ・ブラウワー・ルジン・シェルピンスキー順序 (Kleene–Brouwer–Lusin–Sierpiński) ^{[注 3]}\(<_T^\mathrm{KB}\)は以下のように定義される．\(s<_T^\mathrm{KB} t:\Leftrightarrow s\in T\land t\in T\land(t\subsetneq s\lor(\exists b)[b\subseteq s\land b\subseteq t\land (s)_{\mathrm{lh}(b)}<(t)_{\mathrm{lh}(b)}]).\) 木\(T,S\subseteq\mathbb{N}^{<\omega},t=\langle t_0,\ldots,t_n\rangle\in T,s=\langle s_0,\ldots, s_n\rangle\)とする．\(t\otimes s:=\langle\langle t_0,s_0\rangle.\ldots,\langle t_n,s_n\rangle\rangle\)とし，また\(\langle\rangle\otimes\langle\rangle=\langle\rangle\)とする．\(T\otimes S:=\{t\otimes s\mid t\in T\land s\in T\land\mathrm{lh}(t)=\mathrm{lh}(s)\}\)とする．\(T\otimes S\)は始切片であることを順序として木である．

補題3.1.2 ^[16]
\(T\subseteq\mathbb{N}^{<\omega}\)を整礎でない木\(S\subseteq\mathbb{N}^{<\omega}\)を整礎な木とする．このとき\(T\otimes S\)は整礎で，\(\mathrm{otyp}(T\otimes S)\geq\mathrm{otyp}(S)\)である．証明．　\(T\otimes S\)が整礎なのは\(S\)が整礎だから，\(\otimes\)の定義より明らかである．よって\(\mathrm{otyp}(T\otimes S)\geq\mathrm{otyp}(S)\)であることを示そう．\(T\)は整礎でないことから無限枝\(\{t_i\}_{i\in\omega}\)を取る．\(t'_n:=\langle t_0,\ldots,t_{n-1}\rangle\)とし\(s=\langle s_0,\ldots,s_{n-1}\rangle\in S\)に対する帰納法で\(\mathrm{otyp}_{T\otimes S}(t'_n\otimes s)\geq \mathrm{otyp}_S(s)\)が成り立つことを確かめる．帰納法の仮定から任意の\(s^\frown\langle i\rangle\in S\)を満たす\(i\in\mathbb{N}\)に対し\(\mathrm{otyp}_{T\otimes S}(t'_{n+1}\otimes s^\frown\langle i\rangle)\geq \mathrm{otyp}_S(s^\frown\langle i\rangle)\)であり，よって\(\mathrm{otyp}\)の定義から成り立つことが分かる．□

定理3.1.3（ケーニヒの無限補題，Kőnig's Infinite Lemma）^[17]^[18]^[19]^[20]
\(\mathsf{RCA}_0\)上で以下は同値である．ケーニヒの無限補題，任意の有限分岐な無限木\(T\subseteq\mathbb{N}^{<\omega}\)は無限枝を持つ，あるいは\(T\)は\(\aleph_0\)-アロンシャイン木ではない． \((\mathsf{ACA})\)．証明．　2.から1.が導かれることのみを示す．逆は^[20]などで示されている．以下非形式的に議論する．まず\(T\subseteq \mathbb{N}^{<\omega}\)を無限有限分岐木であるとする．今\((\mathsf{ACA})\)を用いて\(T^\infty\subseteq T\)を，\(s\in T\)で\(\{t\in T\mid s\subseteq t\}\)であるようなもの全体とする． \(T\)が有限分岐であるから，任意の\(s\in T^\infty\)に対し，ある\(i\)が存在し\(s^\frown\langle i\rangle\in T^\infty\)である．そのような\(i\)で最小なものを\(i_s\)と表す．よって原始再帰によって関数\(g:\mathbb{N}\to T^\infty\)を \(\begin{align}g(0)&=\langle\rangle\\ g(n+1)&=g(n)^\frown\langle i_{g(n)}\rangle\end{align}\) と定めればこれが求めたい\(T\)の無限枝である．□

系3.1.4^[20]
\(\mathsf{ACA}_0\)上で以下の同値性が成り立つ．木\(T\)は整礎である．木\(T\)上のクリーネ・ブラウワー・ルジン・シェルピンスキー順序\(<_T^{\mathrm{KB}}\)は整礎である．証明．非形式的に示す．もし無限枝\(\{s_n\}_{n\in\omega}\)が存在するなら\(s_{n+1}<_T^\mathrm{KB}s_n\)が\(<_T^{\mathrm{KB}}\)の定義から従う．よって対偶法により2.を仮定して1.が示せた．逆，1.ならば2.を示す．背理法で示す．今\(<_T^\mathrm{KB}\)に対する無限降下列\(\{s_n\}_{n\in\omega}\)が存在すると仮定する．\((\mathsf{ACA})\)によって集合\(S:=\{t\in T\mid (\exists n)[t\subseteq s_n]\}\)を取る． \(S\)は\(T\)の有限分岐無限部分木になることを示す．よってケーニヒの補題から\(S\)及び\(T\)は無限枝を持つ．\(s\in S\)を、ある\(i\)が存在して\(s^\frown\langle i\rangle\in S\)となるようなものとし，かつ最小のものを\(i_0\)とする．\(S\)の定義から\(s^\frown\langle i_0\rangle\subseteq s_n\)なる\(n\)を取る．\(X=\{j>i_0\mid s^\frown\langle j\rangle\in S\}\)はたかだか\(n\)個の要素しか持たないことを見る．任意の\(j\in X\)に対して\(n_j\)を\(s^\frown\langle j\rangle\subseteq s_m\)なる最小の\(m\)とする．任意の\(j,k\in X\)に対して\(j<k\)なら\(s_n<_T^\mathrm{KB} s_{n_j}<_T^\mathrm{KB} s_{n_k}\)であり，\(n_k<n_j<n\)となるからである．□

算術の理論と不完全性定理[]

定義3.4.1

再帰理論の基本的な事実[]

定理3.4.1, (\(\Pi^1_1\)-標準形定理，\(\Pi^1_1\)-Normal Form Theorem) ^[21]^[22]^[23]