1+1=2 の証明をPythonで実装してみた

Swiftというプログラミング言語で数を構成するという非常に興味深い動画をみました。

4-1. 何もないところから数を作る - 2015/07/24

この動画がとてもとても面白くて触発されたので、N番煎じでしょうが、Pythonの練習(?)にと、同じようなことをPythonで実装してみました。

恥ずかしながらプログラミングに不慣れなため、いきなり全部はちょっと重いので、まずは自然数を構成して、ちゃんと 1+1=2 になることを確かめるというところまでやってみました。

なお、自然数の定義などの集合論の部分はwikipedia先生を最大限に活用いたしました。
集合論や数論には全く詳しくないので、突込み等ございましたら最大限優しくお願いいたします。

自然数の定義

とりあえず、まずはZFC公理系のもとで自然数を定義することを考えます。
以下、自然数には "0" も含めて考えるものとしています。

ペアノシステムと自然数の定義

---

集合 X、X のある要素 x、X から自分自身 X への写像f が下記の性質 1~3 (ペアノの公理)を満たすとき、組 (X,x,f) をペアノ系またはペアノシステムといい、集合 X を自然数といいます。
　1. x は f の値域にはない
　2. f は単射である
　3. もし X の部分集合 A が以下 (i) (ii) を満たすならば、 A = X である。
　　(i) x は A に含まれる
　　(ii) もし a が A に含まれるなら f(a) も A に含まれる

ーーー
つまり、X が自然数全体の集合、x が"0"、 f は"次の数"を決めることを表現しています。
条件1 は、 0 には "前の数" がないことを表していて、
条件2 は、ある数の "次の数" は必ず1つに定まることを表していて、
条件3 は、数学的帰納法の成立を表しています。

同型の定義

---

2つのペアノシステム (X,x,f), (Y,y,g) について、次のような性質 (i)～(iii) を満たす X から Y への写像 φ が存在するとき、(X,x,f), (Y,y,g) は同型であるといいます。
　(i) φは全単射
　(ii) φ(x) = y
　(iii) X の任意の元 a に対して φ(f(a)) = g(φ(a))

ーーー
同型となる2つのペアノシステム同士は同値であるというように同値関係を定めれば、ペアノシステム全体の集合をこの同値関係で割った商集合を考えることができます。
そして、次のことからこの商集合の一意性が言えます。

存在と一意性

---

上のように定義したペアノシステムは同型を除いて一意に定まります。(証明略)

自然数を構成する

Pythonを使って上のような性質を満たす自然数を構成してみます。
一般的な構成法である(らしい)、ジョン・フォン・ノイマンの構成法で構成します。

空集合 {} を "0(ゼロ)" として考えて、
1 := 0+ := 0 U {0},
2 := 1+ := 1 U {1},
3 := 2+ := 2 U {2},
…...
として新たな集合をどんどん作っていき、これらを全部集めた集合族を N とします。
また、写像 suc : N → N を suc(x) := x U {x} として定めます。
このようにつくった N は無限集合の公理によって存在が保証され、組(N, {}, suc) がペアノシステムとなることは簡単に証明できます。
つまり、自然数 1,2,3.... をそれぞれ 1:={0}, 2:={0, 1}, 3:={0, 1, 2} .... として順に作っているイメージです。
要するに、簡単に言うと、Pythonでは↓みたいに構成する感じになります。
(リストを集合と見立てて使っています)

### 手動で9まで構成してみる
>>> N = [""] * 10     ### 便宜的にリストを作る
>>> N
>>> [, , , , , , , , , ]
### 0 ～ 9 を順番に作る
>>> N[0] = []
>>> N[1] = [N[0]]
>>> N[2] = [N[0], N[1]]
>>> N[3] = [N[0], N[1], N[2]]
>>> N[4] = [N[0], N[1], N[2], N[3]]
>>> N[5] = [N[0], N[1], N[2], N[3], N[4]]
>>> N[6] = [N[0], N[1], N[2], N[3], N[4], N[5]]
>>> N[7] = [N[0], N[1], N[2], N[3], N[4], N[5], N[6]]
>>> N[8] = [N[0], N[1], N[2], N[3], N[4], N[5], N[6], N[7]]
>>> N[9] = [N[0], N[1], N[2], N[3], N[4], N[5], N[6], N[7], N[8]]
>>> N[3]    ### "3" がどんなの見てみる
[[], [[]], [[], [[]]]]

### 任意の数の自然数を構成する(Pythonの)関数を作る
def Num(x=10):
    if x == 0:
        return []
    elif x > 0:
        N = [""] * x
        N[0] = []
        for i in range(x-1):
            N[i+1] = [N[j] for j in range(i+1)]
        return N

>>> Num(3)    ### 動作確認
[[], [[]], [[], [[]]]]    ### ちゃんと"3" が作れている

本当は無限個の集合を作る必要がありますが、それは無理(?)なので一旦上のような感じで我慢します。

後者関数を作る

任意の自然数を引数として、その"後者(successor)"を返す写像を実装します。

>>> def suc(x):
    return [Num(i) for i in range(len(x)+1)]
>>> suc(Num(2))    ### 動作確認
>>> [[], [[]], [[], [[]]]]   ### "2" の後者がちゃんと "3" になっている

足し算を定義する

上のように構成した集合にはまだ演算がありません。
この集合の上に足し算を"ちゃんと"定義してみます。

足し算の定義

2つの自然数 N の直積 N×N から N への写像 add: N×N → N を、次の性質を満たすように定義します。
　(i) add(m, 0) = m
　(ii) add(m, suc(n)) = suc(a(m, n))
a, b ∈ N に対し、add(a, b) を "a + b" と表記し、この操作を足し算といいます。

要するに、与えられた自然数分の後者を繰り返しとる操作を足し算として定義しています。
Pythonで↓のように関数として実装します。

def add(x, y):
    y = len(y)
    while y > 0:
        x = suc(x)
        y -= 1
    return x

1+1=2 の証明

上のように構成した自然数と足し算において、 ちゃんと "1+1=2" になっていることを確認してみます。

>>> add(Num(1), Num(1)) == Num(2)
>>> True

きちんと 1+1=2 になっていることが確かめられました。
今後は、整数や有理数を構成したり、乗除法を実装してみたりしようかと思います。