ゲーデルと20世紀の論理学(ロジック)〈1〉ゲーデルの20世紀

だいたい読み終わりました．だいたいというのは，最後の 7 ページ 「計算可能実数と計算可能(不)連続関数」のところが，解析学さっぱり人間の私にはちゃんとフォローできなかったという （苦笑）

vol.4 の集合論とプラトニズムは未だにさっぱり読めてないんですが，これは 20 世紀のロジックの歴史についての巻なので，それほどテクニカルな部分は無くて，私でも普通に読めました．

Lion's Book もそうなんですが，現在では正確無比なところまで磨き上げられた巨大システムである UNIX やロジックの体系なども，その初期は，いろんな人が悩んだり間違えたり誤解したり試行錯誤して作ってきた，人間が作ったものなんだなぁ，という感慨を得ることができる本です．

日本にゲーデルの業績が導入されてきたあたりの話など，昔は本当に海外の情報や論文を得るのは大変だったんだなぁ，偉大な先人たちがみんな頑張って日本に伝えたんだなぁ，今はインターネットとかで簡単に論文が見れる良い時代なんだから，もっと頑張らないといけないなぁ，とか，当たり前なんですけど現代では気づき難いことをいろいろ再確認させてくれます．

日本に集合論が入ってきたのは，だいたい 100 年前，ゲーデルが生まれた頃らしいです．最初は 「1909 （明治 42） 年林鶴一は当時わが国に流布していた微積分学の基礎が薄弱であることを憂い，ジョルダンの 『解析教程』 (1893, 94) の一部分を翻訳し出版した (p.39) 」とか．

ゲーデルがウィーン大学に入学したのが，関東大震災 (1923) の翌年．
東大安田講堂ができたのが 1925 年．
ゲーデルの不完全性定理の論文が出版されたのが 1931 年．
ほとんどタイムラグなく，日本には伝わってきていた模様．
そして同年 9 月に満州事変が勃発して，日本は長い戦争の時代へ．

この当時は，まだドイツ語で数学の論文を書くのがけっこう普通だったんですかねぇ．

その後もいろいろあって，途中，ゲーデルが死んだ年に 「カーニハンとリッチーの共著 『プログラミング言語 C (The C Programming Language』 が出版された (p.98)」 とか，さりげなくロジックからコンピュータの時代への変化が示唆されていたり．

そんなこんなで，日本のロジックの発展が読めるってのは，翻訳本じゃない書き下ろし本の醍醐味だと思いました．他の巻のテクニカルな内容は英語の本でも読めるので，ある意味この vol.1 が一番貴重な日本語の本とも言えるような気がします．

「数学基礎論」 という言葉を，ロジシャンはけっこう嫌ってるような印象を受けました．数学科に「基礎論」じゃなくて「ロジック」がある日本の大学はほとんどない (?) とか，ここらへんはけっこう日本遅れてるような感じみたいです．もはや数学の基礎付けという大義名分は薄れてきていて，ゲーデルによって形式主義の限界が明らかになった以上，有限の立場の意味もどんどん強力なものに変わってきているそうです．ゲンツェンが順序数ε_0 までの超限帰納法を使って PA の無矛盾性を証明したりとか．直観主義も，途中から構成的数学と名前を変え，やがてはアルゴリズムの研究からコンピュータの時代にシフトしていくという流れ．ダイアレクティカ解釈から，その 2 階版のジラールの 2 階の算術 (System F) への流れがハイライトみたいな感じになってます．この本がおススメらしい (本で示されてる URL は現在移動したみたいです)．

Proofs and Types

絶版みたいですけど，ウェブ上で全文 pdf などで読めます．

PA の論理式を，その構成的な部分集合である HA の論理式に変換するアルゴリズムと，意味の等価性をちゃんと与えて，制限された体系 HA の無矛盾性を証明するだけで，PA の無矛盾性も証明できるってのは，なんかプログラム変換の正当性の理論みたいでイカスと思いました．当然，排中律とかが無い HA で，PA の論理式をそのまま表現することは不可能なわけですけど，PA の論理式 A は証明できなくても，その二重否定 ¬¬ A は証明できる，ってことを利用してる (って理解で良いのかな ?) これは賢いなと思いました．ダイアレクティカ解釈すごい．

ちなみに，PA を 2 階に拡張した体系 ACA_0 では，実数の性質がかなり良いところまで議論できるらしい．

ヒルベルトのプログラム

素人考えでは，この調子でどんどん強力な形式体系を考えていけば，やがて 「普通の数学」 の範囲では困らない，十分な強力さを持った無矛盾な数学（の部分）体系が作れそうな気もする．あるいは途中で本質的な困難があるのだろうか ? 単に時間の問題で，あと 1000 年ぐらい逆数学の研究したら作れるのだろうか ?

「（現行の）フルセットの数学体系」 の無矛盾性を証明するためには，現在のフルセットの数学体系よりも強力な体系がいると思うんだけど，それってどういう体系なのだろうか ? という疑問や興味も沸く．

あるいはそれが圏論とか new foundation (?) とかなのだろうか ? 100 年ぐらいしたら，集合論は廃れてて，みんな圏論を学ぶようになってたりするのだろうか ?

途中で，「第 2 部 第 2 章人間と機械 2.1 不完全性と機械論 --- チューリングからペンローズまで」 とかで，AI の話題が出てきたりして，これもまた面白いです．よくありがちな，不完全性定理にまつわる誤解が明確に論破されてて痛快でした．

結論としては，そもそも 「心」 という概念を，機械 （という用語を聞いて，連想するクラスが個々の人ごとに異なるのが，そもそものすれ違いの原因だと思うのですが） という概念以外で説明することはできないのだから，人の心は機械よりも優れているとかいないとかいう議論自体がナンセンスなのではないか ? というあたりに落ち着いてる感じでした．

「人間の心」 っていうのもおかしな話で，そもそもその定義が怪しい．とりあえず 「神の心」 との対比として （有限の立場 vs 無限の真理） 「現実の機械」 と，チューリングマシンのような絶対に壊れないし間違えないし無限の能力を持つ 「理想の機械」 に対応します．

現実の機械と，神の心を対応させて比較したんじゃ，そもそも前提がおかしいですし．理想化された人間の心 （疲れないし，間違えないし，個体差が無い） ってのは，そもそも人間の心とはもはや呼べないんじゃないの ? という疑問も．

つまり，人間の心の方がコンピュータよりも優れてる，という信念を持ってる人は，無意識のうちに，制限された有限の能力の機械と，理想化された無限の人の心を対比しているんですよね．それじゃ，前提がおかしいのだから，人間の心の方が優れててあたりまえ，フェアじゃないよと．

一人の人間が一生の間に生成できる定理の数は有限で，人間の数も有限で，宇宙の長さも有限なのだから，全ての人間の心が生み出せる数学定理のクラスも有限です．

ならば，必ず対応する定理のクラスを生成できるチューリング･マシンが存在します．なので，人間とチューリングマシンは，人間を最大限に理想化したとしても同じ能力を持つ，ということができます．

まぁ，ペンローズ以外にも 「世界の究極理論は存在するか―多宇宙理論から見た生命、進化、時間 」 みたいな本もありますが．

この本の内容は 「全ての現実のコンピュータは，有限の制限された不完全な存在なので，チューリング不完全である．なのでチューリング等価ではない．すなわち，宇宙の物理学的構造 （超並列宇宙論） をもっとも効率的に利用できる計算機械が，一番高い計算能力を持つ．それが人間の脳である．なので，少なくとも現在の計算機は，人間の脳には追いつけない」 という主張だと理解しています．

まだ決着が付いてない，いろいろ面白いところですね．

最後の 「連続体上の計算可能性」 のところが，難しくてよくわからなかったけど面白かったです．

ヒルベルト･ゲーデルを乗り越えて発生し，しかも 19 世紀的アルゴリズムの世界でも受け入れられると想像され，さらに現場の数学者たちと共通の言語で語り合える，この基礎論の子孫について，ぜひ言及しておきたい．(p.204)

再帰的関数によって支配されるのだから，当然ながら計算可能実数は加算個しかない．それでもあたかも計算可能実数の集合が連続体をなすかのように，解析学がその上で展開されることは興味深い． (p.206)

なんとなく実数ってとらえどころが無くて，ロジシャンとかあんまり好きじゃないのかな，という偏見があったのですが，むしろ解析学 （いわゆる，『普通の数学』 の世界） の方までどんどんロジックの手法を拡張していくことを目指している研究者も多いみたい (?)

ロジックの進歩で，人類はようやく実数の正体がわかりかけてきているのかな ? と思いました．

ところで，自分は，数学者が書いた （インフォーマルな） 文章はわりとスラスラ読める気がするのですが，なぜか哲学者(?)寄りの人が書いた文章はなかなか頭に入ってこなくて苦労します．漢字が多いから ? (苦笑) あと，歴史のところも，あんまり年表的になってくると疲れますね… 読み飛ばしがちに．

---

えらく古い本 (1985) ですが，たまたま研究室に転がっていたので眺めていたら，けっこう面白かったのでメモ．

知識表現とPROLOG/KR

ET 言語の，D ルールの定義構文 (as *Head | *Body) とか，変数の頭に * （アスタリスク）が付くのとかも，Prolog/KR の as 構文 (assert の略らしい) なのかな ? Prolog/KR も変数の頭に * が付くのか，とか，こういう由来系の情報ってのは面白いです．

Prolog/KR ってのは Lisp と Prolog の融合を進めたような言語のようです．というか，Lisp で書かれた Prolog 処理系のようです．

知識表現の利便性のために拡張された Prolog であり，多重世界の概念でプログラムの階層化（モジュール化）を可能にするそう．特に，AI における知識フレームなどが，一世界一概念という形で素直に対応付けられるらしい．

Prolog/KR は，もともと Utilisp [Chikayama 1981] (日立，富士通のMシリーズ，IBM370 で動く)上に作製されたが，現在 Franzlisp (VAX Unix)，Maclisp (DEC-20)，Zetalisp (Lisp マシン) の版がある．Lisp マシン版は多重世界機構の拡張とともに Uranus と呼ばれている． (p.70)

あたりに，非常に時代を感じますが，本の内容自体は （非アカデミックの水準では ?） それほど古びてない感じですね．

多重世界機構とか，リストでプログラムが表現されている（メタ記述が容易）とか，パターンマッチング機能がある，自動バックトラッキング部分と，決定的な部分が分離されているのでユーザが任意のプログラミングスタイルを選択できる，などは，まんま ET 言語にもあてはまりますね．なるほど，かなり大きな影響を受けているようです．ET のワールド機構，D ルールと N ルールの区別，単一化とパターンマッチングの分離 （Prolog から，より純粋なルール型言語へ．高レベルから低レベルまでを柔軟に記述可能） などにそのまま対応します．

多重世界機構の応用例として，Smalltalk の持つクラス間の階層構造を，そのまま素直に多重世界の入れ子構造で表現して，Tiny Smalltalk の処理系を十数行で実装したりしたりとか，なかなか面白い本です．

ちょっと検索したみたら，こんな記述も．

100 年 Windows 横山哲也 2006年09月12日 渕一博氏を偲ぶ

Prologは，プログラム言語としてはかなり未完成であった。例えば，まともなプログラムを書くには，カットオペレータという演算子が必須である。ところが，カットオペレータの強力さと単純さはGOTO文の比ではなく，結果としてプログラムの見通しは極めて悪いものとなった。そこで，研究者の間では，述語論理型言語にどのような制御構造が必要かという考察が行われていたことを記憶している。私は，自分の研究に，中島秀之氏（現公立はこだて未来大学学長）の作成したProlog/KRを使うことにした。当時，オンライン・コミュニティはあまり発達しておらず，中島氏が所属していた東京大学まで電話をして磁気テープを送ってもらったことを覚えている。もちろんオープンリールである。

　Prolog/KRは，LispとPrologと融合した言語で，十分な制御構造が備わっていた。ただし，追加された制御構造は手続き型の側面が強く，述語論理の特徴を生かせていたとは言い切れない。ところで，どうでもいいことだが，1986年に広島で開催された情報処理学会全国大会で偶然中島氏をお見かけしたので，著書にサインをいただいた。今でも大事にとってある。

　一方，ICOTではPrologを拡張したGHC（Guarded Horn Clause）をベースに，KL-1を開発した。こちらは，述語論理の特徴を生かし，さらに並列処理まで実現していた。ただ，Prolog固有の構文が色濃く残っており，慣れないと使いこなすのは難しいだろう。

---

追記

Common Lisp 上で動く Prolog/KR 処理系が存在するようです．

Uranus Prolog/KR

---

かなり前に @m0h1can 氏が twitter でコホモロジーについて語っていたので興味を持ちました．

コホモロジーのこころ

カントールから今に至る現代数学の流れは、端的に言ってしまえば集合論からブルバキを通し、そして行き詰まり、関数もっと言うと機能に立ち返り圏論に辿り着いたのだな、と。 07:13 PM February 21, 2008

カントールが生きた時代は、彼の数学は圧倒的に異端だったので、非難も多くそれはそれで辛かったろうという事なんですが、しかしやはり数学の基礎ではなかった。

ヒルベルトプログラムを通して公理的集合論は当時の数学の屋台骨になり、ブルバキによってその上での再構築が行われた。

ブルバキが数学原論を執筆していくうちに、力尽き、あるいは限界が見え始めた。その思想を行き過ぎて突き抜けたグロタンディークやアイレンバーグは、ブルバキを捨てる必要性に達した。

集合を基礎とはせず、関数それも広いクラスでの函数、いわば機能としての構造を数学の基礎とする。その視点からスキーム論や圏論が萌芽して、今やコホモロジーという不可欠な対象を見出した。

高木貞治が解析概論の中で、函数はその一つ一つに与えられた能力がある、という事を言いましたが、そこが数学の土台だろうというわけです。

函数、それも純化した抽象的対象としての機能を考える必要がある。そのために自然変換を用いたい。そのために函手を導入し、射や対象を定義する必要が生まれた。

未だ教育的には扱いの低い圏論だけど、将来はもっと基礎的な概念として教育に組み入れられて行くんだろうな。少なくとも、集合論ではなくて。

とりあえず自然変換すばらしい。

機能としての構造とラムダ算法に同じ匂いを嗅ぐのは同感です。実際、スキーム論の計算なども、代数的に計算して出る答えが最後に何か具体的な対象と対応付けられるようなものだし。

プログラミング的な表現をすれば、アレしてコレしてこうなってという、副作用が積み重なるような古い数学ではなくて、ある代数があってその変換が自然に決まって、具体的な対象は計算の最後で好きに結び付ければ善いような

この本は，普通の数学の本みたいに，定義・定理・証明というスタイルではなく，自由な感じにすいすい進んで行く感じなんですが．いきなり新しい用語が導入され，しばらくしてから説明が入ったりする （ように私のレベルだと感じられる） ので，読んでいる最中にいちいち厳密性についてひっかかったりする感じです．なので，おそらくもう 1 冊ぐらい普通の教科書的な本と併読しつつ読み進める，そして「コホモロジーのこころ」を感じるというのが，良い読み方なのかな，と思いました．

私が多少わかるのは，集合論とか一階の述語論理とか帰納関数の理論とか，そこらへんの計算可能性とか情報数学に関わる部分だけなので，圏論の概念はなかなか慣れない感じがします．

しかし，その圏論的なスタイルというのは面白いなと感じました．まぁ，最初の 10 ページを読み進めるのに，何回読み返したかわからないぐらい苦労したのですが．

凖同型写像とかのところの，圏論独特の矢印を使った図で概念を説明していくところなどは，わかってくると頭の中の思考過程そのものを図式化したような感じがして，なかなか良い感じな気もします．確かに，定義を読むとき，こういう風に考えてるよなぁ，よくできてる，と．まぁ，まだ自然変換まで行って無いのですが…

それこそ具体例が少なく，出てきても高度な圏ばかりなので，檜山さんのはじめての圏論シリーズを最初に読んでおくと良いと思います．

あと，くるるさんが絶賛していた

ゲーデルと20世紀の論理学＜ロジック＞ Vol.4　集合論とプラトニズム

まだ全体的にパラパラとめくってみたレベルですが，これは素晴らしい本ですね．私のレベルだと全然ページが進みませんが…

最近の私の読書のスタイルは，寝床などに本を置いておいて，寝る前の睡眠導入剤代わりや，起きたときの眠気覚ましにダラダラ読むという感じで．一気に全部を通して読むのではなく，何度も何度も繰り返しつまみ食いして，一回本を開く度に，一口新しい概念を得ようとする，ような感じの読み方をしています．TaPL もそういう感じでずっとダラダラ読んでました．この本も，半年や一年，それ以上かけてじっくり読んで行く価値がある本だと思います．この 2 冊レベルの本が血肉になるためには，それこそ日常的に何度も本を開いて，少しずつ攻略していくというやり方が，私のような凡人には向いていると思いますし，結果的に何度も考える機会が増えて，概念と一緒に生活するようなことになるので，最終的に得られるものも大きくなるのではないかと感じています．

これからは証明を行うような論文をたくさん書いていかないといけないので，ここらへんのテクニックの習得が必要に迫られていたりもします．もっと若いときにちゃんと勉強しておけば良かったなぁと．いまさら苦労しつつ，楽しみながら日々勉強しています．

---

古本屋でなんとなく見つけて読んでいる．

対談中，The Catcher in the Rye を 「ライ麦畑の捕まえ手」 (p.104) と呼んでいたりして面白い．普通に直訳すると 「ライ麦畑の捕手」 なんだけど，これを 「でつかまえて」 と訳した野崎先生はすごいな．全然タイトルにでてこない，この部分だけで，西原理恵子の 「ガンジャ (大麻) 畑でつかまえて」 とか，いったいいくつパロディネタが作られたことか．他にも有名な Fuck you を 「オマ○コしよう」 と訳したりとか，いろいろ神懸ってる．

そんな神様みたいな定番野崎訳を乗り越える，とまでいかなくても，匹敵して併読されるレベルの訳まで持ち上げるために，村上春樹はこんだけ考えましたよ，という内容の本．

もしかしたら，過去にも一回新品で買って読んでるかもしれない．しかし，内容があまり記憶に無いので，たぶん 1 の方だったかも．

翻訳夜話2 サリンジャー戦記 (文春新書)，村上春樹・柴田元幸

僕は昔から，キャッチャーはそんなに好きじゃないし，全然共感もできなかったんだけど (単に困った青二才の中二病物語程度にしか思えなかった．フラニーとゾーイとかの方が好きだった)

最近はいろいろ進路に悩んだりしていて，いろいろ現実逃避の妄想をしていたりしていて (南の島で肉体労働して健康的に暮らしたい，とか．北国の人は，日光が非常に少なくなる冬場，多かれ少なかれ，季節性のうつっぽくなったりする)

これ読んでたら，それって，まんまホールデンだよなぁと，いまさら気付いた．16 歳のクソガキと発想のレベルが同じなのかと思うと，我ながらいろいろ情けない．

村上 じゃあ，苛立ちやうしろめたさを感じなくてすむように，自分でお金を稼ぐべくがんばればいいわけだけど，そのためにはまず既成システムの中に入っていかなくちゃいけない．一生懸命勉強して，名門大学に入って，良い職に就かなくてはならない．バスに乗って，マディソン・アベニューのオフィスに通わなくてはならない．

柴田 で，それはいやであると

村上 いやであると．かといって，お金がなくなるとどうしようもない．だから森のはずれに小屋を建てます．世の中を捨てます．だれとも口をききません，みたいなところに行ってしまう．この人の場合，中間段階ってのがないんですね． (p.136)

こうして身も蓋も無い文章にされてしまうと，とんでもなく痛い中二病だよなー (苦笑)

知識も経験も無いから，中間段階が無いっていうのが，若者に特有の発想．すぐ両極端に走る 「女なんて〜 だよ」「世の中なんて〜 ばかりさ」 とかが典型的なセリフ．

その両極端それぞれは，意外と正しかったりするんだけど，歳を重ねるにつれて，その間がつながってくる．落としどころが見付かってくる．みんなそうやって生きている．

自分の悩みなんて，60 年前の少年が抱えていたものと同じくらい普遍的でありふれたものなんだなぁと思うと，いろいろ面白い．これこそ時代を越えて生き残ってきた古典小説の強みだと思う．

---

字面だけ見ると 「ラブひな ！」 に響きが似てますが，超数学 (メタマセマティクス) のことです (ギャグがいちいち古い管理人)

メタマス! - オメガをめぐる数学の冒険

(via 最上の日々 10月22日（月）　▼ チャイティンの「 メタマス 」（白洋社）を読んでいるところ。)

ちなみに，現在わたしは風邪で寝込んでいて，寝床でちょっと読んでました．昨日も寝込んでたので，たまたま普段はみないテレビの NHK スペシャル，100年の難問はなぜ解けたのか〜天才数学者　失踪の謎〜 を見て，数学熱が再燃したというのもあります．

よりによってこんな変な時間に目が覚めてしまい，眠れなくなってしまったので，非常にぽわーんとした頭でこれを書いてます．日本語がおかしいかもしれない．

まだ本論 (本全体 300 ページ中，200 ページぐらい．残りは作者の論文が付録として 2 つ付いてる) の半分ぐらいしか読んでないんですが，メチャクチャ面白いです．いくら僕の駄文を連ねたところでこの面白さは伝わらないと思うので，もう買って読んでくださいとしか (最大級の賛辞) ひさしぶりに心が沸き立ち，知的興奮が得られるような本を読んだという気がした．

メタ数学ってのは，数学自体を数学の枠組で論じるという学問領域のことです．約 100 年前に，ラッセルのパラドクスを始めとした，たくさんのパラドクスが集合論という，これ以上ないほど根本的で確実に思われていた数学の内部に多数発見され，数学の確実性が大きく揺らいだことがその動機となってます （数学の危機）

内容的には，ゲーデルの不完全性定理とチューリングマシンの停止性問題のその後，それらの結果の真に意味することを 「プログラムサイズ計算量」 という観点からの定式化を試みるという，非常にエキサイティングな内容．メタ数学というタイトルですが，それほど数学数学理論理論した本では無く．ゲーデル・エッシャー・バッハもそうでしたが，著者はプログラミングや計算機科学にも明るいらしく (IBM で RISC プロセッサの設計やコンパイラの実装までやっていたそう)，LISP プログラムや，インタプリタという用語が説明無しに普通に出てきたりと，プログラマにとってはかなり馴染深い感じの内容になってます (数学者じゃなくて，普通に理論計算機科学者なのかな ?)．

普通は，ユークリッドの古典的かつエレガントな証明 (2000 年前) だけが紹介される 「素数が無限に存在する」 という命題なんですが，いきなりこの本では 3 つも証明が出てきます．オイラーの，ゼータ関数などの近代数学につながる極めて高度かつ技巧的な証明 (200 年前)，筆者による，計算量に基づいた証明 (20 年前)．ここで筆者は，ポール・エルデシュという偉大な数学者の信念 「ザ・ブック」 を否定しています．完璧な証明などというものは存在しない，数学の証明とは，小説や絵画など，他の芸術作品と同様に，数学者の精神の結晶であり，数学者の数だけ個性があるのだ，と．

まだ読み始めたばかりなので，あんまし深く理解はしてないんですが，確かに 「素数の数が有限ならば，素因数分解が (プログラムサイズ計算量的に) 簡単になりすぎる」 という観点の洞察は非常に鋭いなと思った．

著者は，不完全性定理は技巧的すぎて胡散臭い，単に表面的な事実を証明しただけで，その本当に意味するところまでの洞察は与えない，不満足なものだと長年感じていたようです．リチャード・ファインマンも言ってますが，真に概念を理解するためには，二つの全く異なった観点からの証明が大事なのです．ひとつしか証明が無いと，それが間違いだった場合には何も残りませんし，理解も浅いままで終わってしまうのです．ふたつの方向から山に登った経験があれば，その間もだいたい想像できるというのがあります．

チューリングの仕事により，多少は数学に潜む不完全性についての理解と，その必然性が明らかになりましたが，それでもまだ十分では無いと著者は考えました．

著者は，数学に潜むランダム性こそが，数学の不完全性をもたらしている根本要因だと考えました．真のランダム性に対しては，いかなる圧縮も無意味で，公理系によって全体を捉えることもできないので，それをそのまま見せるしかありません．完全な形式体系を構築できないのは，素数の性質を始めとした，数学のランダム性にある，と．

そして，ランダム性の定式化に，それを生成するためのプログラムのサイズという概念を用いたのが斬新だと思いました．よく構造化された問題を出力するプログラムは，非常に短くなります．しかし，完全にランダムな問題を出力するプログラムは，そのランダムな定数を単に埋め込んだだけのものになり，全く圧縮することが不可能となります．

わかりやすくいえば，shinh さんとか niha さんとかが狂ったように夢中になっている例のアレ，コードゴルフなんですね．もともとは tanakh さんあたりが火をつけて，yaneurao さんあたりが広めて，odzOzy さんが short coding って本を出したりもしてますが．

数学が，静的で絶対の確実性を持つ形式体系である，ということを証明する試み (ヒルベルトプログラム) は，ゲーデルによって完全に葬りさられました．

これは，数学は静的で完全な神の世界のものではなく，血肉が通った人間精神の構造化の産物である，ということを意味します．完全な形式体系は存在しないので，数学は常に拡張され，探究され続ける宿命にあります．

詳しくは本書を読んでもらうとして．

理解とは圧縮の度合であり，ランダム性と密接な関係があります．本質的にランダムな事象は，それ以上簡単な表現で圧縮できないという意味で，既約です．科学理論が意味を成すのは，なんらかの構造化されている概念を，より簡単な表現で圧縮できた場合．表現 (証明) が簡潔であればあるほど，圧縮の度合が大きい （よく理解されている）ということになります．

筆者は，LISP を例に上げ，科学理論 = プログラムとしています．科学理論の価値は，より簡潔で短いプログラムにより，膨大な数の具体的な事象を説明 (導出) できる点にあります．

ところで，プログラムが「エレガント」であること，すなわち，出力を生成する最小プログラムがあること，は証明できません (逆に，エレガントであることの証明不可能性から，チューリングの停止性問題が可解でないことがすぐにでます)．

だから人間は，常により短いプログラム (エレガントな理論，簡潔な数学の証明) を求めて日夜努力し続けるのだなぁと思いました．

要するに，遠く MIT 第一世代ハッカーの時代から始まり，いつの時代も常に優秀なプログラマがプログラムコードの圧縮に夢中になるのは，現在の最先端の理論計算機科学の一分野，アルゴリズム的情報理論の厳密な数学的理論から見ても合理的なんだなぁと (笑)

---