ペアノの公理:
以下を満たすような集合 N の要素を自然数とする.
- O ∈ N
- 任意の x ∈ N について s(x) ∈ N このとき s(x) を x の後者と呼ぶ.
- s(x) ≠ O
- x ≠ y のとき, かつそのときのみ s(x) ≠ s(y)
- 集合 S が O を含み, かつ x ∈ S ならば s(x) ∈ S のとき, N ⊆ S
(厳密性にあまり自信ないけど, とりあえず今回の説明のためにはこれで十分とする.)
ペアノの公理について考える前に「形式化」について明確にしておく.
コンピュータが行なっているのは, 普段われわれが行なっている――例えば 2+3=5 といった――計算をシミュレーションすること. (当たり前)
ここには2つのレベルがあって,
-
1つは人間の (別に公理を仮定したりしなくてもやっていける) 計算のレベル (意味のレベル, メタレベル),
-
もう1つはそれらをシミュレーションするレベル (形式レベル).
で, 1つ目のレベルの物事を2つ目で扱えるようにすることが「形式化」だといえる.
注意すべき点は, 形式レベルの対象はただの「文字列 (記号列)」にすぎないということ.
形式レベルで与えられるのはシンタックスのみであり, メタレベルの対象がこれにセマンティクス (意味論) を与える.
ペアノの公理に戻ると, O, s(O), ... は形式レベルの対象 (= シンタックス).
このとき, O の「意味」は 0, s(O) の「意味」は 1, ... と考えられる.
ここで 0 を意味する表現を O としたのは単に最初に混乱を避けるためで, 別に記号として "0" を採用しても本質的に同じである.
例えば 10 を意味する数 s(s(...s(O)) の略記として s^10(O) と書くことは別に問題ではない.
なぜなら, "s(s(...s(O))" なる文字列を受け取って, "s^10(0)" なる文字列を作るアルゴリズムが考えられるから. 要はシンタックスのみを考えればよいということ.
人間の(公理を前提として、表記も定められた)算術は使ってはいけないのではないか
という疑問はこれで解消するはず.
型なしラムダ計算の Church encoding においては, O が λsz.z, s(O) が λsz.sz, ... に変わるだけで, 同様に帰納的に定義できる.
ここでも, λsz.z の意味は 0, λsz.sz の意味は 1, ... とみなすことができる.
10 を表す数として s(s(...s(O)), あるいは s^10(O), また λsz.s(s(...s(z)...)) を採用するのは, その形式体系において 10 という数をシミュレーションするため.
「s^10(O) が 10 を意味する」というとき, 前に出てくる "10" は形式レベル, 後ろの 10 はメタレベルを説明したもの, とそれぞれ考えられる.