数学の基礎

　本節では、付録５で解説したHeyting算術の中で ε₀ 未満の順序数という概念を定義して、超限帰納法が成立するようにすることができることを解説します。

　自然数 a を２進展開し、通常用いられる２進数字 “ 0 ” と “ 1 ” のかわりにそれぞれ “ » ” と “ « ” を用いることにします。このとき a の桁数を | a | と書くことにし、左から i 桁目までの i 個の数字のうち “ « ” の個数を l_i(a) と書き、“ » ” の個数を r_i(a) と書くと、明らかに

(A7-1a)  li(a) + ri(a) = i       (  1 £ i £ | a |  )

となっていますが、更に

(A7-1b)  li(a) > ri(a)       (  1 £ i < | a |  )

(A7-1c)  li(a) = ri(a)       (  i = | a |  )

の関係が成り立っているとき、a を（ε₀ 未満の）構成的順序数とよび、本節と次節では省略して単に順序数とよぶことにします。
　まず、条件 (A7-1c) により、桁数 a は 2 以上でなければならないことがわかります。
　また、(A7-1b) で i を 1 とすればわかるように、a の左端の数字は “ « ” であることがわかり、また (A7-1b) で i を | a | - 1 としたものと (A7-1c) とを比較することにより、a の右端の数字は “ » ” であることがわかります。

　順序数 a に対し、

(A7-2)  li(a) = ri(a) + 1

が成り立っているような i を a の節目とよぶことにし、j 番目の節目のことを v( j) と書くことにします。
　明らかに 1 と | a | - 1 は a の節目ですが、a の節目の個数から 1 を引いたものを a の項数とよぶことにします。a の項数を k とするとき、各正整数 j < k に対し、a の２進展開の 左から第 v( j) + 1 桁目から第 v( j + 1) 桁目までを切り出した２進数が表わす自然数を a_j と書くと、a の２進展開は

(A7-3)  a º « a1 a2 ¼ ak »

と書かれることになりますが、a の左端が “ « ” であることと節目の定義により、各 a_j は順序数であることがわかります。

　特に k がゼロの場合、すなわち « » のことを（紛れの無い限り） 0 とも書き、« 0 » すなわち « « » » のことを 1 とも書き、« 1 » すなわち « « « » » » のことを w とも書き、一般に « a » のことを w^a とも書くことにします。特に 1 と w はそれぞれ w⁰ , w¹ とも書かれることになります。
　また、順序数 a と自然数 k に対し、« a »_k を、帰納的に

(A7-4a)  « a »0 :º a

(A7-4b)  « a »k+1 :º « « a »k »

で定義します。明らかに « a »₁ º « a » です。

　さて、２つの順序数 a º « a₁ ¼ a_p » と b º « b₁ ¼ b_q » に対して、それらの単純和 a + b と 単純積 a · b を

(A7-5a)  a + b :º « a1 ¼ ap b1 ¼ bq »

(A7-5b)  a · b :º « s11 s12 ¼ s1q s21 s22 ¼ s2q s31 ¼ sp1 ¼ spq »       ( ただし sij :º ai + bj )

で定義します。このとき

(A7-6a)  « a » + « b » º « a b »

(A7-6b)  « a » · « b » º « a + b »

(A7-6c)  a + 0 º 0 + a º a

(A7-6d)  (a + b) + g º a + (b + g)

(A7-6e)  a · 0 º 0 · a º 0

(A7-6f)  a · 1 º 1 · a º a

(A7-6g)  (a · b) · g º a · (b · g)

(A7-6h)  (a + b) · g º a · g + b · g

が成り立ちます。
　実際、(A7-6a) と (A7-6b) は、定義式 (A7-5) において p = q = 1 の場合に他なりません。
　また (A7-6c) は、(A7-5a) において q = 0 又は p = 0 の場合を考えれば明らかです。
　また (A7-6d) は、g º « g₁ ¼ g_r » と置けば、両辺とも « a₁ ¼ a_p b₁ ¼ b_q g₁ ¼ g_r » と書けるので明らかです。
　また (A7-6e) は、a_i か b_j の一方が空なら (A7-5b) の s_ij も空なので明らかです。
　また (A7-6f) は、a º 1 なら p = 1 かつ a₁ º 0 なので、(A7-5b) の s_ij は i = 1 のみで、しかも (A7-6c) により s_1j º a₁ + b_j º 0 + b_j = b_j ですから 1 · b º b が得られます。
　同様に、b º 1 なら q = 1 かつ b₁ º 0 なので、(A7-5b) の s_ij は j = 1 のみで、しかも (A7-6c) により s_i1 º a_i + b₁ º a_i + 0 = a_i ですから a · 1 º a が得られます。
　また (A7-6g) は、g º « g₁ ¼ g_r » と置けば、(A7-6d) により (A7-6d) のような単純和の連結を括弧を省略して s_ijk º a_i + b_j + g_k と置けば、両辺とも « s₁₁₁ s₁₁₂ ¼ s_11r s₁₂₁ ¼ s_12r ¼ s_1qr s₂₁₁ ¼ s_2qr ¼ s_pqr » となるので明らかです。
　また (A7-6h) は、g º « g₁ ¼ g_r » と置き、s_ij º a_i + g_j 、t_ij º b_i + g_j と置けば、両辺とも « s₁₁ s₁₂ ¼ s_1r s₂₁ ¼ s_2r ¼ s_pr t₁₁ t₁₂ ¼ t_1r t₂₁ ¼ t_2r ¼ t_qr » となるので明らかです。

　次に、順序数 a に対し、(A7-1b) により l_i(a) - r_i(a) > 0 となる正整数 i £ | a | が存在します。そこで

(A7-7)  dim a :º max{  li(a) - ri(a)  |  1 £ i £ | a |  } - 1

で定義される自然数のことを a の次元 とよぶことにします。このとき

(A7-8a)  dim 0 º 0

(A7-8b)  dim 1 º 1

(A7-8c)  dim w º 2

(A7-8d)  dim « a1 ¼ ak » :º max{ dim a1 ,¼, dim ak } + 1       ( k ³ 1 )

(A7-8e)  dim a º 0  Û  a º 0

(A7-8f)  dim « a1 ¼ ak » º 1  Û  ( k ³ 1  Ù  "i £ k : ai º 0 )

(A7-8g)  dim « a »k º dim a + k

(A7-8h)  dim (a + b) º max{ dim a , dim b }

(A7-8i)  a, b  /º 0  Þ  dim (a · b) º max{ dim a , dim b }

が成り立ちます。
　実際、(A7-8a)~(A7-8c) が成り立つことは簡単に確かめることができます。
　また (A7-8d) は、l_|ai|(a_i) = r_|ai|(a_i) と、a が “ « ” で始まることから、max{ l_i(a) - r_i(a) | 1 £ i £ | a | } = max{ l_j(a_i) - r_j(a_i) | i £ k, 1 £ j £ | a_i | } + 1 となるので明らかです。
　また (A7-8e) は、(A7-8a) と、(A7-8d) の右辺が 0 にならないことから明らかです。
　また (A7-8f) は、(A7-8d) において dim a_i = 0 ( 1 £ i £ k ) となるので (A7-8e) により明らかです。
　また (A7-8g) は、(A7-8d) により dim « a »_k+1 º dim « « a »_k » = max{ dim « a »_k } + 1 = dim « a »_k + 1 となるので、(A7-4a) と k に関する帰納法により明らかです。
　また (A7-8h) は、dim « a₁ ¼ a_p b₁ ¼ b_q » = max{ dim a₁ ,¼, dim a_p , dim b₁ ,¼, dim b_q } + 1 = max{ dim « a₁ ¼ a_p » , dim « b₁ ¼ b_q » } となるので明らかです。
　また (A7-8i) は、(A7-5b) の記法を用いると、(A7-8h) により dim s_ij = dim (a_i + b_j) = max{ dim a_i , dim b_j } となります。
　ゆえに、dim (a · b) = max{ dim s_ij | 1 £ i £ p , 1 £ j £ q } + 1 = max{ max{ dim a_i | 1 £ i £ p } , max{ dim b_j | 1 £ j £ q }} + 1 となるので明らかです。

　上記の (A7-8e),(A7-8f) により、dim a £ 1 であるような順序数 a は、ゼロ個以上の 0 により « 0 0 ¼ 0 » と書けるので、このような順序数を、この表現における 0 の個数である自然数 k と同一視することにします。この同一視において、順序数の単純和と単純積は、明らかにこれらを自然数とみなしたときの自然数の和と積にそれぞれ一致します。

　さて、一般に排中律を満たす強順序 “ < ”（本文第23節 (23-15) 参照）すなわち

(A7-9a)  a < b  Ú  Ø a < b

(A7-9b)  Ø ( a < b  Ù  b < a )

(A7-9c)  a < b  Þ  ( a < g  Ú  g < b )

を満たす２項関係が与えられている場合、一般に

(A7-10a)  a > b  :º  b < a

(A7-10b)  a £ b  :º  b ³ a  :º  Ø b < a

(A7-10c)  a ¹ b  :º  a < b  Ú  b < a

(A7-10d)  a = b  :º  a £ b  Ù  b £ a

と定義すると、本文第23節の (23-16) がすべて成立するのでした。

　さて、一般に自然数 n に対し、| a | , | b | < n であるような順序数間の排中律を満たす２項関係 ~ は、a ~ b を満たす a と b からなる１階の文字列を（１階の文字列をHeyting算術における本来の自然数とみなした場合の自然数に対する本来の順序で）１列に並べた２階の文字列とみなすことにより、Heyting算術の中で扱えることに注意します。

　| a | , | b | < n であるような順序数間に排中律を満たす強順序 “ <_n ” が与えられているとき、“ <_n ” に伴う擬順序関係を “ £_n ” と書けば、これはこれに伴う同値関係 “ =_n ” のもとで全順序になります（本文第23節 (23-16) の証明直後の注意を参照）。
　そこで、| a | £ n であるような 0 でない順序数 a º « a₁ ¼ a_p » に対して、| a_j | < n ですから

(A7-11)  "j £ p : aj £n ai

を満たす a_i が少なくとも一つ存在します。そのような a_i のうち、添字 i が最大のものを pr_n a と書き、a º « a₁ ¼ a_p » の並びから pr_n a である a_i を取り除いて得られる順序数を res_n a と書くことにします。このとき | pr_n a | , | res_n a | < n であることに注意します。
　そこで、| a | , | b | < n であるような順序数間の２項関係 “ <_n ” を、帰納的に

(A7-12)  a <n+1 b  :º  b /º 0  Ù  ( a º 0  Ú  prn a <n prn b  Ú  ( prn a =n prn b  Ù  resn a <n resn b ) )       (  | a | , | b | £ n  )

で定義します。このとき、２項関係 “ <_n ” が強順序になっていることを n に関する帰納法で証明しましょう。
　まず (A7-9a) の排中律が成り立つことは、(A7-12) の右辺の各２項関係が、帰納法の仮定により排中律を満たすので明らかです。
　次に (A7-9b) ですが、a <_n+1 b と b <_n+1 a が共に成り立つと仮定すると、a も b も 0 ではないので、pr_n a <_n pr_n b  Ú  pr_n a =_n pr_n b が成り立つと同時に pr_n b <_n pr_n a  Ú  pr_n b =_n pr_n a が成り立つので、帰納法の仮定により “ <_n ” が (A7-9b) を満たすことから、どの組み合わせでも矛盾することがわかります。
　最後に (A7-9c) ですが、a <_n+1 b を仮定して | g | £ n であるような順序数 g を取ると、まず g º 0 なら g <_n+1 b が成り立つので、以下 g が 0 でない場合を考えます。
　ここで場合分けをして、まず a º 0 が成り立つときは a <_n+1 g が成り立ちます。
　次に pr_n a <_n pr_n b の場合は、g が 0 でないことから pr_n g が定義され、更に帰納法の仮定により “ <_n ” が (A7-9c) を満たすことから pr_n a <_n pr_n g 又は pr_n g <_n pr_n b が成り立ち、これらはそれぞれ a <_n+1 g あるいは g <_n+1 b を意味します。
　最後に pr_n a =_n pr_n b  Ù  res_n a <_n res_n b の場合を考えます。この場合は、帰納法の仮定により pr_n g <_n pr_n a =_n pr_n b 又は pr_n g >_n pr_n a =_n pr_n b 又は pr_n g =_n pr_n a =_n pr_n b のいずれかが成り立ちます。
　この第１の場合は g <_n+1 b が、第２の場合は a <_n+1 g が成り立ちます。
　また第３の場合は、更に帰納法の仮定により res_n a <_n res_n g 又は res_n g <_n res_n b が成り立ち、これらはそれぞれ a <_n+1 g あるいは g <_n+1 b を意味します。
　以上で２項関係 “ <_n ” が排中律を満たす強順序になっていることが証明されました。

　さて、k に関する帰納法により、| a | , | b | < n なら a <_n b Û a <_n+k b であることがわかるので、任意の順序数 a , b に対し、n :º max{ | a | , | b | } と置いて、pr_n a , res_n a , a <_n+1 b のことをそれぞれ pr a , res a , a < b と書くことにすれば、明らかに “ < ” も排中律を満たす強順序で、(A7-12) より明らかなように

(A7-13a)  a < b  Û  ( b /º 0  Ù  ( a º 0  Ú  pr a < pr b  Ú  ( pr a = pr b  Ù  res a < res b ) ) )

が成り立ちます。ゆえにこの両辺の否定を取り、a と b を入れ替えれば、

(A7-13b)  a £ b	Û  ( a º 0  Ú  ( b /º 0  Ù  pr a £ pr b  Ù  ( pr a ¹ pr b  Ú  res a £ res b ) ) )
	Û  ( a º 0  Ú  ( b /º 0  Ù  ( ( pr a £ pr b  Ù  pr a ¹ pr b )  Ú  ( pr a £ pr b  Ù  res a £ res b ) ) ) )
	Û  ( a º 0  Ú  ( b /º 0  Ù  ( pr a < pr b  Ú  ( pr a £ pr b  Ù  res a £ res b ) ) ) )
	Û  ( a º 0  Ú  ( b /º 0  Ù  ( pr a < pr b  Ú  ( pr a = pr b  Ù  res a £ res b ) ) ) )

　従って (A7-10d) により

(A7-13c)  a = b  Û  ( a º b º 0  Ú  ( a /º 0  Ù  b /º 0  Ù  pr a = pr b  Ù  res a = res b ) )

が成り立ちます。これらを用いて

(A7-14a)	a = b と « a » = « b » は同値。従ってこれらは一般に « a »k = « b »k とも同値。
(A7-14b)	a < b と « a » < « b » は同値。従ってこれらは一般に « a »k < « b »k とも同値。
(A7-14c)	dim a < dim b なら a < b
(A7-14d)	a £ b なら dim a £ dim b
(A7-14e)	a = b なら dim a = dim b
(A7-14f)	dim a < n なら a < « 0 »n
(A7-14g)	自然数 k > 0 に対して a < « a »k
(A7-14h)	a < w となるのは、a が自然数である場合、その場合に限る。
(A7-14i)	a + b = b + a
(A7-14j)	a = b と a + g = b + g は同値
(A7-14k)	a < b と a + g < b + g は同値。
(A7-14l)	a · b = b · a
(A7-14m)	a = b なら a · g = b · g であり、かつ g > 0 なら逆も成り立つ。
(A7-14n)	g > 0 のとき、a < b と a · g < b · g は同値。
(A7-14o)	自然数 n , m と k' < k に対して « n · a + m · b »k' < « a + b »k
(A7-14p)	自然数 m , n と順序数 a > 0 に対して n · a + m < w · a
(A7-14q)	a > 0 かつ b > 0 のとき、« a » + « b » < « a + b » あるいはもっと一般に、k > 0 に対して « a »k + « b »k < « a + b »k が成り立つ。
(A7-14r)	a > 0 , b > 0 , k' £ k , « a¢ »k' £ « a »k  , « b¢ »k' £ « b »k ならば « a + b¢ »k' £ « a + b »k となる。しかも前提の中にある３個の £ のうち少なくとも一つを < に置き換えれば、結論の £ を < に置き換えることができる。
(A7-14s)	a > 0 で b < « g1 ¼ gr a » かつすべての i に対して a £ gi ならば、a' < a が存在して b < « g1 ¼ gr a' ¼ a¢ » の形の式が成り立つ。

が成り立つことを証明しましょう。
　(A7-14a) と (A7-14b) は pr « a » º a , pr « b » º b , res « a » º res « b » º 0 により明らかです。
　以下、a º « a₁ ¼ a_p » , b º « b₁ ¼ b_q » , g º « g₁ ¼ g_r » と表示しておくことにします。
　次の (A7-14c) を n º dim b に関する帰納法で証明します。
　a が 0 なら、(A7-8e) により dim a = 0 ですから dim b > 0 となり、従って (A7-8e) により b は 0 でなく、従って a < b となります。
　また a が 0 でなければ、(A7-8e) により dim a ¹ 0 が、従って dim b ¹ 0 が得られます。そこで a_k :º pr a , b_l :º pr b と置くと、任意の i £ p と j £ q に対して a_i £ a_k , b_j £ b_l となります。
　一方 dim a_k も dim b_l も共に n 未満ですから、帰納法の仮定と (A7-14c) の対偶を取ることにより dim a_i £ dim a_k , dim b_j £ dim b_l が成り立ち、従って (A7-8d) により dim a = dim a_k + 1 , dim b = dim b_l + 1 が成り立ち、従って dim a_k < dim b_l となるので、帰納法の仮定により a_k < b_l すなわち pr a < pr b が得られるので、(A7-13a) により a < b が得られます。
　次の (A7-14d) は (A7-14c) の対偶により明らかです。
　次の (A7-14e) は (A7-14d) 及びその a と b を入れ替えたものにより明らかです。
　次の (A7-14f) は、(A7-8a),(A7-8g) により dim « 0 »_n = n ですから、(A7-14c) により明らかです。
　次の (A7-14g) は、(A7-8g) と (A7-14c) により明らかです。
　次の (A7-14h) は、a º 0 の場合は成り立つので a が 0 でない場合を考えれば十分ですが、pr w = 1 , res w = 0 ですから、a < w は pr a < 1 すなわちすべての i に対して a_i < 1 であることと同値ですが、もし a_i が 0 でないとすると、pr 1 º res 1 º 0 と矛盾するので a_i º 0 となります。
　次の (A7-14i) は、a = « a₁ » + ¼ + « a_p » 及び b = « b₁ » + ¼ + « b_q » と分解することにより、a = « a¢ » , b = « b¢ » と書ける場合について示せば十分です。
　まず a¢ < b¢ のときは、pr (a + b) º pr « a¢b¢ » º b¢ º pr « b¢a¢ » º pr (b + a) かつ res (a + b) º res « a¢b¢ » º « a¢ » º res « b¢a¢ » º res (b + a) ですから (A7-13c) により明らかです。a¢ > b¢ の場合も同様です。
　また a¢ = b¢ のときは、pr (a + b) º pr « a¢b¢ » º b¢ = a¢ º pr « b¢a¢ » º pr (b + a) が成り立ち、更に (A7-14a) により « a¢ » = « b¢ » となることに注意すれば、res (a + b) º res « a¢b¢ » º « a¢ » = « b¢ » º res « b¢a¢ » º res (b + a) ですから、やはり (A7-13c) により明らかです。
　次の (A7-14j) と (A7-14k) は、g = « g₁ » + ¼ + « g_r » と書けるので、g = « g¢ » と書ける場合について示せば十分で、しかも “ £ ” が排中律を満たす全順序であることから、左辺から右辺を導けば十分です。
　しかも b が 0 なら (A7-14k) はあり得ず、(A7-14j) では a も 0 となって (A7-6c) により明らかですから、b は 0 でないと仮定すれば十分です。
　また a が 0 なら、(A7-14j) では b も 0 となるので自明であり、(A7-14k) では pr (a + g) º pr g º g¢ , pr (b + g) ³ pr g º g¢ 及び res (a + g) º res g º 0 と res (b + g) が 0 でないことから明らかです。ゆえに、以下 a も b も 0 でないものとして、n :º max{ | a | , | b | } に関する帰納法により証明します。
　まず g¢ ³ pr b の場合を考えると、pr b ³ pr a ですから pr (a + g) º pr (b + g) º g¢ で、従って res (a + g) º a , res (b + g) º b です。
　ゆえに a = b であるか a < b であるかに応じてそれぞれ res (a + g) = res (b + g) あるいは res (a + g) < res (b + g) となるので、(A7-13) によりこの場合は明らかです。
　次に g¢ < pr b の場合を考えます。
　まず (A7-14j) の場合、pr a = pr b > g¢ なので pr (a + g) º pr a = pr b º pr (b + g) となります。しかも | res a | , | res b | < n で res a = res b ですから、帰納法の仮定により res (a + g) º res a + g = res b + g º res (b + g) となるので、(A7-13c) により a + g = b + g が得られます。
　また (A7-14k) の場合、pr a < pr b なら pr (a + g) < pr b º pr (b + g) なので (A7-13a) により a + g < b + g が得られます。
　また pr a = pr b かつ res a < res b なら pr (a + g) º pr a = pr b º pr (b + g) となりますが、更に | res a | , | res b | < n ですから、帰納法の仮定により res (a + g) º res a + g < res b + g º res (b + g) となるので、(A7-13a) により a + g < b + g が得られます。
　次の (A7-14l) は、s_ij :º a_i + b_j , t_ji :º b_j + a_i と置くと、(A7-14i) により s_j = t_ji となり、従って (A7-14a) により « s_ij » = « t_ji » となることに注意すれば、(A7-5) と (A7-14i) と (A7-14j) により a · b º « s₁₁ » + ¼ + « s_ij » + ¼ + « s_pq » = « t₁₁ » + ¼ + « t_ji » + ¼ + « t_qp » º b · a が得られます。
　次の (A7-14m) と (A7-14n) は、g が 0 なら (A7-6e) により明らかなので g は 0 でない場合を考えれば十分です。そこで、まず g = « g¢ » と書ける場合について、n :º max{ | a | , | b | } に関する帰納法により証明します。
　まず (A7-14j),(A7-14k) により a_i = a_i  Û  a_i + g¢ = a_j + g¢ , a_i < a_i  Û  a_i + g¢ < a_j + g¢ が成り立つので、単純積の定義から pr (a · g) º pr a + g¢ 及び res (a · g) º (res a) · g が成り立ち、b についても同様に pr (b · g) º pr b + g¢ 及び res (b · g) º (res b) · g が成り立ちます。
　ゆえに (A7-14j),(A7-14k) により pr a = pr b  Û  pr (a · g) = pr (b · g) 及び pr a < pr b  Û  pr (a · g) < pr (b · g) が成り立ちます。
　また | res a | , | res b | < n ですから、帰納法の仮定により res a = res b  Û  res (a · g) = res (b · g) 及び res a < res b  Û  res (a · g) < res (b · g) が成り立つので、(A7-13) によりこの場合は証明されました。
　一般の場合は、a < b と a = b と a > b が背反で、しかもこれらのいずれかが成り立つことから、(A7-14m) と (A7-14n) について、いずれも左から右が導けることを証明すれば十分ですが、g = « g₁ » + ¼ + « g_r » と書けることに注意すれば、(A7-6h),(A7-14i),(A7-14j),(A7-14k) を繰り返し適用することにより結論が得られます。
　次の (A7-14o) は、n , m , a , b がいずれも 0 でない場合は、(A7-8e)~(A7-8i) により、左辺の次元は max{ dim a , dim b } + k' 、右辺の次元は max{ dim a , dim b } + k ですから明らかです。他方、n · a + m · b = 0 の場合も明らかです。
　また n · a = 0 で m も b も 0 でない場合は、左辺の次元は dim b + k' で、右辺の次元は dim b + k 以上ですから明らかです。対称性により他の場合も明らかです。
　次の (A7-14p) は、dim a = 1 の場合は、a は 1 以上の自然数、従って左辺は自然数ですから n · a + m < w = w · 1 £ w · a となります。
　また dim a > 1 の場合は、m < a ですから n · a + m < n · a + a = (n + 1) · a < w · a となります。
　次の (A7-14q) の最初の式は、(A7-6a) により « a » + « b » = « a b » ですが、a < a + b かつ b < a + b ですから明らかです。
　後半の主張は、k に関する帰納法で « a »_k+1 + « b »_k+1 = « « a »_k » + « « b »_k » < « « a »_k + « b »_k » < « « a + b »_k » = « a + b »_k+1 となり、証明されました。
　次に (A7-14r) は、l :º k - k' と置けば、(A7-14a),(A7-14b) により、a' £ « a »_l  , b' £ « b »_l のとき a' + b' £ « a + b »_l が成り立つこと、及び l > 0 又は仮定の２つの £ のいずれかが < ならば、結論の £ も < にできることを示せば十分ですが、これは (A7-14k),(A7-14q) より明らかです。
　最後に (A7-14s) は、g :º « g₁ ¼ g_r » と置くと、b < g + « a » = « a » + g のとき a¢ < a と自然数 k が存在して b < g + k · « a¢ » = k · « a¢ » + g が成り立つことを示せばよいことに注意します。
　最初に g が 0 でない場合を n :º | b | に関する帰納法で証明しますが、この場合は条件により pr (« a » + g) º pr g , res (« a » + g) º « a » + res g が成り立つことに注意します。
　まず pr b < pr (« a » + g) が成り立つ場合は pr b < pr g なので、a¢ :º 0 と置くと（k は任意でよい）、pr b < pr g º pr (k · « a¢ » + g) となるのでこの場合は成り立ちます。
　また pr b = pr (« a » + g) かつ res b < res (« a » + g) が成り立つ場合は pr b = pr g かつ res b < « a » + res g となりますから、帰納法の仮定により a¢ < a と自然数 k が存在して res b < k · « a¢ » + res g が成り立ちますが、pr g º pr (k · « a¢ » + g) かつ k · « a¢ » + res g º res (k · « a¢ » + g) となるので、この場合も証明されました。
　最後に g º 0 の場合ですが、この場合は b < « a » のとき b < k · « a¢ » となる a¢ < a と自然数 k を見つければよいことになります。
　そこで、b :º « b₁ ¼ b_q » と表わしたとき、q が 0 なら a¢ :º 0 , k :º 1 と置けば明らかなので、q > 0 の場合を考えれば十分です。
　この場合、a¢ :º pr b と置くと、pr « a » º a , res « a » º 0 に注意すれば、a¢ < a となることがわかります。そこで、一般に b < (q + 1) · « a¢ » が成り立つことを q ³ 1 に関する帰納法により証明します。
　実際、pr b º a¢ º pr ((q + 1) · « a¢ ») であることと、帰納法の仮定（ただし q º 1 のときは res b º 0 であること）により res b < q · « a¢ » が成り立つことと、q · « a¢ » º res ((q + 1) · « a¢ ») から明らかです。

　さて、以上の準備のもとに、超限帰納法の証明に移ります。

　以下、a が順序数であることを ord a と表し、n が自然数であることを nat n と表し、一般にギリシャ小文字 a に対しては "a は "_ord a のことを意味し、ラテン小文字 n に対しては "n は "_nat n のことを意味することとします。
　さて、順序数 g = « g₁ ¼ g_r » が "i : g_i ³ a を満たすことを g ³³ a と表すことにします。特に任意の順序数 a に対して 0 ³³ a が成り立つことに注意します。この記法を用いると、(A7-14s) は

(A7-15)  ( g ³³ a > 0  Ù  b < g + « a » ) Þ $a' < a : $n : b < g + n · « a¢ »

と書くことができます。
　そこで順序数 a に対する性質 P(a) に対し、"b £ a : P(b) のことを P*(a) と略記し、"a ( ("b < a : P(b) ) Þ P(a) ) のことを [P] と略記すれば、

(A7-16)  [P] Þ [P*]

が成り立つことを証明しましょう。
　実際、[P] を仮定し、更に "b < a : P*(b) を仮定します。このとき明らかに、"b < a : P(b) ですから、仮定 [P] により P(a) が成り立ちますが、これは "b £ a : P(b) すなわち P*(a) を意味します。a は任意ですから [P*] が得られ、以上で (A7-16) は証明されました。

　次に、"g ³³ a : ( P*(g) Þ P*(g + « a ») ) のことを P ^#(a) と略記すると、

(A7-17)  [P] Þ [P #]

が成り立ちます。
　実際、[P] と "a' < a : P ^#(a¢ ) を仮定して P ^#(a) すなわち "g ³³ a : ( P*(g) Þ P*(g + « a ») ) を証明すれば十分です。ところが仮定と (A7-16) により [P*] が成り立つので、g ³³ a と P*(g) と b < g + « a » から P*(b) を導けば十分です。
　ここで (A7-15) を用いると、順序数 a' < a と自然数 n が存在して b < g + n · « a¢ » が成り立ちます。ここで仮定により P ^#(a¢ ) が成り立ちますが、任意の自然数 k に対して g + k · « a¢ » ³³ a¢ ですから、P*(g + k · « a¢ ») Þ P*(g + k · « a¢ » + « a¢ ») が成り立ちます。
　ゆえに、P*(g) と k に関する帰納法により P*(g + n · « a¢ ») が得られ、従って P*(b) が得られます。以上で (A7-17) は証明されました。

　この (A7-17) により、

(A7-18)  ( [P #] Þ P #*(a) )  Þ  ( [P] Þ P*(« a ») )

が証明できます。
　実際、[P ^#] Þ P ^#*(a) と [P] を仮定すると、まず (A7-17) により [P ^#] が得られます。従って仮定により P ^#*(a) が、従って特に P ^#(a) すなわち "g ³³ a : ( P(g) Þ P*(g + « a ») ) が成り立つので、特に g に 0 を代入すれば、P*(0) Þ P*(« a ») が成り立ちます。ところが P*(0) は [P] により自明に成り立つので P*(« a ») が得られ、以上により (A7-18) が成り立つことが証明されました。

　さて、[P] が成り立てば、(A7-16) により [P*] なので、明らかに P*(0) が成り立ちます。一方 0 は « 0 »₀ とも書けますから

(A7-19)0  [P] Þ P*(« 0 »0 )

が成り立つことがわかります。従って、(A7-19)₀ の Pに P ^# を代入すれば、a を « 0 »₀ としたときの (A7-18) の前半が成り立つので後半が成り立ち、« « 0 »₀ » は « 0 »₁ と書けますから

(A7-19)1  [P] Þ P*(« 0 »1 )

が成り立つことがわかります。従って、(A7-19)₁ の Pに P ^# を代入すれば、a を « 0 »₁ としたときの (A7-18) の前半が成り立つので後半が成り立ち、« « 0 »₁ » は « 0 »₂ と書けますから

(A7-19)2  [P] Þ P*(« 0 »2 )

が成り立つことがわかります。
　ゆえに、この論法を繰り返せば、P*(« 0 »₀ ) , P*(« 0 »₁ ) , P*(« 0 »₂ ) , P*(« 0 »₃ ) ,¼ が順次証明できることがわかります。

　さて、目の前に “ « ” と “ » ” によって具体的に構成された順序数 α が与えられているとします。このとき、dim α を (A7-7) によって具体的に計算することができ、その計算結果として得られる具体的な自然数を ν とすると、自然数に対する等式 dim α = ν が証明できます。ゆえに ν の次の自然数を μ と書くと、dim α < μ が証明でき、従って (A7-14f) により α < « 0 »_μ が証明できます。ところが P*(« 0 »_μ ) は証明可能ですから P(α) は証明可能であることがわかります。すなわち次のメタ定理が証明されました：

具体的に与えられた順序数に対する超限帰納法 　順序数 a に対する命題 P(a) が [P] 、すなわち "a ( ( "b < a : P(b) ) Þ P(a) ) を満たせば、具体的に与えられたどんな順序数 α に対しても P(α) が成り立つ。

　ここで「具体的に与えられた順序数 α に対して P(α) が成り立つ」という部分が本質的で、これを「"a : P(a) が成り立つ」に置き換えることはできません。なぜならそのためには、その前段で "n : P*(« 0 »_n ) が証明されている必要がありますが、この命題が証明可能であることと、P*(« 0 »₀ ) , P*(« 0 »₁ ) , P*(« 0 »₂ ) , P*(« 0 »₃ ) ,¼ がすべて証明可能であることとの間には、付録６で述べたGödelの不完全性定理の (G1) と (G2) の比較でもわかるように、大きなギャップがあるからです。
　事実、もしHeyting算術の範囲内で "n : P*(« 0 »_n ) が成り立つことが証明できたとすると、以下に述べる超限帰納法がHeyting算術において証明できてしまい、その結果、次節で示すようにHeyting算術自体の無矛盾性がHeyting算術で証明できてしまうので、これはGödelの第二不完全性定理に反してしまいます。
　すなわち、完全な形での超限帰納法を証明するためには、何らかの形で理論を拡大する必要があるのです。

　そこで、Heyting算術上の冪理論（本文第５節参照）を考え、この推論体系を広義の有限の立場とよぶことにします。このように構成主義数学の範疇で理論を拡大することにより、完全な形での超限帰納法が成り立つことを証明することができます：

超限帰納法 　広義の有限の立場においては、順序数 a に対する命題 P(a) が [P] 、すなわち "a ( ( "b < a : P(b) ) Þ P(a) ) を満たせば、"a : P(a) が成り立つ。

　実際、すべての順序数からなる集合を Ω と書き、a 未満の順序数全体からなる集合を Ω(a) と書き、a 以下の順序数全体からなる集合を Ω(a) と書くことにします。また、順序数からなる集合 A は、"a ( Ω(a) Ì A  Þ  aÎA ) であるとき超限帰納的であるといい、Trans A と書くことにします。
　aÎA のことを P(a) と書くと、Trans A は [P] と同値です。そこで A^# :º { a | P ^#(a) } と書けば、自明な事実である [P] Þ P*(0) と、(A7-17) と (A7-18) は、それぞれ次のように表すことができます：

(A7-20a)  Trans A  Þ  Ω(0) Ì A

(A7-20b)  Trans A  Þ  Trans A#

(A7-20c)  ( Trans A#  Þ  Ω(a) Ì A# )  Þ  ( Trans A  Þ  Ω(« a ») Ì A )

　これらの事実から、

(A7-21)  "A : "n ( Trans A  Þ  Ω(« 0 »n ) Ì A )

が成り立つことを証明しましょう。
　実際、命題 "A ( Trans A  Þ  Ω(« 0 »_n ) Ì A ) を n に関する帰納法で証明します。
　まず n が 0 のときは (A7-20a) により明らかです。
　また、n で成り立つと仮定すると、Trans A^# なら、帰納法の仮定の A に A^# を代入すれば、Ω(« 0 »_n ) Ì A^# が成り立つので、(A7-20c) の左辺の a に « 0 »_n を代入したものが成り立つので、(A7-20c) の右辺の a に « 0 »_n を代入したもの、すなわち Trans A  Þ  Ω(« « 0 »_n ») Ì A が成り立ちますが、これは Trans A  Þ  Ω(« 0 »_n+1 ) Ì A とも書けるので、帰納法が完成しました。
　ところで Trans A のとき、任意の順序数 a に対し、(A7-14f) により、a < « 0 »_n となる自然数 n が存在しますから、これと (A7-21) によって aÎA がわかり、従って A = Ω となることがわかります。
　従って、[P] を満たす命題 P(a) に対し、A :º { aÎΩ | P(a) } は超限帰納的な集合ですから、今示したことから A = Ω となり、確かに超限帰納法が成立することがわかります。