>>73 補足

中高一貫生も来るから ハッキリと書いておくが

＜古典論理 vs 直観主義＞
１）特に断らない限り、普通は数学は 古典論理ベースと思っていい
　（ヒルベルトの形式主義が生き残った）
２）では、直観主義が完全に否定されたかというと 特殊分野では 生き残っている
　一つは、ラムダ計算 カリー＝ハワード対応 コンピュータプログラミング（除くAI）の世界
　（コンピュータプログラミングは、プログラム構成してなんぼの世界で、構成主義）
　一つは、量子論理の世界（流行りの量子コンピュータもこれ）
　つまり、普通のコンピュータプログラミングは 0か1のブール論理なのだが
　量子論理は 0か1に限られない（下記 en.wikipedia Boolean_algebra辺り からご自分で調べてください）

https://ja.wikipedia.org/wiki/%E7%9B%B4%E8%A6%B3%E4%B8%BB%E7%BE%A9_(%E6%95%B0%E5%AD%A6%E3%81%AE%E5%93%B2%E5%AD%A6)
直観主義（英: Intuitionism）とは、数学の基礎を数学者の直観におく立場のことを指す。
来歴と評価
これに類する主張は、カントールの集合論に対抗する形でクロネッカーやポアンカレによってもなされていたが、最も明確に表明したのはオランダの位相幾何学者ブラウワーである。ブラウワーの立場に対してポアンカレらの立場は前直観主義と言われることがある。ブラウワーは、数学的概念とは数学者の精神の産物であり、その存在はその構成によって示されるべきだという立場から、無限集合において背理法によって非存在の矛盾から存在を示す証明を認めなかった。それゆえ、無限集合において「排中律」、すなわちある命題は真であるか偽であるかのどちらかであるという推論法則を捨てるべきだと主張し、ヒルベルトとの間に有名な論争を引き起こした。 ヒルベルトの形式主義は、直接的にはブラウワーからの批判的主張に対し排中律を守り、数学の無矛盾性を示すためのものと考えることができる[1]。

ブラウワーの主張は感覚的で分かりにくかったが、その後ハイティング等によって整備され、結果的には古典論理から排中律を除いた形で形式化されたものが今日、直観主義論理として受け入れられている。 現代では直観主義論理は、数学の証明は全て構成的に為されなければならないという主張（数学的構成主義）と関連が深いと考えられている。

https://ja.wikipedia.org/wiki/%E7%9B%B4%E8%A6%B3%E4%B8%BB%E7%BE%A9%E8%AB%96%E7%90%86
直観主義論理
ラムダ計算
カリー＝ハワード対応はIPCと直和と直積を持つ単純型付きラムダ計算との間に拡張できる。[6]

https://en.wikipedia.org/wiki/Boolean_algebra
Boolean algebra