数学の基礎

　本節では、自然数論において、加法と乗法が扱えれば、帰納的に定義されるすべての関数が扱えるという事実を解説します。

　等号 = の他に１変項述語 N 、定項 0 、１変項関数記号 s 、２変項関数記号 + 及び · を持ち、等号 = を持つ直観主義論理の推論規則 (LJ ) に加えて次の公理群：

(A5-1a)   ®  N(0)

(A5-1b)  N(x)  ®  N(x' )

(A5-1c)  N(x) , N( y)  ®  N(x + y)

(A5-1d)  N(x) , N( y)  ®  N(xy)

(A5-1e)  N(x) , x' = 0  ®

(A5-1f)  N(x) , x' = y'  ®  x = y

(A5-1g)  N(x)  ®  x + 0 = x

(A5-1h)  N(x) , N( y)  ®  x + y' = (x + y)'

(A5-1i)  N(x)  ®  0x = 0

(A5-1j)  N(x) , N( y)  ®  x' y = xy + y

及び帰納法とよばれる推論規則：

(A5-2)

A , N(x) , R(x)  ®  R(x' ) ———————————   ( x¢A )  A , N(T ) , R(0)  ®  R(T )

を持つ推論体系をHeyting算術とよびます。
　ただし、sx を x' と略記し、Ø x = y を x ¹ y と略記し、+xy を x + y と略記し、· xy を xy と略記し、"_N を " と略記し、$_N を $ と略記し、R(x) 等で任意の命題を表し、これの x に項 T を代入した命題を R(T ) と書き、x¢A は x が仮定 A に現れない変数であることを意味します。

　以下、変数はすべて N 項を表すものとすると、本文第10節 (10-25),(10-27),(10-30),(10-32) の証明がそのまま適用できて、

(A5-3a)  (x + y) + z = x + ( y + z)

(A5-3b)  0 + x = x

(A5-3c)  x' + y = (x + y)'

(A5-3d)  x + y = y + x

が得られます。(A5-3a) と (A5-3d) をそれぞれ加法に関する結合律及び交換律といいます。
　また、乗法についても本文第10節 (10-41)~(10-44),(10-49),(10-50) の証明がそのまま適用できて、

(A5-4a)  (x + y)z = xz + yz

(A5-4b)  1x = x

(A5-4c)  x0 = 0

(A5-4d)  x( y + z) = xy + xz

(A5-4e)   x( yz) = (xy)z

(A5-4f)  xy + x = xy'

(A5-4g)  xy = yx

が得られます。(A5-4a) を左分配律、(A5-4d) を右分配律、(A5-4e) を乗法に対する結合律、(A5-4g) を乗法の交換律といいます。

　次に、２項関係 < , > , £ , ³ を

(A5-5a)  x < y  :º  y > x  :º  $z : y = x + z'

(A5-5b)  x £ y  :º  y ³ x  :º  ( x < y  Ú  x = y )

で定義します。このとき、本文第11節 (11-1)~(11-23) の議論がそのまま使えて

(A5-6a)  x + y = 0  Þ  x = y = 0

(A5-6b)  x + z = y + z  Þ  x = y

(A5-6c)  xy = 0  Þ  ( x = 0  Ú  y = 0 )

(A5-6d)  xy = 1  Þ  x = y = 1

(A5-7a)  x < y   Ú   x = y   Ú   x > y

(A5-7b)  Ø ( x < y  Ù  x > y )

(A5-7c)  Ø x < x

(A5-7d)  x = y  Ú  Ø x = y

(A5-7e)  x < y  Ú  Ø x < y

(A5-7f)  ( x < y  Ù  y < z )  Þ  x < z

(A5-7g)  y < z  Û  x + y < x + z

(A5-7h)  x > 0  Þ  ( y < z  Û  xy < xz )

(A5-7i)  x > 0  Þ  ( y = z  Û  xy = xz )

(A5-8a)  x £ y  Ú  x > y

(A5-8b)  Ø ( x £ y  Ù  x > y )

(A5-8c)  ( x £ y  Ù  x ³ y )  Þ  x = y

(A5-8d)  x £ y  Ú  Ø x £ y

(A5-8e)  x £ y  Û  Ø y < x

(A5-8f)  x < y  Û  Ø y £ x

(A5-9)  x £ y  Û  ( y = x  Ú  $z : y = x + z' )  Û  $z : y = x + z

(A5-10a)  x ³ 0

(A5-10b)  x £ 0  Û  x = 0

(A5-10c)  x > 0  Û  Ø x = 0

(A5-10d)  x £ x

(A5-10e)  ( x £ y  Ù  y £ z )  Þ  x £ z

(A5-10f)  x £ y  Ú  x ³ y

(A5-10g)  ( x < y  Ù  y £ z )  Þ  x < z

(A5-10h)  ( x £ y  Ù  y < z )  Þ  x < z

(A5-10i)  x £ y  Û  x < y'

(A5-10j)  x' £ y  Û  x < y

(A5-10k)  y £ z  Û  x + y £ x + z

(A5-10l)  x > 0  Þ  ( y £ z  Û  xy £ xz )

が成り立つことがわかりますが、更に (A5-10i),(A5-5b),(A5-10i),(A5-10j) により

(A5-10m)  z < x'  Û  z £ x  Û  ( z < x  Ú  z = x )

(A5-10n)  z £ x'  Û  ( z < x'  Ú  z = x' )  Û  ( z £ x  Ú  z = x' )

(A5-10o)  z > x  Û  z ³ x'  Û  ( z > x'  Ú  z = x' )

が成り立ちます。なお、x < y  Ù  y £ z のことを x < y £ z と書くなどの省略記法を用いることがあります。
　また、本文第11節 (11-26)~(11-29) 及びその直後の注意により、任意の命題 P , Q に対して

(A5-11a)  ( "x (( "z < x : P(z) ) Þ P(x) )) Þ "x : P(x)

(A5-11b)  "z £ x : P(z)  Û  ( "z < x : P(z) )  Ù  P(x)

(A5-11c)  $z £ x : Q(z)  Û  ( $z < x : Q(z) )  Ú  Q(x)

(A5-11d)  ( "x : ( P(x)  Ú  Q(x) ))  Þ  (( "z < x : P(z) )  Ú  ( $z < x : Q(z) ))

(A5-11e)  ( "x : Ø ( P(x)  Ù  Q(x) ))  Þ  Ø (( "z < x : P(z) )  Ù  ( $z < x : Q(z) ))

(A5-11f)  ( "x : ( P(x)  Ú  Ø P(x) ))  Þ  (( "z < x : P(z) )  Ú  Ø ( "z < x : P(z) ))

(A5-11g)  ( "x : ( P(x)  Ú  Ø P(x) ))  Þ  (( $z < x : P(z) )  Ú  Ø ( $z < x : P(z) ))

が成り立つことがわかります。また、

(A5-12a)  Min(x, P)  :º  P(x)  Ù  "z : ( P(z)  Þ  z ³ x )

と置いて

(A5-12b)  (( $x : P(x) )  Ù  ( "x : ( P(x)  Ú  Ø P(x) )))  Þ  $x : Min(x, P)

を証明しましょう。
　そのためには、"x : ( P(x)  Ú  Ø P(x) ) を仮定して、$z < x : P(z)  Þ  $z : Min(z, P) を x に関する帰納法で証明すれば十分です。
　まず x が 0 なら仮定が偽なので明らかです。
　次に x のとき成り立つと仮定して、$z < x' : P(z) が成り立つと仮定します。(A5-10m) により $z < x : P(z) 又は P(x) が成り立ちます。
　一方、(A5-11d) で Q に P を、P に Ø P を代入すると、$z < x : P(x) 又は "z < x : Ø P(x) が成り立ちますが、前者なら帰納法の仮定により明らかで、後者なら $z < x : P(z) は成り立たないので P(x) が成り立ち、従って明らかに Min(x, P) が成り立ちます。以上で帰納法が完成しました。

　同様に、

(A5-13a)  Max(x, P)  :º  P(x)  Ù  "z : ( P(z)  Þ  z £ x )

と置いて

(A5-13b)  (( $x : P(x) )  Ù  ( $x : "z > x : Ø P(z) )  Ù  ( "x : ( P(x)  Ú  Ø P(x) )))  Þ  $x : Max(x, P)

を証明しましょう。
　そのためには、$x : P(x) と "x : ( P(x)  Ú  Ø P(x) ) を仮定して、"z > x : Ø P(z)  Þ  $z : Max(z, P) を x に関する帰納法で証明すれば十分です。
　まず x が 0 なら、Max(0, P) ですから明らかです。
　次に x のとき成り立つと仮定して、"z > x' : Ø P(z) が成り立つと仮定します。ところで仮定により P(x' ) 又は Ø P(x' ) ですが、前者なら明らかに Max(x', P) が成り立ち、後者なら (A5-10o) により "z > x : Ø P(z) が成り立つので、帰納法の仮定により明らかです。ゆえに帰納法が完成し、証明されました。

　さて、付録４の後半により、$!x : P(x) が成り立つ命題 P(x) に対して、理論を真に拡大することなく、ι量化記号を導入して、P(x) を満たす唯一つの x を表す ιxP(x) という記法を用いることが可能なので、以下の議論では、この ι量化記号を用いることにします。このとき

(A5-14)  Q(ιxP(x))  Û  "x ( P(x) Þ Q(x) )  Û  $x ( P(x) Ù Q(x) )

が成り立ちます。
　さて、明らかに、$x : Min(x, P) が成り立てば $!x : Min(x, P) が成り立つので、この場合

(A5-15a)  min{ x | P(x) } :º  ιxMin(x, P)

という省略記号を用いることにします。同様に、$x : Max(x, P) が成り立てば $!x : Max(x, P) が成り立つので、この場合

(A5-15b)  max{ x | P(x) } :º  ιxMax(x, P)

という省略記号を用います。
　特に、命題 x = a  Ú  x = b を P(x) と書けば、明らかに $x P(x) と "x > a + b : Ø P(x) が成り立ちますから、$x : Min(x, P) 及び $x : Max(x, P) の両条件が満たされます。そこで

(A5-16a)  min{a, b} :º  min{ x | x = a  Ú  x = b }

(A5-16a)  max{a, b} :º  max{ x | x = a  Ú  x = b }

と略記することにします。

　さて、本文第12節 (12-1) の証明をそのまま利用すると、

(A5-17a)  y > 0  Þ  $q : $r < y : x = qy + r

(A5-17b)  ( y > 0  Ù  x = py + r  Ù  x = qy + s )  Þ  ( p = q  Ù  r = s )

が得られますから、特に

(A5-18a)  y > 0├ $!q : $r < y : x = qy + r

(A5-18b)  y > 0├ $!r < y : $q : x = qy + r

が成り立つので

(A5-19a)  y > 0├  x/y  :º  ι q($r < y : x = qy + r)

(A5-19b)  y > 0├  rem(x, y)  :º  ι r(r < y  Ù  $q : x = qy + r)

と書くことにします。ただし、├ の左辺の条件が成り立っている場合のみ、右辺の省略記号が導入できることを意味します。また、

(A5-20)  y | x  :º  $q : x = yq

と定義すると、本文第12節 (12-7) 直後の議論がそのまま使えて、y | x に対して排中律が成り立つことがわかります。更に本文第12節 (12-8) の議論がそのまま使えて、

(A5-21a)  1 | x

(A5-21b)  x | x

(A5-21c)  ( x | y  Ù  y | z )  Þ  x | z

(A5-21d)  ( x | y  Ù  x | z )  Þ  x | ( y + z)

(A5-21e)  x | y  Þ  x | ( yz)

(A5-21f)  ( x | y  Ù  y > 0 )  Þ  x £ y

(A5-21g)  ( x | y  Ù  y | x )  Þ  x = y

が成り立ちます。
　さて、「z は x と y の公約数である」という関係を

(A5-22)  Cd(z, x, y)  :º  z | x  Ù  z | y

で定義すると、(A5-21a) により Cd(1, x, y) が成り立ち、更に x > 0  Ú  y > 0 ならば　(A5-21f) により "z > x + y : Ø Cd(z, x, y) が成り立ちます。従って上で示したように、$z : Max(z, Cd(z, x, y)) が成り立ちます。そこで

(A5-23)  x > 0  Ú  y > 0 ├  gcd{x, y} :º  ι z Max(z, Cd( · , x, y)) :º  max{ z |  z | x  Ù  z | y  }

と置けば、本文第12節 (12-11)~(12-15) の証明がそのまま使えて

(A5-24)  y > 0 , z = rem(x, y) ├  gcd( y, x) = gcd( y, z)

(A5-25)  x > 0 , g = gcd(x, y) ├  $u : $v : ux = vy + g

(A5-26)  x > 0 , gcd(x, y) = 1 ├  $u : $v : ux = vy + 1

(A5-27)  x > 0 , gcd(x, y) = 1 , x | ( yz) ├  x | z

(A5-28)  x > 0 , y > 0 , gcd(x, y) = 1 , x | z , y | z ├  (xy) | z

が成り立ちます。なお、gcd(x, y) = 1 のことを x と y は互いに素であるといいます。

　さて、x が素数であるということを Prim(x) と略記します：

(A5-29)  Prim(x)  :º  x > 1  Ù  "z £ x : ( z | x  Þ  ( z = 1  Ú  z = x ))

　この命題 Prim(x) に対しては明らかに排中律が成り立ちます：

(A5-30)  Prim(x)  Ú Ø Prim(x)

　更に、合成数は必ず素数を約数に持つことや、本文第12節 (12-17) の結果もそのまま成り立ちます：

(A5-31)  ( x > 1  Ù  Ø Prim(x) )  Þ  $z ( Prim(z)  Ù  z | x )

(A5-32)  ( Prim(z)  Ù  z | (xy) )  Þ  ( z | x  Ú  z | y )

　ゆえに (A5-30),(A5-31),(A5-21b) により

(A5-33)  x > 1  Þ  $z ( Prim(z)  Ù  z | x )

が成り立ちます。
　また、階乗に相当する自然数の存在も証明できます：

(A5-34)  $c > 0 : "k £ n : ( k > 0  Þ  k | c )

　実際、n に関する帰納法で証明することにし、まず n が 0 なら明らかです。
　また n で成り立つとし、そのような c を取ります。
　さて、k が 0 < k £ n' を満たせば、(A5-10n) により k £ n  Ú  k = n' ですが、k £ n ならば、帰納法の仮定により k | c が成り立ち、k = n' ならば (A5-21b) により k | n' です。ゆえに (A5-21e) により、いずれにせよ k | (cn' ) となり、帰納法が完成しました。

　そこで、c > 0  Ù  "k £ n : ( k > 0  Þ  k | c ) のことを Fact(n, c) と略記すれば、

(A5-35)  ( Fact(n, c)  Ù  k < l £ n )  Þ  gcd(k'c + 1, l'c + 1) = 1

が成り立つことを証明しましょう。
　実際、g = gcd(k'c + 1, l'c + 1) と置いて g > 1 と仮定します。このとき (A5-33) により、p | g となる素数 p が存在します。
　このとき l = k + m となる m > 0 を取れば、l' = k' + m なので l'c + 1 = k'c + 1 + mc となり、p | g と g | (l'c + 1) と g | (k'c + 1) と (A5-21c),(A5-21d) により p | (mc) となり、従って (A5-32) により p | m  Ú  p | c となります。
　ここで p | m なら (A5-21f) により p £ m £ l £ n となり、Fact(n, c) により p | c となるので、いずれにせよ p | c となり、従って Ø p | (k'c + 1) となりますが、p | (k'c + 1) だったのですから矛盾です。よって Ø g > 1 が得られ、明らかに g > 0 ですから g = 1 となり、(A5-35) は証明されました。

　次に

(A5-36)  Fact(n, c)  Þ  "k £ n : $g : "l £ n : (( l < k  Þ  (l'c + 1) | g )  Ù  ( l ³ k  Þ  gcd(l'c + 1, g) = 1 ))

が成り立つことを k に関する帰納法で証明しましょう。
　まず、k が 0 なら g を 1 とすれば成り立ちます。
　次に k について正しいとして "l £ n : (( l < k  Þ  (l'c + 1) | g )  Ù  ( l ³ k  Þ  gcd(l'c + 1, g) = 1 )) と仮定し、更に k' £ n と仮定します。
　このとき、仮定により "l £ k : (l'c + 1) | (g(k'c + 1)) となりますが、更に k < l £ n  Þ  gcd(l'c + 1, g(k'c + 1)) = 1 が成り立つことを証明しましょう。
　実際、k < l £ n と gcd(l'c + 1, g(k'c + 1)) > 1 を仮定すると、(A5-33) により素数 p が存在して p | (l'c + 1) かつ p | (g(k'c + 1)) となります。ゆえに (A5-32) により p | g  Ú  p | (k'c + 1) となりますが、帰納法の仮定と (A5-35) により、g も k'c + 1 も l'c + 1 と互いに素なので矛盾です。
　よって (A5-36) は、k を k' に、g を g(k'c + 1) に置き換えても成立し、帰納法が完成しました。

　さて、項 T(k) が与えられたとき、

(A5-37)  $a : $c : "k < n : ( T(k) £ l  Þ  rem(a, k'c + 1) = T(k) )

が成り立つことを n に対する帰納法で証明しましょう。
　まず n が 0 なら自明なので、n で正しいと仮定します。(A5-34) により

(A5-38)  Fact(l, c)

となる c > 0 が存在します。ここで k = n とした場合の (A5-36) を用いると、

(A5-39)  $g : (( k < n  Þ  (k'c + 1) | g )  Ù  gcd(n'c + 1, g) = 1 )

が成り立つので、そのような g を取ると、(A5-26) により

(A5-40)  $u : $v : ug = v(n'c + 1) + 1

となります。このとき p = rem(a, n'c + 1) と置くと、p < n'c + 1 なので、n'c + 1 + T(n) = p + q となる q を取ると、(A5-39) と帰納法の仮定により

(A5-41a)  k < n  Þ  rem(a + ugq, k'c + 1) = rem(a, k'c + 1) = T(k)

となり、また T(n) £ l なら (A5-38) により T(n) £ l £ c < n'c + 1 ですから、

(A5-41b)  rem(a + ugq, n'c + 1) = rem(a + vq(n'c + 1) + q, n'c + 1) = rem(a + q, n'c + 1) = rem( p + q, n'c + 1) = rem(n'c + 1 + T(n), n'c + 1) = T(n)

となるので、a を a + ugq に置き換えれば (A5-37) は n' でも成り立ち、帰納法が完成し、(A5-37) は証明されました。

　さて、(A5-37) において、仮定 T(k) £ l は実は落とすことができます。すなわち

(A5-42)  $a : $c : "k < n : rem(a, k'c + 1) = T(k)

が成り立ちます。これを n に関する帰納法で証明しましょう。
　まず n が 0 なら自明ですから、n で成り立つと仮定し、そのような a , c を取ると、k < n なら T(k) < k'c + 1 £ nc + 1 ですから、l = max{nc + 1, T(n)} と置けば、"k < n' : T(k) £ l が成り立ちますから、(A5-37) で n を n' に置き換えた式から $b : $d : "k < n' : rem(b, k'd + 1) = T(k) が得られるので帰納法が完成し、(A5-42) は証明されました。

　上の (A5-42) に出てくる項 rem(a, k'c + 1) は、自然数の有限列の替わりになるものです。これを用いてHeyting算術では帰納的に定義された任意の関数を扱うことができます。すなわち、項 S(x) と T(x, y) が任意に与えられたとき、

(A5-43a)  F(0) = S

(A5-43b)  F(x' ) = T(x, F(x))

を満たす項 F(x) を具体的に構成することができます。このことを証明するために、まず

(A5-44)  "n : $a : $c : ( rem(a, c + 1) = S  Ù  "k < n : rem(a, k"c + 1) = T(k, rem(a, k'c + 1)) )

が成り立つことを n に関する帰納法で証明します。
　まず n が 0 の場合は、rem(S, S + 1) = S が成り立ちますから、a と c を共に S と置けばよいことがわかります。
　次に n で成り立つと仮定して、(A5-44) を満たす a , c を取り、

(A5-45)  A(k, x)  :º  ( k £ n  Þ  x = rem(a, k'c + 1) )  Ù  ( k > n  Þ  x = T(n', rem(a, n"c + 1)) )

と置けば、明らかに $!x A(k, x) が成り立ちます。ゆえに記法 ι xA(k, x) が使えるので、(A5-42) により

(A5-46)  "k £ n' : rem(b, k'd + 1) = ι xA(k, x)

を満たす b , d するので、(A5-45) により

(A5-47a)  "k £ n : rem(b, k'd + 1) = rem(a, k'c + 1)

(A5-47b)  rem(b, n"d + 1) = T(n, rem(a, n'c + 1))

が成り立ちます。ゆえに (A5-47a) で k を 0 として、(A5-44) の帰納法の仮定を用いれば、

(A5-48a)  rem(b, d + 1) = rem(a, c + 1) = S

　また、k < n のとき、k' £ n ですから、(A5-47a) と、(A5-44) の帰納法の仮定により

(A5-48b)  rem(b, k"d + 1) = rem(a, k"c + 1) = T(k, rem(a, k'c + 1)) = T(k, rem(b, k'd + 1))

　また (A5-47b) と、(A5-47a) で k に n を代入したものにより

(A5-48c)  rem(b, n"d + 1) = T(n, rem(a, n'c + 1)) = T(n, rem(b, n'd + 1))

　ゆえに (A5-48b),(A5-48c) を併せると、

(A5-48d)  k < n' : rem(b, k"d + 1) = T(k, rem(b, k'd + 1))

となりますが、(A5-48a),(A5-48d) の組は、(A5-44) の n に n' を代入したものが成り立つことを示しており、(A5-44) の帰納法が完成しました。

　さて、

(A5-49)  B(n, a, c)  :º  rem(a, c + 1) = S  Ù  "k < n : rem(a, k"c + 1) = T(k, rem(a, k'c + 1))

と置くと、(A5-44) は

(A5-50)  "n : $a : $c : B(n, a, c)

が成り立つことを意味しますが、更に

(A5-51a)  ( k £ n  Ù  B(n, a, c) )  Þ  B(k, a, c)

(A5-51b)  ( B(n, a, c)  Ù  B(n, b, d ) )  Þ  "k £ n : rem(a, k'c + 1) = rem(b, k'd + 1)

が成り立ちます。実際、(A5-51a) は明らかですから (A5-51b) を k に対する帰納法で証明します。
　まず k が 0 のときは、B(n, a, c) と B(n, b, d) それぞれの前半部分により

(A5-52a)  rem(a, c + 1) = S = rem(b, d + 1)

となるので明らかです。
　次に k で成り立つと仮定し、更に k' £ n とすると、k < n ですから、B(n, a, c) と B(n, b, d) それぞれの後半部分と帰納法の仮定により

(A5-52b)  rem(a, k"c + 1) = T(k, rem(a, k'c + 1)) = T(k, rem(b, k'd + 1)) = rem(b, k"d + 1)

となって帰納法が完成し、(A5-51) は証明されました。

　さて、最後に

(A5-53)  R(x, y)  :º  $a : $c : ( B( y, a, c)  Ù  x = rem(a, y'c + 1) )

と置き、これが

(A5-54)  $!x R(x, y)

を満たすことを証明しましょう。
　まず (A5-50) により $x R(x, y) が成り立つことは明らかです。
　更に、R(x, y) と R(z, y) を仮定し、B( y, a, c)  Ù  x = rem(a, y'c + 1) となる a , c と、B( y, b, d)  Ù  z = rem(b, y'd + 1) となる b , d を取ると、(A5-51b) により x = z が得られ、以上で (A5-54) は証明されました。
　ゆえに

(A5-55)  F( y)  :º  ι xR(x, y)

と置くことができますが、あとはこれが (A5-43) を満たすことを示せば十分です。
　定義 (A5-49) と (A5-55) により

(A5-56a)  B(n, a, c)  Þ  S = rem(a, c + 1)

(A5-56b)  B(n, a, c)  Þ  F(n) = rem(a, n'c + 1)

ですから、特に n を 0 と置いて (A5-50) を満たす a , c を取れば、(A5-56) の右辺同士は一致するので、まず (A5-43a) が得られます。
　また、定義 (A5-49) で特に n を n' に置き換え、k に n を代入すれば

(A5-57)  B(n', a, c)  Þ  rem(a, n"c + 1) = T(n, rem(a, n'c + 1))

が得られ、(A5-56b) の n に n' を代入すれば

(A5-58)  B(n', a, c)  Þ  F(n' ) = rem(a, n"c + 1)

が得られます。ゆえに (A5-50) により B(n', a, c) となる a , c を取れば、(A5-51) により B(n, a, c) となるので、(A5-56b),(A5-57),(A5-58) により (A5-43b) が得られます。
　以上で (A5-43) を満たす項 F(n) が構成できました。

　すなわち、Heyting算術では関数記号として加法と乗法しか用意されていないにもかかわらず、帰納的に定義される任意の関数が扱えます。
　その実例として、まず１変項関数 pd を

(A5-59a)  pd 0 :º 0

(A5-59b)  pd a' :º a

で定義し、２変項関数 - を

(A5-60a)  a - 0 :º a

(A5-60b)  a - b' :º pd(a - b)

で定義します。このとき

(A5-61a)  pd a = a - 1

(A5-61b)  (a + b) - b = a

(A5-61c)  a - (a + b) = 0

(A5-61d)  a ³ b  Û  (a - b) + b = a

(A5-61e)  a £ b  Û  a - b = 0

(A5-61f)  a > b  Û  a - b > 0

が成り立ちます。
　実際、(A5-61a) は (A5-60b) で b を 0 とすれば (A5-60a) により明らかです。
　次に (A5-61b) は、b が 0 のときは (a + 0) - 0 = a - 0 = a なので成り立ちます。
　また、"b : (a + b) - b = a を仮定すると、a + b' = a' + b ですから (a + b' ) - b' = pd((a' + b) - b) = pd a' = a となって帰納法が完成します。
　次に (A5-61c) は、b が 0 のときは、(A5-61b) により a - (a + 0) = (0 + a) - a = 0 なので成り立ちます。
　また、a - (a + b) = 0 を仮定すると、a - (a + b' ) = a - (a + b)' = pd(a - (a + b)) = pd 0 = 0 となって帰納法が完成します。
　また (A5-61d) は、a ³ b Þ $c : a = b + c Þ $c : (a - b) + b = ((c + b) - b) + b = c + b = a Þ (a - b) + b = a Þ $d : a = d + b Þ a ³ b により明らかです。
　最後に (A5-61e) と (A5-61f) は、まず a £ b Þ $c : b = a + c Þ a - b = a - (a + c) = 0 と a > b Þ $c : a = b + c' Þ a - b = (b + c' ) - b = c' > 0 により左辺から右辺が言え、右辺から左辺は互いの対偶から導かれます。

　また、２個の自然数の冪を

(A5-62a)  a0 :º 1

(A5-62b)  an' :º an a

で定義します。このとき、本文第10節 (10-34) 以降の議論がすべて適用できて、

(A5-63a)  a1 = a

(A5-63b)  1n = 1

(A5-63c)  am+n = am · an

(A5-63d)  (a · b)n = an · bn

(A5-63e)  (am )n = an m

が成り立つことがわかります。

　また、一般の２項演算 * と項 T(i) に対して

(A5-64a)  *i £ 0 T(i) :º T(0)

(A5-64b)  *i £ k' T(i) º ( åi £ k T(i)) * T(k' )

と定義します。ただし、２項演算が加法 + のときは + のかわりに記号 å を用いてこれを有限和とよび、２項演算が乗法 · のときは · のかわりに記号 Õ を用いてこれを有限積とよびます。
　なお、*_{i £ k} T(i) のことを T(0) * T(1) * ¼ * T(k) と書くこともあります。

　次に、一般に省略記号として導入した１変項関数記号 j に対して、その k 回合成関数 j^(k) を

(A5-65a)  j(0)(x) :º x

(A5-65b)  j(k' )(x) :º j(j(k)(x))

で定義します。

　また、排中律を満たす命題 P(i) に対し、i £ k の範囲で P(i) を満たす i があればその中で最大のもの、なければ 0 を表す max{ i £ k | P(i) } を

(A5-66a)  max{ i £ 0 | P(i) } :º 0

(A5-66b)  max{ i £ k' | P (i) } :º ι x [ ( P(k' )  Ù  x = k' ) Ú ( ( Ø P (k' ) )  Ù  x = max{ i £ k | P(i) } ) ]

で定義し、これを用いて

(A5-67a)  min{ i £ k | P(i) } :º max{ i £ k | "j < i : Ø P( j) }

と定義します。(A5-66) を用いると、商 n / k と、割り切るという関係 k | n を

(A5-68)  n / k = max{ i £ n  |  ik £ n }

(A5-69)  k | n  Û  (n / k)k = n

と表わすことができます。

　さて、(A5-42) によれば、自然数からなる任意の有限列を、２個の自然数の組を用いてHeyting算術で扱うことができるのでした。そこで、更に強く、正整数からなる長さ１以上の有限列を１個の正整数と１対１に対応づける関数を構成してみましょう。

　まず、関数 s と t を

(A5-70)  s(n) :º max{ i £ n  |  2i | n } + 1

(A5-71)  t(n) :º n / 2s(n)

で定義します。帰納法により 2ⁱ ³ i が成り立つことがわかるので、(A5-70) の右辺第１項は確かに 2ⁱ が n を割り切るような最大の i を表わしていることに注意します。そこで更に

(A5-72)  n[i] :º s(t( pd i )(n))

(A5-73)  | n | :º min{ i £ n | t(i)(n) = 0 }

(A5-74)  n # k :º 2k n + 2pd k

と定義します。このとき s(n) ³ 1 ですから、(A5-71) により n ³ 1 である限り t(n) < n です。従って、(A5-73) で定義される | n | は確かに t⁽ⁱ⁾(n) = 0 となる最小の i になっています。そこで

(A5-75)  n ³ 1  Þ  n = t(n) # n[1]

が成り立つことを証明しましょう。
　実際、k :º max{ i £ n  |  2ⁱ | n } と置けば、s(n) = k' かつ n = 2^kl と書け、l は 2 で割れない、すなわち奇数ですから l = 2i + 1 と書けます。
　ゆえに t(n) = n / 2^s(n) = 2^k(2i + 1) / 2^k' = (2i + 1) / 2 = i となります。
　一方、(A5-72) により n[1] = s(n) = k' ですから t(n) # n[1] = i # k' = 2^k'i + 2^k = 2^k (2i + 1) = 2^kl = n となって証明されました。
　また、(A5-72) により m[1] = s(m) ですから t^(k)(n)[1] = s(t^(k)(n)) = n[k' ] となることと、(A5-73) による t^(k)(n) ³ 1  Û  k < | n | により、(A5-75) の n に t^(k)(n) を代入すれば、

(A5-76)  k < | n |  Þ  t(k)(n) = t(k' )(n) # n[k' ]

が得られ、従って t^(|n|)(n) = 0 と t⁽⁰⁾(n) = n に注意すれば、これらを順次入れ子にすることにより

(A5-77)  n ³ 1  Þ  n = 0 # n[| n |] # ¼ # n[2] # n[1]

が成り立つことがわかります。また、k ³ 1 のとき n # k = 2^{pd k}(2n + 1) に注意すれば、

(A5-78a)  k ³ 1  Þ  s(n # k) = max{ i £ n # k  |  2i | n # k } + 1 = pd k + 1 = k

(A5-78b)  k ³ 1  Þ  t(n # k) = (n # k) / 2k = n

が成り立ちます。そこで、任意に与えられた項 T(i) に対して

(A5-79)  n :º 0 # T(k) # ¼ # T(2) # T(1)

と置くと、帰納法により

(A5-80a)  i < k  Þ  t(i)(n) = 0 # T(k) # ¼ # T(i + 2) # T(i + 1)

(A5-80b)  t(k)(n) = 0

(A5-80c)  1 £ i £ k  Þ  n[i] = s(t(pd i)(n)) = T(i)

が成り立ち、これは、正整数からなる任意の長さ k ³ 1 を持つ任意の有限列 T(1) , T(2) ,¼, T(k) が、一個の正整数 n により一意的に表わされることを意味しています。

　そこで更に、正整数 n を長さ | n | の正整数の有限列とみなしたときの第 i 番目から第 j 番目まで（ただし 1 £ i £ j £ | n | ）を切り出して得られる有限列に対応する正整数 n[ j : i] と、正整数 m と n を正整数の有限列とみなしたときにそれらを繋げて得られる有限列に対応する正整数 m * n と、正整数 k 一個からなる有限列に対応する正整数 { k } を

(A5-81)  n[ j : i] :º 0 # n[ j] # ¼ # n[i + 1] # n[i]

(A5-82)  m * n :º m # n[| n |] # ¼ # n[2] # n[1]

(A5-83)  { k } :º 0 # k º 2pd k

で定義します。このとき明らかに

(A5-84a)  n ³ 1  Þ  n[| n | : 1] = n

(A5-84b)  n ³ 1 , 1 £ i £ | n |  Þ  n[i : i] = 0 # n[i] = { n[i] }

(A5-84c)  m, n ³ 1  Þ  m * n = 0 # m[| m |] # ¼ # m[2] # m[1] # n[| n |] # ¼ # n[2] # n[1]

(A5-84d)  m, n ³ 1  Þ  | m * n | = | m | + | n |

(A5-84e)  m, n ³ 1 , 1 £ i £ | n |  Þ  (m * n)[i] = n[i]

(A5-84f)  m, n ³ 1 , 1 £ j £ | m |  Þ  (m * n)[| n | + j] = m[ j]

が成り立ちます。更に、正整数 k に対して、(A5-78) により s({ k }) = s(0 # k) = k , t({ k }) = t(0 # k) = 0 となるので、(A5-73),(A5-72) により

(A5-85a)  k ³ 1  Þ  | { k } | = 1

(A5-85b)  k ³ 1  Þ  { k }[1] = s({ k }) = k

　ゆえに

(A5-86a)  k ³ 1  Þ  n * { k } = n # { k }[1] = n # k

(A5-86b)  n ³ 1  Þ  n = 0 # n[| n |] # ¼ # n[2] # n[1] = { n[| n |] } * ¼ * { n[2] } * { n[1] }

が成り立つことがわかります。

　さて、このような正整数の有限列を一つの正整数で表現する方法を用いると、関数の帰納的定義において、F(k) を 0 £ i < k に対するすべての F(i) を用いて定義するような関数を構成することができます。すなわち、まず F(0) :º S とし、| n | = k' であるような正整数 n が

(A5-87)  F(i) = pd (n[k' - i])       (  0 £ i £ k  )

の対応によって F の 0 から k までの値を表わしているとき F(k' ) :º T(k', n) と定義したいとします。この場合、帰納的定義：

(A5-88a)  G(0) = { S' }

(A5-88b)  G(x' ) = G(x) # T(x, G(x))'

によって項 G(x) をまず構築し、

(A5-89)  F(k) :º pd s(G(k))

と置けば、これが求めるものです。実際、まず (A5-88a) と (A5-85b) により

(A5-90a)  F(0) = pd s(G(0)) = pd s({ S' }) = pd S' = S

となります。また、帰納法により | G(k) | = k' であり、(A5-88b) と (A5-78a) により

(A5-90b)  F(k' ) = pd s(G(k' )) = pd s(G(k) # T(k, G(k))' ) = pd T(k, G(k))' = T(k, G(k))

となるので、これと (A5-88b) から G(k' ) = G(k) # F(k' )' となることがわかり、これと (A5-88a) と (A5-83) と (A5-90a) により

(A5-91)  G(k) = { S' } # F(1)' # ¼ # F(k)' = 0 # S' # F(1)' # ¼ # F(k)' = 0 # F(0)' # F(1)' # ¼ # F(k)'

となり、従って

(A5-92)  F(i) = pd (G(k)[k' - i])       (  0 £ i £ k  )

が成り立っているので (A5-87) の要件を満たしていることがわかり、これと (A5-90) により、(A5-89) で定義される項 F は確かに求めるものになっていることがわかります。

　さて、(A5-87) の関係式は、0 £ i £ k であるような i に対して定義された関数 F(i) を

(A5-93)  n = 0 # F(0)' # F(1)' # ¼ # F(k)'

の関係により | n | = k' であるような正整数 n で表現していると考えることができます。ここで F の値が取り得る範囲が 0 以上 l 以下の場合、この範囲で定義された関数 G に対応する正整数：

(A5-94)  m = 0 # G(0)' # G(1)' # ¼ # G(l )'

との間の合成関数を考えることができますが、その合成関数に対応する正整数を m _° n と書くことにします：

(A5-95)  m ° n :º 0 # G(F(0))' # G(F(1))' # ¼ # G(F(k))'

　もちろんこの右辺を m と n を用いて陽に表現することもできます。すなわち右辺の各要素を、(A5-87) と、F を G に、n を m にそれぞれ置き換えた式を使って得られる

(A5-96)  G(F(i)) = G(pd (n[k' - i])) = pd (m[l' - pd (n[k' - i])])

によって置き換えればよいわけです。
　更に、F の取り得る範囲の l が k 以下の場合は、(A5-65) の定義による関数 F の r 回合成関数 F^(r) を考えることができるので、この r 回合成関数に対応する正整数 n^(r) を

(A5-97a)  n(0) :º 0 # 0¢ # 1¢ # ¼ # k'

(A5-97b)  n(r' ) :º n ° n(r)

で定義することができます。