2010年8月2日月曜日

数学基礎論ノート

謝辞とおことわり

今回の記事は勉強のためにまとめたノートを備忘のためにブログ記事として編集したもので、自分がオリジナルに発想した内容ではなく大部分は他の方の仕事を引用するかなぞるかしたものです。特に野崎昭弘『不完全性定理ー数学的体系のあゆみ』、林晋/八杉満利子『ゲーデル 不完全性定理』の両著作を広範に参考にしました。野崎さん、林さん、八杉さんのすばらしい仕事に感謝します。もしも引用しすぎであればご指摘ください、対応します。また、特に私の数学への理解が浅いために間違いや勘違いがあると思いますが、もちろんすべて私の責任であることをおことわりしておきます。(河野弘毅)

集合論以前の数学

19世紀なかばまでの数学はシンプルで、図形をあつかう幾何学と数をあつかう算術の二つから構成されていた。当時の数学は、数や方程式などあらかじめ与えられた数学的対象の性質を研究する営みだった。日本で高校までに習う数学もおおむねこの範囲内に設定されている。方法としては、ユークリッドの『原論』以来、最初にいくつかの公理を置きそこから定理を証明する「公理系」の体系が確立していた。

ところが1870年前後になって、幾何学の領域では非ユークリッド幾何学の正当性が異論の余地なく立証され、直観的裏付けをともなわない公理系をどう取り扱うべきかが新たな課題となった。算術の領域では実数の連続性の概念的探究に端を発するカントールの無限集合論が登場し、それがもたらすパラドクシカルな定理の数々は数学者をとまどわせた。

カントールの無限集合論が数学者をとまどわせたのは、それがパラドックスをはらむ危険性をもちながらも、その優れた表現力によって多くの数学者にとってとても魅力ある道具であったためらしい。

公理系と集合論の組み合わせが現代数学の基本

公理系というのは数学者にとって便利な道具で、ある公理系について定理Aが成立することを証明できれば、その公理系が適用できるすべての対象(モデル)においてその定理Aが成立することを証明なしに利用できる。各モデルごとに証明を行なうよりもはるかに効率がよい。

よい公理系はいろいろな対象に共通する「構造」を上手にとりだしているはずで、一般性のある公理系で証明できることがらは「構造的な事実」ともいえる。それまで個別的に知られていた諸事実を抽象化・一般化・構造化して述べてみると、非常に見通しがよくてわかりやすくなる。

ただし新しい公理系を構築するにはそれを表現できる道具がなければならない。その道具を提供するのが集合論だった。数学的対象には数・関数・関数の集合などいくつもの段階があるが、集合論を使えばすべての段階において集合による統一的な記法で定義が可能である(数学的概念は例外なく集合論の記法で記述できる)。

集合論以降は問題にしている数学的な現象をよく反映するような「構造」を積極的に記号論理によって定義し、その構造を持つ集合について何がいえるかを調べる、という考え方が優勢になった。この「一般的・統一的な理論を可能にするために公理系を構築する」考え方は「公理主義」ないし「数学的構造主義」と呼ばれ、現代数学の根本思想とみなされている。とくに20世紀に入ってからの抽象代数学や位相空間論では様々な新しい数学的対象が集合の道具立てを用いて積極的に構成され、研究された。

パラドックスという問題

ところが集合論にはパラドックスという問題があった。いったん公理系にパラドックスが生じてしまうと、その公理系を使って積み重ねた業績(証明)がぜんぶ見直しになってしまう(ときにはゴミになってしまう)ので数学者にとってパラドックスは悪夢である。集合論には次のようなパラドックスが生じることが分かっていた。

「すべてのものの集合Sを定義したとき、どんな集合Xが与えられてもそれより大きい集合Yが存在するという定理と矛盾する」(カントールのパラドックス)

「自分自身を要素として含まないような集合」を全部集めた集合をRとする。定義より任意の集合Xについて「XがRの要素である ⇔ XがXの要素でない」。このXにR自身を代入すると「RがRの要素である ⇔ RがRの要素でない」となり矛盾する」(ここで⇔は理論的同値、すなわち真偽一致を示す記号)(ラッセルのパラドックス)

これらのパラドックスはラッセルの「タイプ理論」によって一応回避されたが、ラッセルの証明は論理学的には若干強引だったようで、「それで数学は絶対に安全確実といえるだろうか?さらに新しいパラドックスが現れて数学の基礎をゆるがすのではないか?」という数学者の不安はおさまらなかったらしい。

集合論の記法はすばらしく強力なのでぜひ使いたい。だが、パラドックスは怖いのでうまく抑えこみたい。そういう需要が数学基礎論を推進する原動力となった。20世紀初頭の数学界のリーダーだったヒルベルトの言葉「カントールが創造してくれた楽園から我々を追放することなど、誰にもできはしない」(野崎2006, p.93)には、集合論を安全な道具に育て上げようという意気込みがよく現れている。

フレーゲの提案

ここで次にラッセルによる論理主義の立場を説明するほうが流れとしては分かりやすいが、ラッセルに行く前にフレーゲの仕事を紹介する。最大の理由はせっかくフレーゲについても調べたので一言紹介したいから(笑)だが、ラッセルに先んじて論理学による数学の基礎づけという画期的アイディアを提出したにもかかわらず世間的に満足な評価をうけられなかったフレーゲの鎮魂に供したいという気持ちも少しある。

1974年にイェーナ大学の私講師となった若きフレーゲ(1848-1925)は、そのような時代状況に対して「算術を論理学の一部とみなし、算術の概念や定理を論理学に基礎付ける」という野心的プランを抱く。(この構想は、数学基礎論において「論理主義」の立場と呼ばれる)。

アリストテレス以来の伝統的論理学やブールの論理学を適当に改訂するだけでは自分の目的が達成できないことが分かっていたフレーゲは、デビュー作の『概念記法』(1879)において、まったく独自に「算術の式言語を模造した純粋な思考のための式言語」(飯田2007, p.135)を作り上げた。概念記法を用いると、従来別建てで研究されてきた三段論法(伝統的論理学)と推論(命題論理学)が統合できるだけでなく、さらにそれ以上の命題を(全称量化子と存在量化子を用いて)表現できる。時代に先行しすぎた『概念記法』の評価は惨憺たるものであったが、フレーゲは自らのプランをコツコツと推し進め、算術定理の導出を概念記法を使って隙間のない推論連鎖として提示した『算術の基本法則』を苦労して自費出版する(1903年)。

だが、フレーゲが創案した『概念記法』は結局数学界には普及せず、同じアイディアを別の論理記号(ペアノの論理記号)を使って展開したラッセルとホワイトヘッドの仕事が普及した。

論理主義の立場

話を戻す。「集合論で構成した公理系の楽園で、パラドックスに脅かされずに安心して遊びたい」という数学者の夢を実現するために数学を確固たる基盤に基礎づけようとする研究、それが「数学基礎論」であり、数学基礎論には「論理主義」「直観主義」「形式主義」の三つの立場があるというのがどの教科書にも書いている定説である。以下、順番に紹介する。

まず「論理主義」、代表はラッセルだと言われる。論理主義は一言でいうと「最も信頼できるのは論理だから論理を基礎としてその上に数学を建設すればよい」という考え方で、それを実際にやってみせたのがラッセルとホワイトヘッドの共著『プリンキピア・マテマティカ』(1910-1913)である。ちなみに共著といっても死ぬほど面倒な記号論理への展開はすべてホワイトヘッドに押しつけてラッセルはおいしいトコだけ持っていったのではないか?という疑惑を個人的には持っている。

論理主義の難点は、本来は数学の問題である無限集合を論理学に帰着させようとして論理学としては不自然で技巧的な複数の公理(=無限公理、選択公理、還元公理)を仮定せざるを得なかった(恣意的になってしまった)点にある。数学のすべてを論理学に帰着させるのは明らかに無理があるだろう、というのが一般的評価らしい。

ちなみにラッセルは「論理学は数学の青年時代であり、数学は論理学の壮年時代である」という有名な言葉を遺している。

直観主義の立場

次に「直観主義」、提唱者はブラウワー(しばしばブローエルとも表記される)。「直観的理解の裏付けのない論理は信用できない」と主張した。ある概念の存在を証明するのに、その概念が存在しないと仮定して矛盾を導き「だから存在する」と結論する「非構成的存在証明」を禁じ手にせよと主張した(この禁じ手を公理として表現すると「排中律の禁止」になる)。

ブラウワーによる非構成的存在証明の排除に猛烈に反対したのがヒルベルトである。当時ヒルベルトはすでに非構成的存在証明を用いて学界で大きな業績を残していたので、ブラウワーの主張はとうてい受け入れ難いものだった。ブラウワーとヒルベルトは1920年代に激しく論争を展開するようになる。ヒルベルトの一番弟子だったワイルがブラウワーの味方に転じた(ヒルベルトからみれば愛弟子に裏切られた?)という感情的な背景も論争を激化させる一因だったらしい。

直観主義の難点は、たしかに直観は重要だが素朴な直観に密着したままですべての数学を建設するのは不可能であって既存の数学の大部分が破壊されかねない点にある。いくら確実でも数学的に生産性悪すぎる、というのが一般的評価らしい。

形式主義の立場

ブラウワーを批判したヒルベルト自身はどういう立場だったのか?ヒルベルトの立場こそ「形式主義」と呼ばれ、(後述するようにゲーデルの発見で挫折することにはなるが)数学基礎論の一応の勝者と呼ばれる立場である。

ラッセル(論理主義)とブラウワー(直観主義)は「自分の体系は現状でも安全」との立場だったが、ヒルベルトはそもそも数学で安全な立場を確保するためには証明をもっと「きちんと」した方法に鍛えあげる必要があると考えていたらしい。彼は証明の構造自体を数学的な問題としてとりあげようと考えた。言い換えれば、公理化・体系化・形式化を徹底することで数学の安全性を数学的に証明しようとした。無謀を承知で、私なりの理解でその方法を以下に紹介する。

そもそも証明とは「公理系」をもとに「推論規則」を適用して公理を導く操作だが、ヒルベルトに言わせると従来の証明は穴だらけであったらしい。論理学の厳密な視点から従来の証明を読み直すと、必要な公理が省略されていたり、暗黙の前提として証明もなしに公理を使っているケースが多い。特に「等号の公理系」や、もっと基本的な論理の法則(恒真文)が省略されている。

そこで、証明にいつのまにかパラドックスが入り込む危険を予防するために「基本的な恒真文と基本的な正しい推論のパターンをいくつか選び、それだけを論理的基礎として証明を推進する。」という方針を徹底することにした。

ヒルベルトは実際に『幾何学基礎論』でユークリッド幾何学を公理的に再構成(編み換え)してみせて、自分の考える「形式化」の方法を例示してみせた。だが、幾何学以外の分野については証明の中で用いられる自然言語の曖昧さをどのように克服すればよいか、その手段が19世紀末にはまだ発明されておらず、ヒルベルトの「形式主義」の理念を徹底して展開することができなかった。このためもあってか、20世紀初頭にヒルベルトはいったん数学基礎論の研究を中断し、しばらくは物理学の基礎づけに没頭してアインシュタインとの間で有名な学説の先陣争いをやったりしている。

その中断期間に出版されたラッセルの『プリンキピア・マテマティカ』が、中断前のヒルベルトには欠けていた洗練された論理学的道具を提供してくれたらしい。ヒルベルトは『マテマティカ』を「数学の基礎つけ計画のための予定調和」だとさえ呼んだ。(林八杉2006 p.189)

新しい洗練された道具を得て、ヒルベルトが到達した(「形式主義」の)数学の基礎づけ方法は次のとおり。

1. 研究の対象を公理系によって記述された数学の形式的体系に限定する。
2. 「無矛盾性」と「完全性(=可解性)」の基準を満たす公理系だけを使う。

この方法にそって「安全な数学」を展開するための方針、それが「ヒルベルト・プログラム」である。

ヒルベルト・プログラム

(林八杉2006 p.84より引用)

第1段階:「ヒルベルトのテーゼの基礎付け」現実の数学を形式系というコピーに写し取る。以後、数学の実体は忘れ、このコピーを数学本体とみなす。

第2段階:「無矛盾性の証明」形式系の無矛盾性、つまり、どの命題もそれ自身とその否定が同時にその体系内で証明されることがない、ということを示す。これにより、自己矛盾することがないという意味で、数学の絶対的安全性が保証される。

第3段階:「完全性の証明」形式系の完全性、つまり、「どの命題についてもそれ自身かその否定のどちらかがその形式系で証明できる」といことを示す。これにより、数学の問題は常に解決できることが判り、その意味で数学が完全無欠であることが示される。

ゲーデルの登場

ヒルベルトによる数学の基礎づけ理論=「証明論」は「20世紀の新数理論理学の助けを得て洗練化された公理論」(林八杉2006)だった。ヒルベルトのアプローチは数学者の支持を得た。ブラウワーが事実上の敗北宣言をヒルベルトに提出したこともあって、ヒルベルト・プログラムの達成も近いと思われたときに、ウィーンの無名の青年が物語に劇的な展開をもたらす。

その青年、ゲーデルは数学基礎論(ヒルベルトプログラム)の主要研究グループから見れば周辺的なウィーン大学出身の青年数学者だった。ゲーデルは最初ヒルベルトプログラムの参画者としてスタートし、プログラムを推進すべく第2段階を実数論の形式系の場合に実行しようとしていたが、その課程で図らずもヒルベルトプログラムの第2段階および第3段階が実行不可能であることを発見した(林八杉2006 p.86)。つまり数学基礎論に関与してすぐにそれを終わらせてしまった。

以下、林八杉2006によるとゲーデルの不完全性定理の要点は以下のとおり。

1. (定理Ⅵ 第一不完全性定理)数学の形式系、つまり、形式系と呼ばれる論理学の人工言語で記述された「数学」は、その表現力が十分豊かならば、完全かつ無矛盾であることはない。

その意味⇒「ある数学が内部矛盾していないならばその数学には解答のない問題がある」

2. (定理Ⅺ 第二不完全性定理)数学の形式系の表現力が十分豊かならば、その形式系が無矛盾であるという事実は、(その事実が本当である限り)その形式系自身の中では証明できない。

その意味⇒「数学は絶対的に確かな知識のように思われがちだがそう保証する術はない」

これらの命題はつまり、ヒルベルトが「ヒルベルト・プログラム」で目指したような無矛盾で完全な形式系は実現できない、つまり「数学の絶対的な基礎付けは不可能である」ということを示した。

ゲーデル以後の展開

そういうわけでヒルベルトが夢見た「無矛盾にして完全な形式系」は幻に終わった。しかし、ヒルベルトのパラダイムはそれで終わったわけでない。それどころか、私の理解ではヒルベルトのパラダイムこそが現代の数学の基本思想になっているようだ。そのあたりの詳しい雰囲気に興味のある方は、林八杉2006の第6章「不完全性定理のその後」をぜひお読みください。

林八杉2006によると、ゲーデルが不完全性定理を証明した後でも、大部分の数学者はそれに脅かされる心配を意外にしていない。自分が依拠している公理系に問題が生じれば確かにそれまでの仕事がムダになる危険があるが、そのときは安全な別の公理系をまたみつければよい。集合論の公理系は確かに現代数学の共通基盤であるが、絶対基盤というわけではない。ゲーデルにより絶対基盤という存在はありえないことを知っているから。だけど、そのことを承知したうえで、数学的アイディアを交換するためのプラットフォームとしての共通基盤の必要性は誰でも理解できる。そしてその共通基盤を使ってアイディアを交流するときの方法として、厳密性を担保できる形式的な公理主義が有効なこともよく分かっている。どうやらそういうフィーリングらしい。

そう考えると、現代数学を築いた先人として、ヒルベルトとゲーデルの二人がどれほど偉大であったか、素人にも分かるような気がした。

(付録)ゲーデルの不完全性定理

(引用者注:林八杉2006, p.15-16より引用。翻訳は林晋・八杉満利子。『ゲーデル不完全性定理』岩波文庫は原著論文の完全な翻訳を含む。林晋・八杉両氏の充実した解説は、数学基礎論、数理論理学、不完全性定理に関心がある人にとって興味の尽きない内容であると思う。一読をお勧めします。)


プリンキピア・マテマティカおよび関連した体系の形式的に決定不能な命題についてⅠ

クルト・ゲーデル(ウィーン)1931

数学は一層の厳密性を目指して進化し、周知のように、その大部分を形式化するにいたった。すなわち、僅かな機械的規則によって証明が実行できるような数学の形式化が達成されたのである。
現在までに構築された形式系のうち、もっとも包括的なものは、一方ではプリンキピア・マテマティカの体系(以下、PM)であり、他方では、ツェルメロ-フレンケルの集合論の公理系である(後者はJ. フォン・ノイマンが更に発展させている)。
これらの二つの体系は十分に完成されたものであり、今日数学において使用されるすべての証明法が、それらの内部で形式化されるほどである。つまり、それらの証明法が少数の公理と推理規則に還元されるのである。したがって、これらの体系の内部で形式的に表すことのできるすべての数学的問題を決定するためには、その公理と推論規則で十分である、と予想するのは自然なことである。
しかし、以下において示すように、事実はこれに反する。それどころか、普通の整数の理論における比較的単純な問題でありながら、これら両体系の公理から決定することができないようなものさえ存在する。この情況はこれらの体系に特有のことではなく、非常に広い範疇の形式系に対して成り立つ。特に前述の二つの体系に有限個の公理を追加してできた体系は、“その公理の追加によって、脚注4(下記参照)で述べた形の命題のうち偽なものが証明可能になることはない”という条件が成り立つ限り、すべてこの範疇に属すことになる。
詳細に立ち入るまえに、まず、証明の基本思想を概説する。(以下5ページにわたって証明の基本思想を概説した後、約40ページにわたって厳密な証明が記載されている)(翻訳は林晋・八杉満利子)

脚注4:すなわち、より正確に言えば、論理定数〜(でない)、∨(または)、(x)(すべての)、=(等しい)からできており、自然数に関する+(和)と・(積)以外にはどんな概念もでてこないような、決定不能な命題が存在するということである。ただし、接頭辞(x)も、自然数についてのみ参照するものとする。

参考文献

野崎昭弘(2006)『不完全性定理ー数学的体系のあゆみ』ちくま学芸文庫
林晋/八杉満利子 訳と解説(2006)ゲーデル『不完全性定理』岩波文庫
飯田隆責任編集(2007)『哲学の歴史11』中央公論新社

数学基礎論年表

1874 カントール 無限集合に濃度の差があることを発見
1879 フレーゲ 小冊子『概念記法』を出版
1893 フレーゲ 『算術の基本法則』第1巻出版
1899 ヒルベルト 『幾何学基礎論』出版
1900 ヒルベルト パリ公演(「ヒルベルト問題」の発表)
1901 ラッセル 「ラッセルのパラドックス」を発見(フレーゲに連絡)
1903 ラッセル 『数学の原理』出版
1904 ヒルベルト ハイデルベルク講演
1907 ブラウワー 学位論文『数学の基礎について』発表
1908 ツェルメロ 集合論の公理系を発表
1910 ラッセル・ホワイトヘッド 『プリンキピア・マテマティカ』第1巻 刊行出版
1918 ワイル 『連続体』出版
1921 ワイル 論文「数学の基礎の新危機について」発表
1922 ヒルベルト 論文「数学の新基礎」発表(ヒルベルト・プログラム登場)
1928 ブラウワー ウィーン大学講演(ウィトゲンシュタインが出席)
1930 ゲーデル ケーニヒスベルク会議で発言(不完全性定理に言及)
1931 ゲーデル 不完全性定理論文を出版(ヒルベルト・プログラム挫折)

2010年7月20日火曜日

SDLがLanguage Weaverを買収

SDL は7月15日に、機械翻訳ベンダーである Language Weaver の買収を発表した。
このトピックに関するプレスリリースとブログからコメントをピックアップしてみる。

プレスリリースによると、買収価格は$42.5Mで全額現金による買収である。Language Weaver(以下LW)は2009年における売上が$12.2Mに対して$1Mの損失を出しているから、売上に対して約3.5倍の買収価格となる。LWの96名の従業員を解雇する予定はなく、創業者であるDaniel MarcuとKevin Knightは留任、LWのCEOであるMark Taplingも留任すると発表されている。

SDLのCEOであるMark Lancasterは、今後5年ですべての翻訳コンテンツのうちの30%以上がMTをプロセスに組み込むと予想している。SDLでは、現在自動翻訳は翻訳市場の1%を占めるにすぎない(IDC予想)が、マーケット全体も自動翻訳の占める割合も大幅に増えていくと予想しており、自動翻訳の普及により顧客は翻訳単価の30%から50%の下落と同時に翻訳時間の50%以上の短縮を期待できると予想している。

SDL Announces Acquisition of Language Weaver 

LWに対しては複数のベンチャーキャピタル(VC)が投資していたが、その中で注目されるのはIn-Q-Telだろう。In-Q-TelはCIAの運営する非営利VCで、CIAの意向を反映して先端技術への投資を行なうVCとして知られており、かつてはGoogle Earth の開発企業だった Keyhole(現在はGoogleに買収)にも投資していた。9.11テロの翌年である2002年に創業されたLWはこれらの投資を受けて、主に米国政府に対してアラビア語ー英語間の翻訳を行なうサービスを提供してきたと考えられている。

Language Weaver Announces Second Strategic Investment and Contract from In-Q-Tel

LWは昨年4月からSDLとの間で販売代理店契約を結んでおり、今回LWを直接傘下に収めたことで同社のワンストップソシューリョンに統計的機械翻訳サービスを追加したことになる。SDLはこの買収によってLWの優れたソリューションをより多くの顧客に提供できると期待している。

Global Watchtower™ » Blog Archive » SDL Acquires Language Weaver http://bit.ly/dxcXEs

とはいうものの、かつてSDLはIdiomを買収してそのオープンな製品の長所をうまく継承できなかった(あるいは意図的に継承しなかった)という印象を持つ業界関係者も多く、SDLの顧客サポートでは顧客の満足が得られないのではないかという辛辣な見方も一部にはある。Renato Beninattoは、SDLが上場しているロンドン株式市場の投資家を喜ばせるためにソフトウェア開発企業の買収を繰り返すのだという皮肉な見方を披露している。

Localization Industry 411: SDL Acquires Language Weaver. First Reactions. http://bit.ly/bhWRZE

また、かつてLWでセールス&マーケティング担当のVPだったKirti VasheeはLWのSMT技術の優位性に疑問をなげかけている。Google Translateが提供する無償のアラビア語ー英語翻訳に対してすでにLWのMTは品質上の優位性を失っているのではないかという。さらにVasheeはLWが翻訳産業との連携を数年前から行っていない点を問題視している。MTの品質改善のためには翻訳業界の(人間の)リンギストとの協力が非常に重要だがLWはそれをやっていないと指摘している。

MTの市場を拡大するには品質が決定的に重要だが、LWのアプローチではそれは達成できず、その結果としてLWが米国政府以外への売上を伸ばせなかったとの解釈である。また、SDLについてはすでに3つもTMS製品を持っているのにその製品相互間のデータ交換すらロスなしには行えない点を指摘し、SDLが買収した製品をユーザーの利用しやすい形(オープンな仕様による容易な相互接続)で提供することはできないのではないかとの懸念を指摘している。

eMpTy Pages : Is SDL Getting Serious About MT? Does It Matter?