1+1=2を証明するためには1万ステップ以上かかるよ，という話

なんかすごいサイトを見つけてしまいました．

Metamath Proof Explorer Home Page

数学の基礎付けに関する 20 世紀の記念碑的偉業と称えられながらも，歴史上何人がこれまで読破したのか，と常にネタにされる Principia Mathematica （12 万円，2000 ページ！） に，1+1=2 の証明が載ってるっていうのはわりと有名な話だと思いますけど．

追記 : Radium Software Development 2006-06-30 : Proof that 1 + 1 = 2

# ちなみに，三巻組の大著の全文をオンラインで見ることができます．"From this proposition it will follow, when arithmetical addition has been defined, that 1+ 1= 2."．

このサイトでは，全ての定理が索引付けでハイパーリンクされていて，例の 1 + 1 = 2 の証明も，トップレベルから全てのサブ命題を追うことが可能になってます．

Theorem o1p1e2 4165

なんと 1518 個のサブ定理を 11086 ステップかけて証明する必要があるそう．

定理っていうのは，プログラムにおけるサブルーチンみたいなものなんですけど．
もし，途中の定理を全て「インライン展開」すると 10 億ステップを超えるとか．

---

ちなみに，us.metamath.org では，現代公理的集合論 ZFC (1+1=2 程度ならば，公理 C は必要ないみたいですが) を数学の基礎においているみたいですが，PM の初版では分岐階型理論 (theory of types)，2 版では単純階型理論 (simple theory of types) という定式化が採用されているそうです．

ラッセルの論理学は確かに時代後れである。ゲーデルその他の数理論理学者の批判をまつまでもなく、ラッセルの論理学が厳密さを欠いているということは、いまや周知の事実である。たとえば、『数学原理』には公理は与えられているが、推論法則を欠いている。したがって、やかましくいえば、『数学原理』において公理以外の定理を導出することは不可能である。また、初版において用いられている分岐階型理論においても、また、一九二五年に発表された第二版において採択された単純階型理論においても、その定式化は甚だしく厳密さを欠いている。そして、これらの理論が組合せ論理学の立場から正しく再構成されたのは比較的最近のことなのである。

(中略)

すでに述べたように、『数学原理』に内在するいろいろの技術的欠陥を現在の進んだ立場からあげつらうことはむづかしいことではない。しかし、理性の分析、あるいは、その再構成という仕事に哲学史上はじめて着手することによって、十九世紀的理性、あるいは、ドイツ観念論的理性と訣別して現代への第一歩を踏みだしたという点において、『数学原理』に代表されるラッセルの論理学の功績は永遠に残るであろう。したがって、『数学原理』が現代ヨーロッパにおげる最高の思想的所産であるというボヘンスキーの手放しの礼讃もけっして誇張ではあるまい。

ラッセルは哲学者で，メタ数学は 「数理哲学」 なんですよね．数学の道具を使って，人間知性を哲学している．

もう一つ引用．

バートランド・ラッセルのポータルサイト (著書解題４)ラッセル著『数理哲学序説』（中村秀吉・解題） 『ラッセル協会会報』n.４（1966年５月）pp.3-5.

ラッセルのこの方面で業績は、師のホワイトヘッドとの共著である大作『数学原理』に集大成されているといってよい。かれは1900年から1910年頃までの、かれの人生における最良の10年間をこの仕事の完成に惜しみなくささげたのである。しかしこの本は非常に大冊であるばかりか、かなり冗長な、ほとんど退屈な記号の羅列なので、実際に通読した人はほとんどないといっても過言ではあるまい。これを通読した人は一ダースしかいないだろうとか、ことによると、これを書いたラッセルとホワイトヘッドだけではなかろうか、などといううわさもたてられたほどである。しかしラッセル自身はここにとりあげる『数理哲学入門』において、ほとんど記号を使わないでその平易な解説を試みたのである。この『数理哲学入門』は、ラッセルが1918年５月から1919年９月まで（松下注：「1918年９月」の間違い）、反戦運動のかどで、獄につながれていた間に一気に書き上げたもの（注：獄中での執筆）である。われわれは彼の集中力にも驚くのであるが、同時に、いかほど自分がやったことの要約とはいえ、ほとんど参考書もない不便ななかで、これほど明晰かつ性格に『数学原理』の要点を叙述できたことに一驚を禁ぜざるえないのである。
本書ではまず数学のもっとも基本的概念である自然数列から問題が説き起こされ、自然数の定義が導入される。がんらい哲学では、自然数を何か感性的対象とふつうの一般者との両面をもったもの、ないしその中間者として、独自の対象と考えられてきた。一方、ペアノは自然数の公理系をつくるのに成功し、ある命題群を満足する勝手のものとして自然数を陰伏的に定義した。ラッセルはこの両方の考え方にあきたらず、個々の自然数を相似な、個物のクラスのクラスとして定義した。これによって個々の自然数は純粋に論理的な慨念であるクラスに還元されることになり、その把握に何か特殊な直感力のようなものを必要としなくなったのである。同時に、ペアノの公理とは違って現実的個物との関係もつき、一と他の関係のような哲学的アポリアにも一応の答を用意できることとなった。