このノートでは、ゲーデルの完全性定理と
不完全性定理についての解説を試みる。
この解説は、完全性定理や不完全性定理の手短な理解には、
どれだけの数学的予備知識が必要か、それを明らかにすることが目的である。
この知恵ノートを通じて、読者の予備知識としては、
一階の等号述語論理の一般論(有限の立場の考え方を含む)
を仮定するが、完全性定理の記述については、読者は、
形式的体系のモデルの定義をあらかじめ知っているとし、
不完全性定理の記述においては、読者は
ゲーデル数の定義をあらかじめ知っているとする。
これらの知識を仮定するのは、モデル、ゲーデル数の両者とも、
論理式の構成的な定義に立ち戻って定義する必要があるからである。
(等号) 述語論理, 形式的体系のモデル、ゲーデル数についての解説はこちら。
完全性定理の定式化その1
1.1 述語論理を含む形式的体系が無矛盾であれば、モデルを持つ。
1.2 等号述語論理を含む形式的体系が無矛盾であれば、正規モデルを持つ。
完全性定理の定式化その2
2.1 述語論理を含む形式的体系 T の閉論理式 A が、Tの任意のモデル
M 上で真ならば、A は T 内で証明可能である。
2.2 等号述語論理を含む形式的体系 T の閉論理式 A が、Tの任意の
正規モデル M 上で真ならば、A は T 内で証明可能である。
（完全性定理の証明は、有限の立場ではなく、超限的であることに注意しておく。）
定式化その1とその2は同値であり、1.1, 1.2, 2.1, 2.2 の超数学的命題は、
逆も成り立つ（逆はトリビアルである）。
特に、定式化その2 のほうは、命題論理に関する超数学的定理：
3.1 トートロジー（恒真式）は証明可能である。（逆も成り立つ。）
の、述語論理や等号述語論理における自然な拡張になっている。
ここで、述語論理や等号述語論理においては、トートロジーの概念の拡張として、
「任意のモデルで真」と言う概念が使われるのである。つまり、完全性定理の
「完全」とは、大雑把に言うと、述語論理や等号述語論理を念頭に置いて、
「意味論的に正しい（任意のモデルで真な）閉論理式は、全て証明可能」
と言う意味である。
なお、述語論理や等号述語論理に於いても、閉論理式 A が
「任意のモデルで真」のとき、A は恒真と呼ばれる。
また、このモデルの概念は、集合論 ZF(C) で形式的に扱われ、歴史的には、
構成可能性公理の相対無矛盾性証明（ゲーデル）
4.2 generic モデルを用いた、構成可能性公理、一般連続体仮説、
選択公理の（相対）独立性証明（コーエン）
の二つの仕事が有名である。特に、generic モデルの方法は、今日でも
盛んに扱われ、（すでに 30 年以上前だが）例えば集合論 BGE が 集合論 ZFC
の保存拡大になっていると言う超数学的定理の有限の立場による証明
（もっと精密に、「原始帰納的な」証明）にも応用されている。
又、筆者は専門外なので詳しくはないが、竹内外史先生の P=NP に関連する
著書にも、generic モデル（forcing）に関する記述があるようである。
今後この方面の発展に期待する次第である。
次に、不完全性定理の解説に移ろう。
不完全性定理には二つあり、その比較的わかり易い
定式化は、次のとおりである：
5.1 第一不完全性定理
T 内においては、論理式 A を構成して、A と ￢A の両方が、
T からは証明不可能であるようにできる。
5.2 第二不完全性定理
T については、T 内で形式化できる方法では、T の無矛盾性証明ができない。
（T の論理式 U を構成し、U の直観的な意味が自然に 「T は無矛盾である」
と言うものになり、なおかつ U は T からは証明できないようにできる。）
（これら二つの不完全性定理の証明は、有限の立場で遂行できる。）
ここで、形式的体系 T が「自然数論を定式化できる」とは、T が以下の条件
6.1～6.10を満たすこととする。
6.1 T は述語論理を含み、T のある一変数論理式 N(x) ,
変数を持たない対称式 0, 一変数対象式 S(x), 二変数対象式
x+y, x・y, 二変数論理式 x=y が T 内で構成できて、
以下の論理式 6.2～6.11 が、全て T の定理になる：
6.2 N(0)∧(∀x)(∀y((N(x)∧N(y)) ⇒ (N(S(x))∧N(x+y)∧N(x・y)))
6.3 (∀x)(∀y)(∀z)((N(x)∧N(y)∧N(z)∧x=y∧x=z) ⇒ y=z)
6.4 (∀x)(∀y)((N(x)∧N(y)∧x=y) ⇒ S(x)=S(y))
6.5 (∀x)((N(x) ⇒ S(x)≠0)
6.6 (∀x)(∀y)((N(x)∧N(y)∧S(x)=S(y)) ⇒ x=y)
6.7 (∀x)(N(x) ⇒ x+0=x)
6.8 (∀x)(∀y)((N(x)∧N(y) ⇒ x+S(y)=S(x+y))
6.9 (∀x)(N(x) ⇒ x・0=0)
6.10 (∀x)(∀y)((N(x)∧N(y)) ⇒ x・S(y)=(x・y)+x)
6.11 (R(0)∧(∀x)((N(x)∧R(x)) ⇒ R(S(x)))) ⇒ (∀x)(N(x) ⇒ R(x))
ここに、R(x) は、T 内の論理式全てをわたるものとする。
（第一不完全性定理に関しては、条件6.2～6.11をもっと緩められる。)
6.12 論理式 N(x) は、「x は自然数である」と言う意味に解釈される。
6.13 対象式 S(x) は、(x が自然数のとき) 「x の次の自然数」と言う意味
解釈される。x+y は自然数の和、x・y は自然数の積、x=y は
自然数の間の等号として、それぞれ解釈される。
次に、形式的体系 T が帰納的であるとはどういうことか、説明しよう。
そのための準備として、有限の立場での自然数を以下の 7.1～7.3 で定義する。
7.1 図形 0 は有限の立場での自然数である。
7.2 図形 n が有限の立場での自然数ならば、図形 n+1 も、
有限の立場での自然数である。
7.3 上記 7.1 と 7.2 によって定義されたもののみが、
有限の立場での自然数である。
さらに我々は、帰納的関数というものを、以下によって定義する。
8.1 有限の立場での自然数 n 個の列 (a_1, ... ,a_n) に a_i
を対応させる n 変数関数 P_{n, i} は、帰納的関数である。
8.2 有限の立場での自然数 a に a+1 を対応させる 1 変数関数は、
帰納的関数である。
8.3 有限の立場での自然数 n 個の列 (a_1, ... , a_n) に有限の立場での
自然数である定数 q を対応させる n 変数関数は、帰納的関数である。
8.4 f_1(x_1, ... ,x_n), ... , f_k(x_1, ... , x_n) が k 個の n 変数の帰納的関数で、
g(y_1, ... , y_k) が k 変数の帰納的関数ならば、合成関数
g(f_1(x_1, ... ,x_n), ... , f_k(x_1, ... , x_n)) は、帰納的関数である。
8.5 h(y, z, x_1, ... x_n ) が n+2 変数の帰納的関数で、g(x_1, ... , x_n)
が n 変数の帰納的関数ならば、次のように帰納法で定義される
n+1 変数関数 f(y, x_1, ... , x_n)は、帰納的関数である：
8.5.1 f(0, x_1, ..., x_n) = g(x_1, ... , x_n)
8.5.2 f(y+1, x_1, ..., x_n) = h(y, f(y, x_1, ..., x_n), x_1, ... x_n )
8.6 h(y, x_1, ... , x_n) が n+1 変数の帰納的関数で、次の式が有限の立場で
証明可能とする：
8.6.1 (∀x_1)....(∀x_n)(∃y)(h(y, x_1, ... , x_n)=0)
（つまり、任意に有限の立場の自然数 x_1, ... , x_n を具体的に与えると
それに応じて有限の時間内で、有限の立場の自然数 y を構成できて、
h(y, x_1, ... , x_n)が有限の時間内で計算できて、0 に等しい。）
このとき、次の関数 f(x_1, ... , x_n) は、帰納的関数である：
8.6.2 f(x_1, .. , x_n) = {h(y, x_1, ... , x_n) =0 を満たす、
最小の(有限の立場での)自然数 y}
8.7 以上によって定義された関数のみが、帰納的関数である。
そこで我々は、形式的体系 T が帰納的であるということを、
T 内における論理式 A に対するゲーデル数を G(A) として、次のように定義する：
9 0 か 1 の値を取る 1変数帰納的関数 f(x) を構成できて、
T の任意の論理式 A に対して、
9.1 A が T の公理のときは、f(G(A)) = 1 が、
9.2 A が T の公理でないときは f(G(A)) = 0 が、
有限の立場で証明できる。
（直観的には、T の任意の論理式に対し、それが T の公理かどうかが、
機械的な計算で、有限時間内に判定できる、と言う意味である。）
いくつか同値な定義があり、それら同値な定義を以って、
「計算可能関数とは、帰納的関数のことである」
と、認めることもある。（Church の提唱）
（帰納的関数についてもまた、数学では深く研究されている。）
9.3 なお、第一・第二不完全性定理の成立する形式的体系の満たすべき条件を、それぞれもっと弱めることもできる。第一不完全性定理については、ロビンソン算術など（もう少し弱い形式的体系でも良い）がその典型で、第二不完全性定理については、IΣ_1 と呼ばれる形式的体系でも良いそうである。（IΣ_1 については、筆者は検証していない。）
以上で、不完全性定理のアウトラインを述べ終わった。
10 不完全性定理の歴史的な経緯。
第一・第二不完全性定理は、それが証明された当時、
ヒルベルトが次の問題を提唱していたことに対し、
ゲーデルが与えた否定的な回答である。
（第一不完全性定理のほうには、ロッサーの貢献もある。）
10.1 数学理論(ZFC や BGE のようなものを想定している）は、無矛盾か？
もし、無矛盾とすると、その無矛盾性証明を有限の立場で
遂行することができるか？
10.2 数学理論（ZFC や BGE のようなものを想定している）は、完全か？
即ち、任意の論理式 A に対して、 A か、又は ￢A のどちらかが
必ず証明可能か？（ここでの完全性の意味は、完全性定理における
「論理の完全性」の意味とは、全く異なる。）
さらに、次の問題についても、否定的な回答が与えられている：
10.3 自然数論を定式化できる形式的体系 T が無矛盾かつ帰納的のとき、
T 内の 1変数論理式 B(x) を構成し、T の任意の論理式 A に対して
次の超数学的命題が有限の立場で証明できるか？
10.3.1
10.3.1.1 T 内で A が証明可能 ⇒ B(Z(A)) がT内で証明可能
10.3.1.2 T 内では A は証明不可能 ⇒ ￢B(Z(A)) がT内で証明可能
（つまり、T 内で形式化できる方法で、T の論理式の証明可能性を
系統的に判定できるか？（T は 自己決定可能か？））
10.3.1.3 ここに、Z は、論理式 A のゲーデル数 G(A) と
超数学的自然数 n に対し、T 内の対象式 0 に n 回
S を施したものを S^n(0) とおくと、Z(A) は記号列として
S^(G(A))0) に等しい。
10.3.2 ちなみに、ここでも、T としては、ZFC や BGE のようなものが
想定されている。
10.3.3 T が自然数論を定式化できなくても、例えば T が少なくとも一つの
2変数述語記号を持つような述語論理のときは、T の決定問題は
否定的に解かれることが知られている。
11 いくつかの無矛盾性証明（不完全性定理以後の話題）。
11.1 ゲンツェンによって、次のことが証明されている。
11.1.1 帰納法を含む自然数論（公理系 6.2～6.10 を参照のこと）は、
無矛盾である。
11.1.2 ゲンツェンの証明では、有限の立場に「近い」方法で、
ε_0 までの順序数による超限帰納法を使って、
（カット消去定理との組み合わせにより）
数学的帰納法を仔細に分析している。
11.1.3 第二不完全性定理からもわかるように、ゲンツェンによる
することはできない。
以下については、筆者は詳しくないので、大雑把に述べる。
11.2 竹内外史によって、実数論の矛盾性証明が成されている。
11.2.1 二階述語論理におけるカット消去定理がその証明の中核を成す。
その解決のために、ordinal diagrams と言うものが使われたそうである。
11.2.3 やはり、第二不完全性定理により、その証明は実数論内部
において形式化することはできない。
11.3 さらに、ゲンツェン・竹内らによる「巨大順序数の構成」を拡張し、
『順序数解析』と言う研究分野が誕生した。
この分野では新井敏康先生が多大なる貢献をされ、
2024年3月に、新井先生の退官記念公演が行われた次第である。
以上で、完全性定理・不完全性定理の解説を終わる。
参考文献として、以下の5冊を挙げておく。
第一不完全性定理の証明については、
福山克「数理論理学」（培風館）
有限の立場についてのわかりやすい説明、
自然数論の無矛盾性証明については、
第一・第二不完全性定理の証明については、
以下の文献も非常に参考になる：
前原昭二「数学基礎論入門」朝倉書店
（＊）「記号論理」は、第二不完全性定理の証明がきっちり書かれている、
数少ない本の一つである。
（＊＊）「証明論入門」が執筆された当時は、二階述語論理の
カット消去定理は、超限的な立場でしか証明されていなかった。
（＊＊＊）又、特に「ゲーデルの世界」における完全性定理と
不完全性定理の解説は、この知恵ノートよりも遥かに詳しい。
ゲーデルの原論文の和訳も掲載されているので、
興味ある方には、是非、勧めたい本である。
文責: Dr. Kazuyoshi Katogi (加藤木 一好)
