English version

前回は Peano がどうやって自然数を定義したかの話だった．λ計算でも実は同じ方法で自然数を定義するので Peano の話をしたのだ．形式化自体は証明を厳密にするということにかかわってくるので，数学者にはそちらの方が重要であるようだ．しかし，形式化によって厳密さが増した結果「数なんてもの位，わかるだろう，適当にやってくれよ」という部分がなくなる．あたりまえのようなことも全部定義されるからである．こうなるとその副作用で機械で作ることも可能になる．コンピュータを作ることができるのだ．私にとって形式化が面白いのはこの部分である．

実際どのように機械で作るのかはいろいろな方法がある．パスカルの計算機 Pascaline やCharles Babbageの differential engine のような歯車方式もあるだろう．ここでは Peano の定理に近いものを考えよう．

マービンに言われるまえに言っておくが，これは佐藤雅彦，桜井貴文両先生の「プログラムの基礎理論」にある方式，だったと思う．(本が皆実家にあるというのは不便なものだ．ところでこの文章は佐藤先生が最初に実装された SKK という入力方法で書いている．) 佐藤先生の授業はタフな授業である．聞いているだけでは，少なくとも私には，絶対にわからない．しかし，質問をするとどんなに馬鹿げていることでもわかるまで答えて下さる．ところが，あまりにタフな授業なので何を質問して良いのかがわからない．質問できるレベルまで予習をするのは大変であった．

まず，数であることを示す記号として丸を使う，そして Peano でいう 0 を四角で示すことにする．次の数は 0 を繰替えすことで示そう．Figure 1 を参照のこと．

ここでは 1 とか 2 は使っていない．というのも，定義ではそういうものがないからだ．現在の 1 とか 2 の記法は 10 進法に関係するのでそんなに本質ではない．ローマ数字のような方式でも数は示せるし，メソポタミアの方式や，漢字という手もある．これらは数そのものをより人間に便利になるようにしてあって，自然数そのものはこのように 0 と数字の区切りがあればで示せるのである．その0 も別に何語で書いても良いのでここでは四角を使う．

四角が一つだから1にしたいという考えもあると思う．それは確かにそうなのだが，0 を示すにも何か記号が必要だ．「0 は何もないことがある」ことを示す記号である．ここでは四角しかないのでこうなってしまった．ここでは数のようなものを作って，それを実際の数に map することになるので，どこからはじめるかはあまり問題ではない．自然数は 1 からはじめても良いし，42 からはじめても良いのだ．ただ直感的には Figure 1 方式では 1 からの方が良いとは私も思う．

また，本来0 だけで済むのに丸を導入した理由は次回に示そう．

チャーチ数