Skip to content

Instantly share code, notes, and snippets.

@yingtai
Last active December 19, 2015 21:29
Show Gist options
  • Save yingtai/6020449 to your computer and use it in GitHub Desktop.
Save yingtai/6020449 to your computer and use it in GitHub Desktop.
ペアノの公理のとらえ方について cc/ @potetisensei

自然数の定義


ペアノの公理:

以下を満たすような集合 N の要素を自然数とする.

  1. O ∈ N
  1. 任意の x ∈ N について s(x) ∈ N このとき s(x) を x の後者と呼ぶ.
  1. s(x) ≠ O
  1. x ≠ y のとき, かつそのときのみ s(x) ≠ s(y)
  1. 集合 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 はメタレベルを説明したもの, とそれぞれ考えられる.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment