数学の基礎

　付録５で定義したHeyting算術より強い無矛盾な理論では、証明することも反証することも不可能であるような閉命題（＝変数を持たない命題）が存在する、というのが有名なGödelの不完全性定理です。
　以下で、Gödelにより初めて証明され、後にRosserにより改良されたこのメタ定理を証明します。

　まず任意に与えられた理論 T  で規定された文字、文字列、sequent、証明文といった概念を、すべて自然数（メタ言語における自然数の定義は付録１参照）によって表現する方法を考えましょう。なお、メタ言語における自然数は、太文字の 0 , 1 , 2 等を用いて表現することにします。
　理論 T  で用いる記号の全体を s₁ ,¼, s_M とし、また鎖を用いない流儀（付録１参照）を採用し、変数の全体に番号を付けて、これらを x₁ , x₂ ,¼ と表すことにします。
　ここで、各文字に対し、次の対応表によって正整数を対応させます：

文 字	s1	s2	¼	sM	xi	£j
コード	1	2	¼	M	M + 2i - 1	M + 2j

　このような対応により、理論 T  のすべての文字とすべての正整数との間に一対一の対応が付きます。そこで、以下理論 T  の各文字を、対応する正整数と同一視することにします。

　また一方で、付録５ (A5-72) の手法を用いれば、正整数からなる有限列の全体を正整数の全体と１対１に対応付けることができます。各文字を正整数と同一視する立場では、各文字列は正整数の有限列と同一視できますから、これも各正整数との間に一対一対応がつくことになります。そこで、各文字列も、それに対応する正整数と同一視することにします。
　以下同様にすれば、一般に N 階の文字列（付録１参照）の全体を正整数の全体と１対１に対応付けることができ、従って、N を指定するごとに、N 階の各文字列を、対応する正整数と同一視することができます。

　一般に超数学の議論は、理論の無矛盾性等を議論するようになると、超数学でどのような推論が許されるかということ自体が問題になることがあります。
　そこで、上記のように各 N 階の文字列をすべて正整数とみなすことによって、超数学の議論をすべて前節で導入したHeyting算術内部での推論に限定することにした立場を（狭義の）有限の立場とよぶことにします。
　前節で示したように、Heyting算術では帰納的に定義された関数はすべて扱うことができますし、更には自然数からなる有限列や、自然数の有限な範囲で定義された関数、あるいはその合成関数なども扱えるので、かなり豊富な議論を展開することができます。

　例えば、付録１で導入した A[i] や A[ j : i] や | A | や A * B や { A } などの表記は、各 N 階の文字列を正整数と同一視することにより、前節で導入した対応するHeyting算術における諸関数と同一のものとみなすことができます。
　これ以外でも、例えば付録１の (A1-2) で定義される関数 μ_A のように、定義が再帰的で複雑な形をしていて、一見Heyting算術で扱えるのか自明でない関数もありますが、その定義式 (A1-2b) に現れる pd を「定義域を 0 以上 | A | 以下の自然数の範囲に制限した関数」に置き換えることにより、付録５の (A5-87) 以下で示したような、「k における値を、k 未満の自然数における定義値をすべて用いて定義する」タイプの定義式に帰着されるので、Heyting算術の範疇（すなわち有限の立場）で扱えることがわかります。
　従って、本文第１節〜第５節の超数学的な推論の部分はもちろんのこと、付録１〜付録４の議論、特に付録３で証明したGentzenの基本定理も有限の立場における推論とみなすことができます。

　さて、本稿ではHeyting算術より強い任意の理論 T  を考察の対象にし、T  における定項のゼロを 0 と書き、n の次の自然数 sn を n' と略記することにし、（メタ言語における）各自然数 n に対し、次のような帰納的な方法で、T  の項 「n「 を定義します：

(A6-1a)  「0「 :º 0

(A6-1b)  「n + 1「 :º 「n「'

　すなわち、「n「 とは、定項 0 の左に１変項関数記号 s を n 個並べて得られる項を表します。これを自然数 n に対応する数字とよぶことにしましょう。また 「1「 を 1 , 「2「 を 2 （以下同様）と略記します。

　以下、理論 T  の公理群をすべてカンマで区切って並べたものを A と書くとき、A, B ® P というsequentが T  で証明可能であることを B├ P と表すことにします。特に B が空の場合、├ P と書いて、P は証明可能であるということにします。例えば、自然数 n に対し、N(「n「) は証明可能です。

　このとき自然数 m , n に対して

(A6-2a)  l £ 「m「├ l = 「0「  Ú  l = 「1「  Ú ¼ Ú  l = 「m「

(A6-2b) ├ 「m + n「 = 「m「 + 「n「

が成り立つことを証明しましょう。

　実際、付録５ (A5-10n) により l £ m'├ l £ m  Ú  l = m' ですから、(A6-1b) により l £ 「m + 1「├ l £ 「m「  Ú  l = 「m + 1「 となるので、自然数 m に関する（メタ言語の）帰納法により (A6-2a) が得られます。

　また (A6-2b) は、m + 0 º m ですから ├ 「m + 0「 = 「m「 が成り立ち、これと ├ 「m「 = 「m「 + 0 と (A6-1a) により n が 0 の場合は明らかです。
　次に、(A6-2b) が n について成り立つと仮定すると、m + (n + 1) º (m + n) + 1 により├ 「m + (n + 1)「 = 「(m + n) + 1「 ですから、これと (A6-1) の n に m + n を代入したもの├ 「(m + n) + 1「 = 「m + n「' により├ 「m + (n + 1)「 = 「m + n「' が得られます。
　一方、(A6-2b) により├ 「m + n「' = (「m「 + 「n「)' となりますから、これと├ (「m「 + 「n「)' = 「m「 + 「n「' により├ 「m + (n + 1)「 = 「m「 + 「n「' が得られます。
　ゆえにこれと (A6-1b) により├ 「m + (n + 1)「 = 「m「 + 「n + 1「 が得られ、n に関する帰納法により (A6-2b) は証明されました。

　さて、自然数に対する演算 f(m ,¼, n) は、条件：

(A6-3) ├ 「f(m ,¼, n)「 =  f(「m「,¼, 「n「)

を満たす、m ,¼, n 以外の変数を持たない T  の（一般には付録５で行ったような ι 量化記号を用いてよいことにした場合の）N 項 f(m ,¼, n) が存在するとき、f(m ,¼, n) によって算術表現されるといいます。

　また、自然数に対する性質 P (m ,¼, n) は、成り立つか成り立たないかいずれかであり、かつ次の条件を満たす、m ,¼, n 以外の変数を持たない T  の命題 P(m ,¼, n) が存在するとき、P(m ,¼, n) によって算術表現されるといいます：

(A6-4a)  ├ P(m ,¼, n) Ú Ø P(m ,¼, n)

(A6-4b)  P (m ,¼, n) が成り立つとき、├ P(「m「,¼, 「n「)

(A6-4c)  P (m ,¼, n) が成り立たないとき、├ Ø P(「m「,¼, 「n「)

　このとき、次が成立します：

(A6-5a)	特定の引数の値を与える演算 f(m ,¼, n) :º m は項 m により算術表現される。
(A6-5b)	定数値を与える演算 f(m ,¼, n) :º k は項 「k「 により算術表現される。
(A6-5c)	次の自然数を与える演算 g(n) :º n + 1 は項 n' により算術表現される。
(A6-5d)	演算 f(k, m ,¼, n) が f(k, m ,¼, n) により、演算 g(i ,¼, j) が g(i ,¼, j) により算術表現されるならば、f(k, m ,¼, n) の k に g(i ,¼, j) を代入して得られる演算 h(i ,¼, j, m ,¼, n) :º f(g(i ,¼, j), m ,¼, n) は f(g(i ,¼, j), m ,¼, n) により算術表現される。
(A6-5e)	演算 f(m ,¼, n) が f(m ,¼, n) により、演算 g(m ,¼, n, i, k) が g(m ,¼, n, i, k) により算術表現されるなら、h(m ,¼, n, 0) :º f(m ,¼, n) と h(m ,¼, n, i + 1) :º g(m ,¼, n, i, h(m ,¼, n, i)) によって帰納的に定義される演算 h(m ,¼, n, i) は、 h(m ,¼, n, 0) = f(m ,¼, n) と h(m ,¼, n, i' ) = g(m ,¼, n, i, h(m ,¼, n, i)) を満たす（存在が保証された） h(m ,¼, n, i) によって算術表現される。
(A6-5f)	命題 R(m ,¼, n) によって算術表現される性質 R(m ,¼, n) が成り立つとき 1 、成り立たないとき 0 として定義した場合分けの演算 f(m ,¼, n) は、項 ι k ( (R(m ,¼, n) Þ k = 1 ) Ù (Ø R(m ,¼, n) Þ k = 0 ) ) により算術表現される。
(A6-5g)	性質 m = n , m < n , m £ n はそれぞれ命題 m = n , m < n , m £ n により算術表現される。
(A6-5h)	性質 P (k, m ,¼, n) が P(k, m ,¼, n) により、演算 f(i ,¼, j) が f(i ,¼, j) により算術表現されるならば、P (k, m ,¼, n) の k に f(i ,¼, j) を代入して得られる性質 R(i ,¼, j, m ,¼, n) :º P ( f(i ,¼, j), m ,¼, n) は P( f(i ,¼, j), m ,¼, n) により算術表現される。
(A6-5i)	性質 P (m ,¼, n) が P(m ,¼, n) により、性質 Q(m ,¼, n) が Q(m ,¼, n) により算術表現されるならば、以下引数を省略すれば、性質「P かつ Q 」、「P 又は Q 」、「P ならば Q 」、「P でない」は、それぞれ P Ù Q , P Ú Q , P Þ Q , Ø P により算術表現される。
(A6-5j)	性質 R(i, m ,¼, n) が R(i, m ,¼, n) により算術表現されるならば、性質「すべての i £ k に対して R(i, m ,¼, n)」、「ある i £ k に対して R(i, m ,¼, n)」はそれぞれ "i £ k : R(i, m ,¼, n) , $i £ k : R(i, m ,¼, n) により算術表現される。

　実際、(A6-5a),(A6-5b) は定義から明らかです。

　また (A6-5c) は (A6-1b) から明らかです。

　また (A6-5d) は、k :º g(i ,¼, j) , l :º h(i ,¼, j, m ,¼, n) と置けば、l = f(k, m ,¼, n) となります。
　ゆえに├ 「k「 = g(「i「 ,¼, 「j「) と ├ 「l「 = f(「k「, 「m「 ,¼, 「n「) が得られ、├ 「l「 = f(g(「i「 ,¼, 「j「), 「m「 ,¼, 「n「) が得られます。

　また (A6-5e) は、l :º h(m ,¼, n, i) と置いたとき、├ 「l「 = h(「m「 ,¼, 「n「, 「i「) となることを、i に関する（メタ言語の）帰納法で証明します。
　まず i が 0 なら、l = f(m ,¼, n) ですから ├ 「l「 = f(「m「 ,¼, 「n「) で、├ h(「m「 ,¼, 「n「, 0) = f(「m「 ,¼, 「n「) から ├ 「l「 = h(「m「 ,¼, 「n「, 0) が得られます。
　次に i で成り立つと仮定し、k :º h(m ,¼, n, i + 1) と置くと、k = g(m ,¼, n, i, l) から ├ 「k「 = g(「m「 ,¼, 「n「, 「i「, 「l「) が得られます。
　一方、帰納法の仮定から ├ 「l「 = h(「m「 ,¼, 「n「, 「i「) なので ├ 「k「 = g(「m「 ,¼, 「n「, 「i「, h(「m「 ,¼, 「n「, 「i「)) が得られます。
　他方、├ h(「m「 ,¼, 「n「, 「i「' ) = g(「m「 ,¼, 「n「, 「i「, h(「m「 ,¼, 「n「, 「i「)) が成り立ちます。
　ゆえにこれらと (A6-1b) の n に i を代入した式により、├ 「k「 = h(「m「 ,¼, 「n「, 「i + 1「) が得られます。

　また (A6-5f) は、l :º f(m ,¼, n) と置き、(A6-5f) の最後の項（この項の定義式で ι量化記号を使ってよいことの証明に、条件 (A6-4a) が必要となることに注意します。）を f(m ,¼, n) と書くことにします。
　まず R(m ,¼, n) が成り立つときは、l は 1 なので 「l「 は 1 であり、しかも仮定により ├ R(「m「 ,¼, 「n「) なので、├  f(「m「 ,¼, 「n「) = 1 すなわち ├ 「l「 =  f(「m「 ,¼, 「n「) となります。
　他方、R(m ,¼, n) が成り立たないときは、l は 0 なので 「l「 は 0 であり、しかも仮定により ├ Ø R(「m「 ,¼, 「n「) なので、├  f(「m「 ,¼, 「n「) = 0 すなわち ├ 「l「 =  f(「m「 ,¼, 「n「) となります。よって証明されました。

　また (A6-5g) は、いずれも成り立つか成り立たないかどちらかであることは明らかで、また前節 (A5-7d),(A5-7e),(A5-8d) により (A6-4a) も成り立つことがわかります。
　また明らかに m = n なら ├ 「m「 = 「n「 です。
　また m < n のときは、自然数 k が存在して n は m + k + 1 と書けるので、├ 「n「 = 「m + k + 1「 が得られますが、更に (A6-1b) と (A5-2b) により ├ 「n「 = 「m「 + 「k「' なので ├ 「m「 < 「n「 が得られます。
　また m £ n のときは、自然数 k が存在して n は m + k と書けるので、├ 「n「 = 「m + k「 が得られますが、(A6-2b) により ├ 「n「 = 「m「 + 「k「 なので、前節 (A5-9) により ├ 「m「 £ 「n「 が得られます。

　また (A6-5h) は、k :º f(i ,¼, j) と置けば ├ 「k「 = f(「i「 ,¼, 「j「) が成り立ち、R(i ,¼, j, m ,¼, n) すなわち P (k, m ,¼, n) が成り立つか成り立たないかに従って、それぞれ ├ P(「k「, 「i「 ,¼, 「j「) 又は ├ Ø P(「k「, 「i「 ,¼, 「j「) が成り立ちます。
　これは更に、それぞれの場合に ├ P( f(「i「 ,¼, 「j「), 「m「 ,¼, 「n「) 又は ├ Ø P( f(「i「 ,¼, 「j「), 「m「 ,¼, 「n「) が成り立つことを意味します。なお、(A6-4a) の成立は明らかです。

　また (A6-5i) ですが、以下 P(「m「 ,¼, 「n「) 及び Q(「m「 ,¼, 「n「) をそれぞれ P 及び Q と略記することにします。まず本文第３節メタ定理39 (a) により (A6-4a) が成り立つことがわかります。
　さて、「P かつ Q」が成り立てば、P も Q も成り立つので ├ P と ├ Q が成り立ち、よって ├ P Ù Q が成り立ちます。一方「P かつ Q」が成り立たなければ、少なくとも P か Q の一方が成り立たないので ├ Ø P か ├ Ø Q が成り立ち、よって ├ Ø (P Ù Q) が成り立ちます。
　また、「P 又は Q」が成り立てば、P か Q のいずれかが成り立つので ├ P 又は ├ Q が成り立ち、よって ├ P Ú Q が成り立ちます。一方「P 又は Q」が成り立たなければ、P も Q も成り立たないので ├ Ø P と ├ Ø Q が成り立ち、よって ├ Ø (P Ú Q) が成り立ちます。
　また、「P ならば Q」について P が成り立つ場合と成り立たない場合に分けて考えると、後者の場合、「P ならば Q」は常に成り立ち、一方 ├ Ø P ですから ├ P Þ Q が成り立ちます。
　一方前者の場合は「P ならば Q」の成否は Q の成否と同じことで、その成否に応じてそれぞれ ├ Q 又は ├ Ø Q が成り立ちますが、├ P が成り立っているのですから、これらに応じてそれぞれ ├ P Þ Q 又は ├ Ø (P Þ Q) が得られます。
　また「P でない」については、「P ならば Q」で Q が「矛盾する」の場合を考えれば明らかです。

　最後に (A6-5j) ですが、まず前節 (A5-11f),(A5-11g) により "i £ k : R(i, m ,¼, n) も $i £ k : R(i, m ,¼, n) も (A6-4a) を満たすことがわかります。
　また「すべての i £ k に対して R(i, m ,¼, n)」が成り立てば、すべての i £ k に対して ├ R(「i「, 「m「 ,¼, 「n「) が成り立ちます。ゆえに (A6-2a) により、├ "i £ 「k「 : R(i, 「m「 ,¼, 「n「) が得られます。
　また「すべての i £ k に対して R(i, m ,¼, n)」が成り立たなければ、R(i, m ,¼, n) が成り立たないような i £ k が存在し、├ Ø R(「i「, 「m「 ,¼, 「n「) となります。ゆえに ├ 「i「 £ 「k「 により ├ $i £ 「k「 : Ø R(i, 「m「 ,¼, 「n「) が、従って ├ Ø "i £ 「k「 : R(i, 「m「 ,¼, 「n「) 得られます。
　また「ある i £ k に対して R(i, m ,¼, n)」が成り立てば、├ 「i「 £ 「k「 なので、├ $i £ 「k「 : R(i, 「m「 ,¼, 「n「) が得られます。
　また「ある i £ k に対して R(i, m ,¼, n)」が成り立たなければ、すべての i £ k で、R(i, m ,¼, n) が成り立たないので ├ Ø R(「i「, 「m「 ,¼, 「n「) が成り立ちます。ゆえに (A6-2a) により ├ "i £ 「k「 : Ø R(i, 「m「 ,¼, 「n「) が、従って ├ Ø $i £ 「k「 : R(i, 「m「 ,¼, 「n「) が得られます。

　さて、ここで (A6-5) で列挙した次の方法：

(A6-6a)	特定の引数の値を与える演算 f(m ,¼, n) :º m
(A6-6b)	定数値を与える演算 f(m ,¼, n) :º k
(A6-6c)	次の自然数を与える演算 g(n) :º n + 1
(A6-6d)	演算 f(k, m ,¼, n) の k に演算 g(i ,¼, j) を代入して得られる演算 h(i ,¼, j, m ,¼, n) :º f(g(i ,¼, j), m ,¼, n)
(A6-6e)	演算 f(m ,¼, n) と演算 g(m ,¼, n, i, k) から h(m ,¼, n, 0) :º f(m ,¼, n) と h(m ,¼, n, i + 1) :º g(m ,¼, n, i, h(m ,¼, n, i)) によって帰納的に定義される演算
(A6-6f)	命題 R(m ,¼, n) によって算術表現される性質 R(m ,¼, n) が成り立つとき 1 、成り立たないとき 0 として定義した場合分けの演算
(A6-6g)	性質 m = n , m < n , m £ n
(A6-6h)	性質 P (k, m ,¼, n) の k に演算 f(i ,¼, j) を代入して得られる性質 R(i ,¼, j, m ,¼, n) :º P ( f(i ,¼, j), m ,¼, n)
(A6-6i)	性質 P (m ,¼, n) と性質 Q(m ,¼, n) から作られる（以下引数を省略）性質「P かつ Q 」、「P 又は Q 」、「P ならば Q 」、「P でない」
(A6-6j)	性質 R(i, m ,¼, n) から作られる性質「すべての i £ k に対して R(i, m ,¼, n)」、「ある i £ k に対して R(i, m ,¼, n)」

のみを組み合わせて得られる演算 f (m ,¼, n) を帰納的演算とよび、(A6-6) の方法のみを組み合わせて作られる性質 P (m ,¼, n) を帰納的性質とよぶことにします。
　帰納的性質 P (m ,¼, n) は、Heyting算術における（メタ）命題とみなすことができますから、これをそっくりそのまま理論 T  における命題 P(m ,¼, n) に“翻訳”することができますが、(A6-5) のそれぞれを見れば明らかなように、そこで実際に構成している P (m ,¼, n) を算術表現する命題は、この翻訳された命題 P(m ,¼, n) に他なりません。帰納的演算についても同様です。すなわち

(A6-7a)	帰納的演算 f(m ,¼, n) は、それをHeyting算術におけるメタ項だと思って T  の中に翻訳して得られる項 f(m ,¼, n) によって算術表現される。
(A6-7b)	帰納的命題 R(m ,¼, n) は、それをHeyting算術におけるメタ命題だと思って T  の中に翻訳して得られる命題 P(m ,¼, n) によって算術表現される。

ということがわかります。

　自然数の和 m + n 、積 mn 、冪 mⁿ 、差 m - n 、算術表現可能な演算の有限和 å_{i £ n} f(i, j ,¼, k) 及び有限積 Õ_{i £ n} f(i, j ,¼, k) 、算術表現可能な性質 P から作った max{ i £ k | P (i) } や、 k / n , σ , τ , n[i] , | n | , { k } , m * n , ν , μ_n , 「n「 などの演算や、k = n , k < n , k £ n , k | n などの性質は、すべて帰納的です。

　また、付録１における文字列 A が論理式であるかどうかの判定において、A （あるいは A と T ) に現れない k 個の変数を任意に選ぶ箇所がありますが、A （あるいは A * T ）と同一視される自然数を n とするとき、A （あるいは A と T ）に現れる変数の添字は n を超えないことに注意すれば、これらの変数として x_n+i ( 1 £ i £ k ) を選ぶことにすれば、すべてのステップが (A6-6) の組み合わせで構成できます。
　また、ある文字列の中の一文字を別の文字に置き換える操作も明らかに (A6-6) の組み合わせで構成できるので、A^(k) も帰納的です。以上により、「文字列 A は論理式である」という性質も算術表現可能であることがわかりました。

　また、論理式 A に対して A の標準的な構成手続き C を対応させる演算も明らかに算術表現可能で、しかも付録１ (A1-16) の、論理式 A の変数 x に論理式 T を代入する操作も帰納的であることがわかります。

　以上の事実に注意して付録１の (A1-13) 以降の議論を眺めれば、「２階の文字列 S はsequentになっている」とか「３階の文字列 P は証明文になっている」とか「１階の文字列 P , A₁ ,¼, A_n は命題になっていて、各 A_i は公理であり、３階の文字列 P は証明文になっていて、更にsequent “ A₁ ,¼, A_n ® P ”は P の中で証明されている」という性質も帰納的であることがわかります。

　そこで、自然数 n , p に関する性質：

n はある命題と、p はある証明文とそれぞれ同一視できる正整数で、n と同一視される命題のすべての変数に数字 「n「 を代入した命題が、p と同一視される証明文の中で証明されている。

を A(n, p) と書くことにすると、この性質も帰納的であり、従ってこれをHeyting算術におけるメタ命題だと思って理論 T  内に翻訳して得られる命題を A(n, p) と書けば、(A6-7b) により A(n, p) は A(n, p) で算術表現できることがわかります。
　そこで "p : Ø A(n, p) という命題と同一視される正整数を g と書いて、G( p)  :º  Ø A(「g「, p) と置きます。
　このとき、g と同一視される命題の変数に自分自身に対応する数字 「g「 を代入して得られる命題は、"p : Ø A(「g「, p) すなわち "p G( p) となりますが、このとき次の結果が成り立ちます：

不完全性定理（Gödel） 　理論 T  には、次の性質を持つ1変項命題 G( p) が存在する： (G1)　すべての自然数 p に対して ├ G(「p「) 、すなわち ├ G(0) , ├ G(1) , ├ G(2) ,¼ である。 (G2)　├ "p G( p) ならば T  は矛盾する。

　実際、任意に自然数 p を取ります。
　もし p が命題 "p G( p) の証明文と同一視できる正整数ならば、そもそも ├ "p G( p) なのですから、推論規則 (" 消去) を適用して├ G(「p「) となります。
　また、そうでない場合は、A( g, p) が成り立たないということですから├ Ø A(「g「, 「p「) すなわち├ G(「p「) が得られます。
　ゆえに、いずれにせよ├ G(「p「) となり、p は任意でしたから、(G1) は証明されました。

　次に、"p G( p) は、g と同一視される命題の全変数に項 「g「 を代入した命題ですが、これが証明可能なら、その証明文の一つと同一視される正整数を p とすると、これは A( g, p) が成り立っていることを意味します。
　ゆえに├ A(「g「, 「p「) となりますが、一方で├ "p G( p) すなわち├ "p : Ø A(「g「, p) から (" 消去) により├ Ø A(「g「, 「p「) が得られるので T  は矛盾し、(G2) も証明されました。

　この定理は、Heyting算術より強い無矛盾な理論では、すべての数字に対して証明されるにもかかわらず、全称記号 " で束縛した命題は証明できないような命題が存在することを意味しています。
　ただし、この命題（Gödel命題） "p G( p) は、理論 T  が無矛盾ならば証明不可能であることは言えますが、一般に反証不可能性は持っていません。反証も不可能であるためには、理論 T  が無矛盾より強いw-無矛盾という性質、すなわち「一般に、上記の (G1) の性質を満たす命題 G( p) については Ø "p G( p) という形の命題は証明できない」という性質を持つという条件が必要です。

　しかし、命題の構成の仕方に一工夫すると、理論 T  のw-無矛盾を仮定しなくても、単に無矛盾であると仮定するだけで、決定不能、すなわち証明も反証もできないような命題を構成することができます。

　実際、自然数 n , p に関する性質：

n はある命題と、p はある証明文とそれぞれ同一視できる正整数で、n と同一視される命題の否定命題のすべての変数に数字 「n「 を代入した命題が、p と同一視される証明文の中で証明されている。

を B(n, p) と書くことにすると、この性質も帰納的であり、従ってこれをHeyting算術におけるメタ命題だと思って理論 T  内に翻訳して得られる命題を B(n, p) と書けば、(A6-7b) により B(n, p) は B(n, p) で算術表現できることがわかります。
　そこで、"p ( A(n, p)  Þ  $q £ p B(n, q) ) という命題と同一視される正整数を r と書いて、R( p)  :º  A(「r「, p)  Þ  $q £ p B(「r「, q) と置きます。
　このとき、r と同一視される命題の変数に自分自身に対応する数字 「r「 を代入して得られる命題は "p R( p) となりますが、このとき次の結果が成り立ちます：

不完全性定理（Rosser） 　理論 T  には、次の性質を持つ1変項命題 R( p) が存在する： (R1)　すべての自然数 p に対して ├ R(「p「) すなわち ├ R(0) , ├ R(1) , ├ R(2) ,¼ である。 (R2)　├ "p R( p) ならば T  は矛盾する。 (R3)　├ Ø"p R( p) ならば T  は矛盾する。

　実際、任意に自然数 p を取ります。もし p が命題 "p R( p) の証明文と同一視される正整数ならば、そもそも├ "p R( p) なのですから (" 消去) により├ R(「p「) となります。
　また、そうでない場合は、A(r, p) が成り立たないということですから├ Ø A(「r「, 「p「) となり、R(「p「)  º  A(「r「, 「p「)  Þ  $q £ 「p「 B(「r「, q) なのですから、第３節メタ定理14により├ R(「p「) が得られます。
　ゆえに、いずれにせよ├ R(「p「) となり、p は任意でしたから、(R1) は証明されました。

　次に、"p R( p) は、正整数 r と同一視される命題の全変数に項 「r「 を代入して得られる命題ですから、もしこれが証明可能なら、その証明文の一つと同一視される正整数を p とすれば、A(r, p) が成り立っていることになるので、├ A(「r「, 「p「) となります。
　ここで、0 , 1 ,¼, p のいずれかが Ø "p R( p) の証明文と同一視される正整数になっている場合は、そもそも ├ Ø "p R( p) なのですから T  は矛盾します。
　また、そうでない場合は、B(r, 0) , B(r, 1) ,¼, B(r, p) がすべて成り立たないので、├ Ø B(「r「, 「0「) , ├ Ø B(「r「, 「1「) ,¼, ├ Ø B(「r「, 「p「) となります。
　ところが (A6-2a) により ├ "q £ 「p「 : Ø B(「r「, q) すなわち ├ Ø $q £ 「p「 : B(「r「, q) が得られ、これと├ A(「r「, 「p「) により├ Ø R(「p「) が得られます。ところが├ "p R( p) なのですから、(" 消去) により├ R(「p「) となり、T  は矛盾します。
　すなわちいずれの場合でも T  は矛盾するので (R2) は証明されました。

　最後に、Ø "p R( p) は、正整数 r と同一視される命題の否定命題の全変数に項 「r「 を代入した命題ですから、もしこれが証明可能なら、その証明文の一つと同一視される正整数を p とすれば、B(r, p) が成り立っていることになるので、├ B(「r「, 「p「) となります。
　ここで、0 , 1 ,¼, p のいずれかが "p R( p) の証明文と同一視される正整数になっている場合は、そもそも├ "p R( p) なのですから T  は矛盾します。
　また、そうでない場合は、A(r, 0) , A(r, 1) ,¼, A(r, p) がすべて成り立たないので、├ Ø A(「r「, 「0「) , ├ Ø A(「r「, 「1「) ,¼, ├ Ø A(「r「, 「p「) となります。
　従って (A6-2a) により p £ 「p「├ Ø A(「r「, p) となり、R( p)  º  A(「r「, p)  Þ  $q £ p B(「r「, q) なので、第３節メタ定理14により p £ 「p「├ R( p) が得られます。
　一方├ B(「r「, 「p「) ですから ($ 導入) により p > 「p「├ $q £ p : B(「r「, q) となり、第３節メタ定理９により p > 「p「├ R( p) となります。
　ゆえに├ p £ 「p「  Ú  p > 「p「 に注意すれば、(Ú 消去) により├ R( p) が得られ、(" 導入) により├ "p R( p) となり、T  は矛盾します。
　すなわちいずれの場合でも T  は矛盾するので (R3) は証明されました。

　このRosserにより改良された不完全性定理により、Heyting算術より強い無矛盾な理論では、（排中律を仮定してもしなくても）証明も反証もできない決定不能な閉命題が必ず存在することがわかります。

　さて、ここでGödel命題 "p G( p) の“意味”を考えるため、“命題 "p G( p) は証明できない”という性質を、理論 T  の中へ翻訳してみましょう。
　命題 "p G( p) は、正整数 g と同一視される命題の変数に項 「g「 を代入した命題です。ゆえに "p G( p) が証明できない、すなわち“どんな証明文の中でも証明されていない”という主張は、“任意の自然数 p に対して A( g, p) でない”と言い換えることができます。
　ゆえにこれを T  の中の命題に翻訳すると、具体的な自然数 g は具体的な数字 「g「 に翻訳されますから、この性質は "p : Ø A(「g「, p) という命題に翻訳されることがわかります。ところが、この命題は "p G( p) 自身に他なりません。すなわち、Gödel命題というのは“自分は証明できない”ということを意味する命題だとみなすことができるわけです。

　ところで、“T  は無矛盾である”、すなわち“任意の証明文で ^ は証明されていない”という性質は、T  の中に "p : Ø A(「^「, p) と翻訳されるので、この命題を Consis と略記することにすれば、Gödelの不完全性定理 (G2) の対偶である“T  が無矛盾なら "p G( p) は証明できない”というメタ定理の証明を理論 T  内部の証明に翻訳することによって、├ Consis Þ "p G( p) が得られます。
　ゆえに、├ Consis を仮定すると、(Þ 消去) により├ "p G( p) が得られますが、ここでGödelの不完全性定理の (G2) を用いると、T  は矛盾することがわかります。すなわち次の結果が得られました：

第二不完全性定理（Gödel） 　理論 T  において、自分自身の無矛盾性を内部に翻訳した命題 Consis が証明できれば、T  は矛盾する。

　さて、一般に、帰納的な性質は、それを T  の中に翻訳した命題によって算術表現されるのでした。
　それでは、帰納的な性質 P を算術表現する命題は、いつでも P を T  の中に翻訳した命題の代わりに使えるかというと、そうとは限りません。

　例えば Gödel の不完全性定理の証明に出てきた性質 A(n, p) を考えてみましょう。
　A(n, p) を T  に翻訳した命題は A(n, p) ですが、A*(n, p)  :º  A(n, p) Ù "q £ p : Ø B(n, q) と置くと、実はこの命題 A*(n, p) も性質 A(n, p) を算術表現しています。
　実際、A(n, p) が成り立っていれば、まず ├ A(「n「, 「p「) が成り立ちます。
　ここで、0 £ q £ p を満たすある自然数 q に対して B(n, q) が成り立っていれば、これは、正整数 n と同一視される命題が、かたや正整数 p と同一視できる証明文の中で証明され、かたや正整数 q と同一視できる証明文の中で反証されているということですから、T  は矛盾します。ゆえに矛盾する理論 T  では任意の命題が証明可能で、特に命題 A*(「n「, 「p「) も証明できます。
　他方、B(n, q) が成り立つような自然数 0 £ q £ p が無ければ、├ Ø B(「n「, 「0「) , ├ Ø B(「n「, 「1「) ,¼, ├ Ø B(「n「, 「p「) が成り立ち、(A6-2a) により├ "q £ 「p「 : Ø B(「n「, q) がわかり、この場合も A*(「n「, 「p「) は証明できるので、いずれにせよ├ A*(「n「, 「p「) となります。
　また A(n, p) が成り立たなければ、├ Ø A(「n「, 「p「) なので、この場合は明らかに├ Ø A*(「n「, 「p「) が成り立ちます。
　以上で、命題 A*(n, p) もまた性質 A(n, p) を算術表現していることがわかりました。

　そこで、“理論 T  は無矛盾である”という性質を T に翻訳した命題 "p : Ø A(「^「, p) を Consis と略記したのに倣って、命題 A の部分を A* に置き換えて得られる命題 "p : Ø A*(「^「, p) のことを Consis* と略記することにしましょう。
　すると、Ø ^ は証明可能、すなわち ^ は反証可能ですから、命題 ^ が反証されている証明文と同一視される正整数を p とすれば、B(^, p) が成り立ち、従って├ B(「^「, 「p「) が成り立ちます。
　もし 0 , 1 ,¼, p のいずれかが ^ の証明文と同一視される正整数になっている場合は、そもそも ^ が証明されるので理論 T  は矛盾し、任意の命題は証明可能ですから、特に Consis* は証明可能です。
　また、そうでない場合は、A(^, 0) , A(^, 1) ,¼, A(^, p) がすべて成り立たないので、├ Ø A(「^「, 「0「) , ├ Ø A(「^「, 「1「) ,¼, ├ Ø A(「^「, 「p「) となります。
　従って (A6-2a) により p £ 「p「├ Ø A(「^「, p) となりますが、A*(「^「, p)  º  A(「^「, p) Ù "q £ p : Ø B(「^「, q) なので p £ 「p「├ Ø A*(「^「, p) が得られます。
　一方├ B(「^「, 「p「) ですから ($ 導入) により p > 「p「├ $q £ p : B(「^「, q) となるので、p > 「p「├ Ø A*(「^「, p) が得られます。
　ゆえに├ p £ 「p「  Ú  p > 「p「 に注意すれば、(Ú 消去) により├ "p : Ø A*(「^「, p) すなわち Consis* は、（Consisの場合とは異なり）理論 T  で証明できてしまうことがわかります。

　以上の例はKreiselによるもので、Kreiselの注意とよばれています。