形式化とは，現代数学の主要な技法であると同時に，計算機の扱える対象でもある．
「言葉」というものの記号的機能(symbolic functionality)を推し進めたものを「形式」と呼ぶ．
現代数学は形式を形式として扱う．１つの対象を記号に押し込める．抽象化した理論の形式ほど，強力な言葉になる．
最近、数学を専門として勉強し始めた学生向けの授業をうけもつ機会が多い。今の数学のカリキュラムでは、まず抽象的な数学の思考法に慣れることが重要になる。そこで、抽象数学では、記号はただの記号であることがだいじだが、ただの記号と思ってはいけないなどという話をする。矛盾しているようだが、いいたいのはこんなことである。ただの記号であるとは、どんなものでもあてはめてよいということである。そう思ってはいけないというのは、 記号にあてはめられるものには、実に多様なものがあり、それらについての実体感抜きでは、本当の理解にはならないというつもりである。 しかし、グロタンディークは、スキーム$X$とい えば、ただ$X$だと思っていたのではないかという気もしてくる。とすると、そんな話をしても、未来のグロタンディークにとっては、余計なお世話かもしれない。でもグロタンディークだからこそ、それでよかったのだとも、一数学者としては思うのである。
斎藤毅「グロタンディーク」
数学科には実験がない．形式科学であるからだ．つまり，数学は「形式」を用いて実験をする．
HelmholtzがMayerについて語っているように，素人を専門家から区別するものは，ただ素人がこれと決まった作業方法を欠き，従って与えられた思いつきについてその効果を判定し，評価し，かつこれを実現する能力を持たないということだけである．
Max Weber著，尾高邦雄訳 『職業としての学問』（岩波文庫）
コメント