5 年ぐらいぶりに新しい PC 買いました．あと，我が家で初めての Windows 機です．

ずっと，学会やゼミ，勉強会などのために，持ち運びがしやすい note PC が欲しかったのですが．

期待していた新型の EeePC も，高い重いデカいと散々な感じで，一時は MacBook の中古で良い出物があった (core 2 duo 2.0 GHz / Mem 2 G / 英語キーボード) ので，心が動きかけたのですが．やはり，白い note PC とか無いなと (あと，大きくて持ち運びしんどそうだし．Mac はハードの選択肢がほとんど無いのが…)．

そんなこんなでいろいろ悩んでいたところ，タイムリーなことに，先週の i-うぃん堂 の特価セールで，Thinkpad X61 と X61s が同じ値段で安売りされていました．夏の感謝セールとかで，送料が無料の上，8 万円以上のアウトレット品を買うと無料でメモリ 1 GB 増設キャンペーン (計 2 GB積まれる) とかもありーので，代引き手数料込みで 85430 円．

やはり Thinkpad は超カッコいい．これだよこれ，他の軽量モバイル note PC など全くに相手にならない．これは買うしか無いでしょう．

X61 と X61s のどちらにしようか迷ったのですが，

(1) 基本的に s の方が軽量化のため元値が高価 (231000 円 vs 168000 円)なのでお得 （まぁ，アウトレット品なので微妙なんですが）

(2) X61 の方は CPU クロックが上 (core 2 duo 2.2 GHz) なのは良いものの，発熱量が多そう (Matz さんが低温火傷という事例あり）．X61s は 1.4 GHz なので，クロックは下ではあるが，もともとモバイル note PC に速度など求めてないので，発熱量が低い方が良いに決まってる．

(3) X61 は Windows Vista が初期インストール (X61s は XP) だが，おそらくビデオチップがチップセット内臓で，メモリが 2 GB 程度で HDD も低速の X61 では使い物にならない

(4) X61s ならば重量も 1.3 kg 弱ぐらいなので，1 kg 弱ぐらいの UMPC と重さ自体はそれほど変わらない (X61 だと 1.43 g ぐらいで 500 g ぐらい違う)．

というわけで X61s に決定しました．X61 が X30 系列 （パワフルモバイル）で X61s が X40 系列 （スリムモバイル) らしいです．

僕は Thinkpad の X40 に強い憧れがあったのですが，その後継機種がこんなに安く手に入るとは．

防水キーボードでコーヒーがこぼれても大丈夫，「火事の炎にさらされ、消火ホースからの水を浴び、2階の窓から放り投げられ、さらに数昼夜の間ずぶ濡れになった家財道具の残骸にまみれ」ても全てのデータが無事だったなど，数々のレジェンドに彩られた愛すべき過剰品質，プロフェッショナル御用達の高級機種の代名詞だった Thinkpad．

それが中国企業 lenovo によりコモディティ化し，単なるイチ家電製品になってしまったということなのでしょうね．常に僕達の憧れだった，赤緑青に輝く IBM のロゴが消えてしまったのは悲しいですが，そのおかげで，僕のような貧乏学生の手にも届く価格帯にまで降りてきてくれたわけで，これはこれで大変素晴らしいことだと思います．

まだ今のところは IBM のチェックもしっかりしていて，生産体制にも以前と比べて大きな変化は無いようですし，X61 は評判がなかなか良い感じです．大事にしようと思います．

---

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

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年９月」の間違い）、反戦運動のかどで、獄につながれていた間に一気に書き上げたもの（注：獄中での執筆）である。われわれは彼の集中力にも驚くのであるが、同時に、いかほど自分がやったことの要約とはいえ、ほとんど参考書もない不便ななかで、これほど明晰かつ性格に『数学原理』の要点を叙述できたことに一驚を禁ぜざるえないのである。
本書ではまず数学のもっとも基本的概念である自然数列から問題が説き起こされ、自然数の定義が導入される。がんらい哲学では、自然数を何か感性的対象とふつうの一般者との両面をもったもの、ないしその中間者として、独自の対象と考えられてきた。一方、ペアノは自然数の公理系をつくるのに成功し、ある命題群を満足する勝手のものとして自然数を陰伏的に定義した。ラッセルはこの両方の考え方にあきたらず、個々の自然数を相似な、個物のクラスのクラスとして定義した。これによって個々の自然数は純粋に論理的な慨念であるクラスに還元されることになり、その把握に何か特殊な直感力のようなものを必要としなくなったのである。同時に、ペアノの公理とは違って現実的個物との関係もつき、一と他の関係のような哲学的アポリアにも一応の答を用意できることとなった。

---