Waseda Institute for Advanced Study (WIAS)早稲田大学 高等研究所

News

ニュース

数学における構成概念の探求 藤原誠 助教 (2016年12月当時)

数学的思考の本質に迫りたい

私は子供のころから数学は得意でしたが、公式を暗記することは大嫌いでした。簡単に証明することが出来る主張を公式としてわざわざ暗記する必要性を見出せなかったからです。また、公式を暗記し、それを適用して答えを出しても何も「できた」気がせず、その証明の構造や意図を理解して初めて「できた、わかった」という感覚になりました。それは今も変わっていません。
私はいつしか「数学の主張には全て厳密な証明があるはずだ」という漠然とした信念のようなものを持っていました。半分は希望でしかなかったその信念が確信に変わったのは、一つ一つ掘り下げる私の質問に一寸のごまかしや曖昧さも残さず明瞭な回答をくれる高校の数学の先生に出会った時でした。数学をきちんと理解したい、理解しなければならないという思いで大学の数学科に入学しました。しかし、高度に抽象的で難解な大学の数学の前に私は「数学の証明が理解できない」という大きな壁に直面します。そんな時、数学基礎論の一分野として証明論と呼ばれる分野があると知り、数学の証明とは何なのかを理解すればその壁を超える糸口を見出せるかもしれないと思い、本格的に数学基礎論の勉強を始めました。この時の暗中模索した経験は「数学的思考の本質に迫りたい」という願いとなって私の現在の研究テーマに繋がっています。

数学基礎論:数学そのものを数学によって解析する

数学はよく解析学、代数学、幾何学、その他に分類されますが、私の専門分野である数学基礎論は、この分類に従えば「その他」に分類されるある種「風変り」な数学の一分野です。解析学や幾何学、代数学がそれぞれ実数や図形、代数構造などを考察の対象とするのに対し、数学基礎論は「形式化」という手段を介して数学そのものを考察の対象とします。

ブラウアーの直観主義と構成的数学

素朴集合論に矛盾があることが発見されて以降、数学の基礎に関する問題は当時の先駆的数学者らにとって重要な問題となりました。20世紀初頭、オランダの位相幾何学者ブラウアーは、数学的概念とは数学者の精神の産物であり、その存在はその構成によって示されるべきという立場をとり、ヒルベルトの形式主義に対抗する形で、直観主義と呼ばれるその独自の哲学に基づいて数学の再構築を試みました。ブラウアーの数学は当時の数学者たちに受け入れられることはありませんでしたが、その構成的な推論を形式化しようとして弟子のハイティングによって導入された「直観主義論理」はその後の数学基礎論や計算機科学の発展に多大な影響を及ぼしました。
1960年代以降、ビショップらによって展開された構成的数学は、その証明において構成的な推論のみを認める(制限された)数学であり、現代では、およそ「直観主義論理」に基づく数学と理解されています。構成的数学では、通常の数学では暗に仮定されている排中律「全ての命題は真であるまたは偽である」は認められません。構成的数学では「命題Pが真であるまたは偽である」ということは『「命題Pが真であること」の構成的な証明があるまたは「命題Pが偽であること」の構成的な証明がある』ということに他なりません。しかし、我々は(少なくとも現時点では)すべての命題に対してこのどちらかを持っているわけではありません。例えば、リーマン予想やP-NP問題のような数学の未解決問題については、我々はどちらの証明も未だ持ち合わせてはいないのです。

ヒルベルトの形式主義と逆数学

20世紀初頭、当時の先駆的数学者ヒルベルトは、形式化と言われる、数学的命題を少数の記号の列、証明において使われる推論をその記号列に関する記号操作と捉える考え方で、排中律を守りつつ、初等的な(有限の立場に基づく)証明方法によってそれまでの数学の無矛盾性を示そうと試みました。ヒルベルトのこの試みはヒルベルト・プログラムとして知られています。ゲーデルの不完全性定理により、ヒルベルト・プログラムはおよそ実現不可能であることが判明しましたが、「数学の理論を形式化し、その形式化した対象を解析する」というヒルベルトの方法論はその後も数学基礎論の主流として受け継がれていきました。
その流れを汲むものとして、1970年代から行われている逆数学と呼ばれる研究があります。逆数学では、数学の諸定理を適切な基盤体系の上で形式化し、その証明に最低限必要な公理は何であるかを調べます。ここで、基盤体系の取り方はとても重要です。なぜなら、基盤体系の取り方は「どのような立場から数学を分析するか」を反映するからです。従来の逆数学では、およそ計算可能数学に対応するRCA0と呼ばれる基盤体系を採用しており、これにより「どれくらい計算不可能な集合の存在を認めれば数学の諸定理が証明できるか」が分析できます。最近では、RCA0の推論規則を、通常の数学の証明における推論の形式化である「古典論理」から前述の「直観主義論理」に置き換えた(弱めた)ものを基盤体系として採用した、いわば直観主義版の逆数学研究も行われています。
私は現在、数学における構成概念に興味を持っており、構成的な推論に基づいて数学的思考に関する逆数学的な解析をしてみたいと思っています。それは、数学の証明の多くが共通して持つ特徴はその構成性であり、私には構成概念は数学的思考の本質に関わるものであるように思えるからです。そのためには、そのような解析に相応しい基盤体系を構築する必要があります。

直観主義論理は本当に数学における構成的推論の形式化なのか?

直観主義論理は古典論理よりも真に弱い論理であり、直観主義論理に前述の排中律を公理として加えると古典論理が得られることが知られています。それゆえ、現代では「直観主義論理は古典論理から排中律を除いたもの」と一般に理解されています。しかし、「通常の数学の推論」に対応する古典論理から排中律を除いただけで、なぜ「構成的推論」に対応する論理が得られるのでしょう。そもそも、構成的推論は本当に直観主義論理によって完全に形式化されているのでしょうか。実際には、直観主義論理がおよそ構成的推論に対応するということは数学基礎論の研究者の共通認識と言っても過言ではありません。しかし、それは、直観主義論理に基づいた基盤体系の上で構成的数学における証明が模倣できるということが経験則として知られているからであって、直観主義論理がちょうど構成的推論の形式化であることの理論的根拠は未だ十分であるとは言えません。また、直観主義論理では証明できないが、ある意味では構成的であると思えるような論理原理も知られています。構成的推論の形式化についてのこの根本的問題には、1920-30年代に直観主義論理が考案された当時から現在に至るまで明確な回答が与えられておらず、現在も哲学と数学の両面から研究が続けられています。
私は、この哲学的な問いに何かしらの数学的な回答を与えたいと思っており、現在いくつかの方向から並行して研究を進めています。また、この問題についての考察を深めるため、数学の哲学の専門家とも積極的に交流をしています。まだまだ先は長いですが、いつしか、数学によって、数学的思考の本質を捉えるような研究ができればうれしいです。

図:数学のつくられ方のイメージ
Theoremは定理 Axiomは公理

 

 

協力:早稲田大学大学院政治学研究科J-School

Page Top
WASEDA University

早稲田大学オフィシャルサイト(https://www.waseda.jp/inst/wias/)は、以下のWebブラウザでご覧いただくことを推奨いたします。

推奨環境以外でのご利用や、推奨環境であっても設定によっては、ご利用できない場合や正しく表示されない場合がございます。より快適にご利用いただくため、お使いのブラウザを最新版に更新してご覧ください。

このままご覧いただく方は、「このまま進む」ボタンをクリックし、次ページに進んでください。

このまま進む

対応ブラウザについて

閉じる