数学に正解は一つしかないのか？

概要: 自分はそうは思わないし，数学はもっと広く捉えられるべきだろう．

記事の主張は「数学の学習は寛容性を育む」ということだが，その点については同意も否定もしない*1．
ただ面白いのが

数学が他の学問とはっきりと違うことは真の意味で正解が一つしか無いことである

と主張していることだ．これは数学の哲学における数学的実在論である．
著者は次のように続ける(強調は自分が追加):

(注: 社会科学における正しさはある種恣意的であるものの)一方で数学は基本的に正しいとされているものは（現代の一般的な数学においては）ZFC公理系のみであり、それと一階述語論理の重なり合った推論を用いて数学は記述されている。つまり、そのルールに違反しているものはすべて一様に間違いであり、そこに人間の恣意的な部分が入り込む余地は全く残されていない。「正しそう」「多くの人に支持されている」などといったものは厳密には数学には存在せず、そこには「正しい」と「間違い」しかない。

すなわち，数学的な命題の真偽は我々人間とは独立に定まっており(太陽が我々とは独立して「実在」するように)，数学とは真理に接近するための手段であるのだ*2．
このような立場は一般の人たちにも広く受け入れられているだろう．数学の命題は十分注意を払えば取り違えなんて起こらないような明確さで記述されているし，数学的な議論というのは我々が普段するような議論とは異なってとても厳密さに注意を払っているようである．学校教育は数学という科目でそのようなただ一つの正解を教え込んでいるのだ！
しかし「数学者」が実際にやっていることを眺めてみると案外そうでもないかも…という気になるかもしれない．自分は残念ながら数学者ではないのだが*3，数学の哲学を含む科学哲学に興味を持つ立場から意見を述べたい．

数学の様々な基礎づけ

ZFC公理系による公理的な集合論が現代の数学における標準的な基礎づけである，すなわちZFCを公理系として採用することは合理的なことであり*4現代数学をその上に展開することができる，ということは広く受け入れられていることである．
しかし，数学にはそれ以外の基礎づけも知られている．この記事では型理論を基にした基礎づけを紹介しよう．

型理論では数学の項に対して型を割り当てる．例えば0や100という数値には整数型が割り当てられるし，「∀x∃y. xRy」のような命題を表す項には真理値型が割り振られるだろう．プログラミング言語を触ったことがある人にはなじみ深い概念かもしれない*5．
型理論を用いた数学の基礎づけでは，型の合わない文は無意味である．これは集合の所属関係∈のみをベースとし，「7 ∈ 42」が有意味である(しかも適当な構成の下で真ですらある)ZFCとは対照的である．
型理論ベースの数学は定理証明支援系の分野で広く用いられている．

例えば，Isabelle/HOLという定理証明支援系ではSimple Type Theoryという型理論をベースに高階論理を用いて数学を形式化している．Isabelle/HOLで形式化された数学の一つにはHOL-Analysis(実解析)がある．
Simple Type Theoryよりも高度な型理論，特に依存型を用いた定理証明支援系も良く使われている．その典型例がCoqやLeanだろう．Leanのmathlibでは「数学者」とコンピュータ科学者が共同で数学の形式化に取り組んでいるようだ．
これらの体系は型理論をベースとしているという点では似ているが，採用している公理系は異なる．例えば，Isabelle/HOLでは排中律やHilbertの選択演算子(選択公理より強いらしい)を公理として導入しているが，CoqやLeanでは公理ではない(もしくは慎み深く部分的に用いられる)．
当然，片方の体系では成立する定理がもう片方の体系では成立しないということもある．「数学に一つの正解しか存在しない」ならば，彼らのいずれかは間違っていることになりそうだ．
しかし自分はそうは思わない．特に数学には複数の「正解」が存在すると捉えるのが良いと考える．つまり，やりたい「数学」を便利に展開できるように公理系は好きに選べば良いのだ．

型理論ベースの数学でも集合論的な議論は良く用いられている．ただし，その定式化のされ方は，既存の型をベースにして分出公理によって部分集合を構築するようなやり方である．
一方，ZFCでは分出公理は導出される定理の一つであり，これらの体系間で集合の様相というのは異なっているように見える．HOLZF(ZFCをIsabelle/HOL上で形式化したもの)では「ZF集合(の型を持つ項)全体の集合」なんてものも定義できてしまう．
しかし，それでもZFCの集合と型理論上の集合で同じようにクリーネの不動点定理を証明することができる．
これはある意味当然なことである．なぜなら，数学の公理系は我々の行うような数学的議論を再現し正当化するために作られてきたからである．
一方でこの事実は驚くべきことでもある．異なる数学の基礎づけ(それぞれ成立する定理も異なる)が同じ「数学」(順序集合の理論)を再現できるからである．
自然言語に例えるならば，日本語と英語はそれぞれ異なる言語であるけれども「涼宮ハルヒ」はどちらの言語でも刊行できるということだ(細部のニュアンスは変わってしまうだろうが)．

我々(や「数学者」)のやりたい「数学」が様々な公理系で展開できるのならば，それらから一つを選ぶ理由は外から与えられるであろう．
それは例えばコミュニティにおいてスタンダードであったり自分が慣れている(ZFC公理系)からかもしれない．一方で，定理証明支援系の分野で型理論が広く使われているのはプログラミング言語との相性の良さだろう．
もしくは「論文になるならなんでもやる」のかもしれない(これはやりたい「数学」のために公理系を選ぶ例だが)．

たまたまです。論文になるならなんでもやります。
CHとある命題が両立するかというのをポスドクのときから考えていて、その経緯でCHのモデルに詳しくなりました。そのためむしろ、CHがいかに不安定かを感じることが多く、安定状態は¬CHだろうという気がします。
— くるる (@kururu_goedel) 2020年11月28日

もしくは一つを選ぶ必要すら無いかもしれない．我々が消費税を計算する際に実数の構成までいちいち後戻りしないように，通常の「数学者」もやりたい「数学」のために公理系まで戻る必要は無いし，実際気にしないことが多いと想像している*6．

数学の範囲

一方で様々な基礎づけが用いられている状況を実在論者の視点から擁護することもできる．つまり，今我々が持っている公理系は「未完成」であり，「真の数学」のイデアを射影したようなものなのだ．
この視点から見ると，同じ「数学」(順序の理論)が種々の公理系から再現できることはまさに実在論の証拠となる．なぜならば，異なる数学体系から順序の理論がそれぞれ構築できるということは，順序の理論が数学の形式化とは独立した対象(実在)であることを意味しているからだ*7．
したがって，「数学には一つの正解しか存在しない」(真の数学だけが数学である)．しかしそれぞれの公理系を採用する「数学者」たちは別に間違っているわけではない．彼らは様々な方法で真理(真の数学)に接近しようと努力しているのだ．

自分はこの視点も筋は通っていると思う．ただし，現状真の数学を我々が獲得できていない以上，この立場では「数学者」がやっていることが数学では無くなってしまう．「前数学」とでも呼べばよいのだろうか．
しかし，そのようなラベリングはあまり豊かではないと考えている．「数学者」が(とりわけ)やっていることは数学だと考えるのが我々の言語感覚にマッチしているし，そこに色々面白いことがあると思うのだ．

前数学も数学に含めるような感覚は歴史的にも肯定できる．例えば，ピタゴラス学派が三平方の定理を発見したとき・古代インドでゼロの概念が発見(発明?)されたとき，彼らのやっていたことはその時代で最先端の数学と呼ぶのがふさわしいだろう．
当時にも『原論』のような公理化の動きはあったのかもしれないが，それらと現代の基礎づけの厳密さとは比べるべくもないだろう．しかし彼らは数学者であったはずだ．
ニュートンとライプニッツは微積分学を発見(考案?)した．オイラーはその上に豊かな力学の世界を築いたのだ．彼らの働きを数学からのけてしまうのは不適切だと思われる．
もしくは，「数学者」たちが現在取り組んでいる未解決問題を考えてみるのも良い．象徴的な例が宇宙際タイヒミュラー理論だろう．考案者らは当然理論が正しいと考えている一方で，「数学者」コミュニティからは疑問の声が挙がっている．
真の数学が存在するという立場からすれば彼らの論争はあまり意味のないことかもしれない．しかし，自分はこのような例を人間の営みの一部の数学としてとても興味深いと考えている．

結局のところ，自分は数学を単なる定義・定理・証明の羅列に還元したくないのである．数学は数学的なアイデアを発見(考案)したりそれを伝達したりするようなプロセスだと考えたいのだ．
この視点からすると，アルゴリズムやヒューリスティクスだって数学の一部である．小学生にさくらんぼ計算を教えるとき，我々は足し算というアイデアを具体的なアルゴリズムを通じて伝達しているのだ．
ヒューリスティクスは常に成功するとは限らないという点では「一つの正解」であるとは言いがたい．しかし，ε-δ論法を用いて収束列の評価をするとき，必要条件から逆算していって良さそうなδを見つけるのは数学だ(そして学生は「天下りだ！」と不平を垂れるのだ)．
このようなヒューリスティクスは「数学者」の中でも用いられているように見える．例えばフェルマーの最終定理のワイルズによる証明とグロタンディーク宇宙の関係についての質問では

Many working arithmetic and algebraic geometers however take it as an article of faith that in any use of Grothendieck cohomology theories to solve a "reasonable problem", the appeal to the universe axiom can be bypassed.

と述べられており，信頼のおける「数学者」によると実際に回避は可能なようだ．このような信条・テクニックと呼ばれるものはほかにも存在する．例えば「巨大基数公理に関する目覚しい知見の一つとして、それらが無矛盾性の強さ（英語版）から見ると厳密な線形順序に従うという経験則」が存在するらしい．
これらはとても興味深いし，数学だ(と思いたい)．

数学ゲームの比喩

元の記事では数学とスポーツ競技を比較して違うものであると述べている部分がある．

学問に限らずに話を広げると、ルールが画一されているという点ではスポーツ競技を思い浮かべることがあるかもしれない。例えばサッカーや野球は全世界でほとんど共通のルールで争われている。しかしながらその勝ち方やゲームの進め方はチームや各選手それぞれである。パスサッカー、カウンター狙い、機動力野球に重量級打線。そのどれもがスポーツのエンターテインメント性を高め、そういった差異がある状態こそがスポーツのコンテンツパワーを向上させている。麻雀に関してはルールさえ画一されていない上に絶対的な正しさを知ることは物理的に不可能である。

自分はこの議論をあまり説得的だとは思えない．それよりも数学とゲームの類似性を際立たせているのではないかとすら思う．
すなわち，数学は(形式化にはいろんなやり方があるとはいえ)ほとんど共通のルールで営まれており，しかしながら勝ち方は各選手それぞれなのだ．代数を使ってもよいし幾何でも解析でもいい．やっていることには差異があるのに，しかし数学ができてしまう．それが数学のコンテンツパワーを向上させているのだ．絶対的な正しさ(真の数学)を知ることはできるのだろうか？自分はとんでもなく難しいと思うけれども，あなたの意見は違うかもしれない(特に実在論者なら)．

なんならサッカーコートに立つ必要すらない．チームのオーナーは個々のプレイになんて興味は無くて，動員数が増えればいいのかもしれない．物理学者やコンピュータ科学者，もしくは応用「数学者」が純粋数学の結果だけ刈り取っていくかのように*8．
しかし，数学の応用，例えば物理数学が純粋数学の発展に繋がることも歴史的に多々生じてきた．そしてそれは今後も続くだろう(くりこみ群とか)．すると数学の応用ですらも数学の範囲に含めてしまっても良い気がしてくる*9．