不完全性定理どんな形式体系も自らが
矛盾していないことは示せないゲーデルの第二不完全性定理

ある程度の算術が行える無矛盾な形式体系は、
自らの無矛盾性を証明できない。

ゲーデルはこの定理について概要を述べただけで、詳しい証明を与えるはずだった続編を発表しなかった。その後（1939年）、ヒルベルトとベルナイスが最初の厳密な証明を与えた。証明の大筋は第一定理の形式化になるが、第二定理が成り立つ体系の条件は第一定理のそれよりも強く、和積演算が正しく行えるだけでなく、数学的帰納法が必要条件となる。以下では、無矛盾【無矛盾】ある命題とその否定が同時に導出されることを矛盾といい、矛盾が導かれないことを無矛盾という。矛盾する体系からは任意の命題が証明でき、証明できない命題がある体系は無矛盾である。また、「体系Tで命題Aが証明できる」と、「T+￢Aが矛盾する」とは同値である。 な形式体系として１階論理上のペアノ算術PAを選んでおくが、公理系の詳細は重要でないので省略する。いま、「命題AがPAで証明可能である」を □Aで表すと、ゲーデル文GはPA上でG↔︎¬□Gを満たす。また、「PAが無矛盾である」は¬□(0=1)で表せ、これをCon(PA)とおく。すると、第一不完全性定理の【補足説明】【補足説明】ゲーデルの不完全性定理の原論文においては、形式体系に対する仮定は「健全性」より少し弱い「ω無矛盾性」という条件で、体系がω無矛盾であるとは「どの論理式A(x)についても、∃x A(x)が証明できれば、¬A(n*)が証明されない自然数nがある」ことをいう。ここで、n*は自然数nを形式的に表現する記号列で、例えば 3*は「1+1+1」などとする。そして、ゲーデルの結果を厳密に述べれば、（1） 無矛盾な体系では、Gは証明できない。（2） ω無矛盾な体系では、¬Gは証明できない。となる。（2）の仮定を「無矛盾」に弱めたのはロッサーの仕事（1936年）である。 で述べた、定理の前半（1）はCon(PA)→¬□Gと形式的に表せる。¬□GはGに等しいから、Con(PA)→Gでもある。問題はこれをPAの中で証明することであり、その概要^※は下記で示す。さて、Con(PA)→Gが言えたとして、さらにCon(PA)が証明できるなら、論理規則によってGも証明できるので、第一定理の結論に反する。よって、Con(PA)は証明できないことになる。

※ 第一不完全性定理の証明をそのまま PA内で形式的に展開しようとした場合、難所は、Σ₁完全性（第一不完全性定理の＜さらに知りたい方へ＞を参照）の形式化、つまり任意のΣ₁文∃𝑥 A(𝑥)に対して、∃𝑥 A(𝑥)→□∃𝑥 A(𝑥)を示すことである。標準モデルの上では、任意の自然数kに対して、A(k) → □A(k*)がいえるが、形式的議論では ∀𝑥 (A(𝑥) → □A(𝑥*))をPAで証明する必要があり、ここに帰納法が必要である。これがヒルベルトとベルナイスの証明の要だが、これ以上の議論は、形式体系の詳細な定義が必要となるので、ここでは省略する。その代わりに、算術化された完全性定理を用いたCon(PA)→G の証明について述べる。
PA＋Con(PA)のモデルMを任意に固定し、そこでＧが成り立つことをいえばよい。まず、Ｇ, つまり¬□G はCon(PA+¬G)と同値であることに注意する。MはCon(PA)を満たすので、Mの拡大となる超準モデルM′が作れる。M′が¬Gを満たせば、M′ はPA+¬Gのモデルなので、MでCon(PA+¬G)がいえる。M′がGを満たせば、GはΠ₁文で、Mに関する∀量化はM′の領域の一部を変域にするだけだから、Gは Mでも成り立つ。よって、PAでCon(PA)→G がいえる。

問1 「自らが証明できる」という意味のヘンキン文Hは（PAで）証明できることを示せ。

PAにおいてH↔□H となるヘンキン文 Hを考える。第二不完全性定理の対偶から、PA + ¬H がCon(PA + ¬H)を導くなら、PA + ¬H は矛盾する。いま、Con(PA + ¬H)は¬□Hと同値であり、Hの定義からそれは ¬Hとも同値になる。すると、PA + ¬Hが¬Hを導くのは明らかだから、PA + ¬H は矛盾しており、よってPAでHが証明できる。

問2 自らの矛盾性 ¬Con(T)を証明する無矛盾な理論Tがあることを示せ。

T = PA + ¬Con(PA) とおくと，PA から Con(PA)が証明されないので、Tは無矛盾である。他方、Tは ¬Con(PA)を証明し、PA ⊂ T だから Tは ¬Con(T)も証明する。