形式主義

前回、直観主義に対してヒルベルトが
「そんな禁欲的な数学、耐えられるか！」
と新しい数学体系の樹立に動き出した、というお話をしました。

その新しい数学は、形式主義と呼ばれています。形式主義を一段階だけ説明しますと、
・数学を形式的な公理系として整備すること
・無矛盾性と完全性を有限の立場のメタ数学で証明すること
この2本立てです。

( ゜Д゜)ナンノコッチャ???

ゆっくり説明していきます。数学を形式的な公理系として整備するとは、数学を単なる式変形のゲームと考え、そこに一切の意味を与えないようにします。

例えば、
「ドラゴンクエストⅢでは、魔法使いは炎を出す魔法(メラ)が使える」
ということに対して、
「人間が炎出すなんてナンセンスだろ？」
という人が直観主義。でも形式的体系として考えれば、
「ある特徴を持つキャラクターは、敵にダメージを与える特殊な行動が可能である」
という“意味抜き”の次元に抽象して
「こういうゲームだから！」
と説明するわけです。

こうしてしまえば、無限や排中律という概念の「意味」を考える必要がなくなります。ただ、パラドックスが起こってはいけないので、今までの数学体系から不具合のある部分だけを修正する必要があります。

次の無矛盾性と完全性をメタ数学でチェックするとは、上の議論で整備した数学が、首尾よくゲームとして機能することの確認です。

どんな手段を用いても相手にダメージを与えられないとか、島から外に出る手段がないとか、そんな不具合があるとゲームとして成立しないわけで、(どんなに難しかろうが)ちゃんとクリアできることを確認する作業です。

なおかつその証明の手段を「有限の立場」に限定しました。排中律が問題になるのは無限に関係した対象を扱う際であり、有限回の式変形で全て証明できてしまえば、排中律を拒否する理由はなくなります。なぜなら、有限回であれば、(たとえどれほど時間がかかったとしても)地道にチェックしていけば「AかAでないか」を直接調べることができるからです。有限の立場にこだわることで、排中律を復権させようとする魂胆です。

意味のない式変形のカタマリとしての数学と、直観主義者でも拒否できない形で展開されるチェック機構。これが形式主義の構図です。これが上手くいけば、排中律は大手を振ってまかり通り、ラッセルのパラドックスはおろか、二度とそんな憂き目には遭わない無矛盾で完全な数学が打ち立てられることになります。

「こんな理想的な数学を作ろう！」
ヒルベルトが音頭を執って始まった「ヒルベルトプログラム」。・・・だったんですが、若き天才・クルト=ゲーデルがヒルベルトプログラムの破産を宣告してしまいました。それはまた次回のお話。