最初に食いついたのは「仮想化（virtualization）」がらみの部分。
不完全性定理とかの話で出てくる「算術の算術化」、昔は全然イメージが湧かなかったんですが、最近は「人間（メタメタレベル）がコンピュータ（メタレベル）の中で仮想機械（対象レベル）を動かしているんだ」と説明できるようになったのでとっても楽ですね。
— ytb (@ytb_at_twt) March 20, 2019
ちなみにグレッグ・イーガンの「順列都市」ってエミュレータ上でエミュレータを動かすプロセスを「無限」に続ければ、無限だから出発点の物理世界は関係なくなってエミュレータだけが存在すると仮定できるという話で何その余帰納法。
— ytb (@ytb_at_twt) March 21, 2019
あ、これ「楽園追放 Expelled from Paradise （2014年）」の元ネタ…
それにしても強い…
数学的事実に対し「この世のバグだと思う」とか言っている人、バグなのはオマエだ。
— ytb (@ytb_at_twt) March 21, 2019
こういう話にこう返すとは…
第一の点は、〈数学の概念は、まったく予想外のさまざまな文脈のなかに登場してくる〉ということ。
The first point is that mathematical concepts turn up in entirely unexpected connections.しかも、予想もしなかった文脈に、予想もしなかったほどぴったりと当てはまって、正確に現象を記述してくれることが多いのだ。
Moreover, they often permit an unexpectedly close and accurate description of the phenomena in these connections.第二の点は、予想外の文脈に現れるということと、そしてまた、数学がこれほど役立つ理由を私たちが理解していないことのせいで、〈数学の概念を駆使して、なにか一つの理論が定式化できたとしても、それが唯一の適切な理論なのかどうかがわからない〉ということ。
Secondly, just because of this circumstance, and because we do not understand the reasons of their usefulness, we cannot know whether a theory formulated in terms of mathematical concepts is uniquely appropriate.〔この二つの論点をさらに言い直すと〕第一の点は〈数学は自然科学のなかで、ほとんど神秘的なまでに、途方もなく役立っているのに、そのことには何の合理的説明もない〉ということ。
The first point is that the enormous usefulness of mathematics in the natural sciences is something bordering on the mysterious and that there is no rational explanation for it.第二の点は〈数学の概念の、まさにこの奇怪な有用性のせいで、物理学の理論の一意性が疑わしく思えてしまう〉ということ。
Second, it is just this uncanny usefulness of mathematical concepts that raises the question of the uniqueness of our physical theories.
しかしもちろん、ちゃんと理解するのは難しそう…
数学者にとって、数学的事実とは何よりも大切なモノであるはずである。数学的事実が、自分の貧しい直観を越えていることを認識すること、そしてそれが物理世界にも何故か応用できることを知ること、それが数学の楽しみのはずだ。
— ytb (@ytb_at_twt) March 21, 2019
ところが、 一部の直観主義者には、自分の貧しい直観に揃えて数学を切り刻むことが楽しくてしょうがないらしい。ブラウアー以来の伝統であろうが、「無限論の教室」のような哲学側のカウンターパートと合わせて、数学基礎論における暗愚主義の流れを形成している。
— ytb (@ytb_at_twt) March 21, 2019
構成主義が計算機科学に引き取られ、計算という現象についての経験科学となり、厨二病のテロリストのようなことは言わなくなった影で、未だに直観主義的世迷い言がはびこることは大変残念である。
— ytb (@ytb_at_twt) March 21, 2019
日本のネット上では、一時期、数学基礎論の話題と言えば、自称「直観主義者」のポイントレスな話ばっかりで（stormdorf氏とかなつかしい）、あまりにもあんまりで、ボクがhatena diaryを始めたのは、少しは公共的な議論のレベルをあげたいと思ったからです。十年一日。
— ytb (@ytb_at_twt) March 21, 2019
数学の基礎を数学者の直観におく立場のことを指す。これに類する主張は、カントールの集合論に対抗する形で、クロネッカーやポアンカレによってもなされていたが、最も明確に表明したのは、オランダの位相幾何学者、ブラウワーである。
ブラウワーの立場に対してポアンカレらの立場は前直観主義と言われることがある。ブラウワーは、数学的概念とは数学者の精神の産物であり、その存在はその構成によって示されるべきだという立場から、無限集合において、背理法によって、非存在の矛盾から存在を示す証明を認めなかった。それ故、無限集合において「排中律」、すなわち、ある命題は真であるか偽であるかのどちらかであるという推論法則を捨てるべきだと主張し、ヒルベルトとの間に有名な論争を引き起こした。 ヒルベルトの形式主義は、直接的にはブラウワーからの批判的主張に対し排中律を守り、数学の無矛盾性を示すためのものと考えることができる。
ブラウワーの主張は、感覚的で分かりにくかったが、その後ハイティング等によって整備され、結果的には古典論理から排中律を除いた形で形式化されたものが今日、直観主義論理として受け入れられている。 現代では直観主義論理は、数学の証明は全て構成的に為されなければならないという主張（数学的構成主義）と関連が深いと考えられている。
直観主義論理に基づく数学によって得られる成果は、古典論理に基づく数学に比べて制限されたものにならざるを得ない。具体的には、ab = 0 から a = 0 または b = 0 を直接結論することはできない。なぜなら、直観主義においては、「a = 0 または b = 0」が証明できるというのは、「a = 0」が証明できるか、または「b = 0」が証明できることを意味するからである。また、ワイエルシュトラスによる実数体の任意の有界な部分集合は上限を持つという定理が証明できない。
しかし、直観主義は単なる思想としてだけではなく、数学基礎論や計算機科学に様々な影響を与えている。
逸話
ブラウワーは「AであるかAでないかが分からない場合もある」を説明する例として、「円周率の無限小数の中に0が100個続く部分があるかどうか分からない」というものをあげていた。
あるとき、ブラウワーがこの話をしたとき、「しかし神なら100個続く部分があるかどうか分かるのでは？」という質問を受けたが、 ブラウワーはそれに対し「残念ながら我々は神と交信する方法を知りません」と答えた。
数学の哲学において、構成主義（constructivism）とは「ある数学的対象が存在することを証明するためには、それを実際に見つけたり構成したりしなければならない」という考えのことである。標準的な数学においてはそうではなく、具体的に見つけることなしに背理法によって存在を示す、すなわち存在しないことを仮定して矛盾を導くことがよくある。この背理法というものは構成的に見ると十分ではない。構成的な見地は、古典的な解釈をもって中途半端なままである、存在記号の意味を確かめることを含む。
多くの形の構成主義がある (Troelstra 1977a)。これらはブラウワーによって創始された数学的直観主義のプログラム、ヒルベルトならびにベルナイスの有限主義、ShaminならびにMarkovの構成的で再帰的な数学、そして構成的解析学であるBishopのプログラムを含む。構成主義はCZFやトポス論の研究のような構成的集合論の研究もまた含む。
- Troelstra, A. S. (1977a). “Aspects of constructive mathematics”. Handbook of Mathematical Logic. pp. 973–1052.
構成主義はしばしば直観主義と同一視される、しかしながら直観主義は構成主義者のプログラムのひとつでしかない。個人的な数学者の直観のなかに数学の基礎がおかれるところの直観主義数学は、それによってひとつの内在的で主観的な活動のなかへと数学をさせている (Troelstra 1977b)。他の形の構成主義は直観のこの見地において基礎をもたない、そして数学において客観的な見地をもって両立できる。
- Troelstra, A. S. (1977b). “Choice sequences”. Oxford Logic Guides. ISBN 0-19-853162-X.
数学基礎論（foundations of mathematics） - Wikipedia
数学の一分野。他の分野が整数・実数・図形・関数などを取り扱うのに対し、数学自体を対象とする。
厳密な論理によって構成される数学は、発展するに従って自分自身をも厳格に定義する方向へと進み、多くの数学者・論理学者がその夢に心血を注いだ。数学を論理学の上に基礎づける論理主義はフレーゲの独創的な仕事に始まるが、この計画はラッセルの発見したパラドックスによって頓挫する。
ラッセルは『数学原論』によってフレーゲの論理主義の問題点を解決するが、そこに用いられた公理はもはや論理的に自明とはいえず、本来の目的であった論理学に基づく数学の基礎づけに成功したとはいえない。
一方、ブラウワーは、直観主義によって数学をパラドックスから解放しようと試みるが、この考え方は、排中律の使用を制限することで数学の結果に対して大規模な修正を求めるものであった。
ヒルベルトは、数学を記号によるゲームとみなして無矛盾性を証明する形式主義によるヒルベルト・プログラムを提唱したが、ゲーデルの不完全性定理によって、その実現の不可能性が示された。また、数論を展開するのに十分な体系に見えるペアノの公理系では証明できないグッドスタインの定理など、特定の公理系では証明も反証もできない問題が数多く見いだされた。
このように一定の結論が得られた現在では、数学基礎論は本来の意味していた数学の基礎づけの活動から離れ、広義の数理論理学、特に集合論、モデル理論、証明論、計算理論等の数学の総称に変化している。
影響
数学を人間の精神活動から離れて、形式主義的にかつ有限の立場から検証しなおすことにより、計算機科学の基礎と発展に大きく寄与した。たとえば、今まで自明なものとして受け入れられていた多くの数論的関数を有限の立場から考察することにより、アルゴリズムの研究に直接の影響を与えた。
現在、プログラミングは初等教育にも取り入れられるほど一般的になっているが、プログラミング言語で必ず登場するデータ型の形式的宣言や論理構造、関数の概念は遠くは数学基礎論に由来する。ゆえに、数学基礎論で活躍したフォン・ノイマンやチューリングが後に計算機科学において先駆的な役割を果たしたのも、偶然ではない。
そのような意味で数学基礎論は単なる机上の空論ではなく、むしろコンピュータをインフラの一つとする現代社会の形成に多大な影響を与えたといえる。
とどのつまり方便、すなわちヒューステリックな方向に逃げない戦い方もあるという考え方なんでしょうか？
ヒューリスティクス（英heuristic, 独Heuristik） - Wikipedia
必ず正しい答えを導けるわけではないが、ある程度のレベルで正解に近い解を得ることができる方法である。答えの精度が保証されない代わりに、回答に至るまでの時間が少ないという特徴がある。主に計算機科学と心理学の分野で使用される言葉であり、どちらの分野での用法も根本的な意味は同じであるが、指示対象が異なる。すなわち、計算機科学ではプログラミングの方法を指すが、心理学では人間の思考方法を指すものとして使われる。なお、論理学では仮説形成法と呼ばれている。
