「1+1=2」に至る道 [趣味の数学]

先の「『プリンキピア・マテマティカ』を読む (0)」において、「1+1=2」であることの証明の「示唆」は『プリンキピア・マテマティカ』第1巻の379ページ目でなされると言ったが、これはじっさいどれほどの手数がかかっているものなのであろうか？

もちろん、それなりにでかい版型の本の379ページ目ということだけで「けっこうな手数」がかかっているであろうことは直感的に感得できると思われるが、もう少し厳密に追求するために、Metamath programで「1+1=2」の「素」になる定理*54.43の「手数」を調べてみよう。すると、この定理を証明するのにトータルで（つまり、この定理の証明に用いられるサブ定理も証明した場合）10766ステップかかることが分かる（ちなみに、Metamath programの教えるところによれば、この証明を完全に、つまり、ひとつの省略もせずに展開した場合、その手数は10億ステップを越える、とのこと）。では、じっさいに「1+1=2」を証明すると、どうなるか？　これも*54.43と同様にカウントしてみると、意外なことに（？）トータルでかかる手数は11831とのことで、*54.43とは1000ステップちょいしか違わない。なるほど、これはたしかに*54.43は「1+1=2」の「素」と言ってもいいかもしれない……。

というか、いずれにせよ、1万ステップを越える道のりをこれからちまちま歩んでゆくのかと思うと、おそろしいような、たのしいような。