ウィトゲンシュタインの「数学者は数学的対象を発見しているのではなく発明している」という言葉について考えていた。
例えば、形式的なルールが与えられていれば、コンピュータを用いてひたすら定理を作ってゆくことができる。形式主義の立場はそういうものだ。そして、ここにおいて矛盾が導かれることは致命的である。コンピュータは機械的にルールを適用してゆくだけだから、そこにおいて生じた矛盾は、コンピュータにとっては他の結果と区別できないひとつの結果に過ぎず、それ故我々が期待するものと異なる数学を作り上げてしまいかねない。だがそれは我々にとって好ましくないというだけであり、ルールの適用として間違ったものではないのである。ここにおいて矛盾の好ましくなさはメタな記述である。
この好ましくなさを排除するために、数学が満たすべき性質を公理として織り込んでおくことは自然な方法である。例えば、ゼロ除算を排除しておくことで、1=2といった(我々にとって)不都合な定理が導かれないようすることが可能である。だが不都合な定理を導きうるすべての規則をはじめから除いておくことはむつかしい。数学の全体を見通すことなんてできないわけで、無矛盾性の証明は不可能であることが知られている。
ウィトゲンシュタインは、矛盾が生じたところでそこに新たな規則を付け足せば十分であると述べた。抜け道はあるのだがその存在がこれまで知られていなかった牢獄は、牢獄として十分機能していたわけであり、抜け道が見つかってしまったならそのときにそこを塞いでやれば良い、と。この考え方は、還元すれば、証明をコンピュータのみに任せないということである。我々にとって好ましい数学は、我々の生活の階層において規定されているのであり(例えば1!=2という規則は、ものを数えるために必要である)、形式的証明がそれからずれた場合には、適宜修正を加えればよろしいという、素朴な考え方だ。これは「発明」という表現によく現れていると思う。
ところで、n!=mという規則を先に与えておくことによって、機械的にゼロ除算を除くような形式的体系をつくることはできないだろうか。これはおそらく難しい。なぜならそのためにはルールと、それによって導かれる命題とが同じ階層に存在せねばならないことになるから。コンピュータは矛盾が生じたことを知ることはできる。だがそれが「何によって」生じたのかを知ることはできない。それはメタな記述である。
「論理的形式を表現しうるためには、われわれは、命題を携えて論理の外に、すなわち世界の外に出ることが出来なければならぬ」(『論考』4.12)とは、このような考えを背景にしているのだろうと思う。形式的な数学の中で行われる記号操作が規則そのものに対して物申せないのと同じように、論理の内側で思考する我々は、論理については語りえないのである。
