5分でわかる直観主義数学

今日は直観主義数学について5分で分かるように解説する。

直観主義数学とは何か?

直観主義数学とは、オランダの数学者ブラウアー(1881-1966)によって提唱された「直観主義」という立場に基づく数学である。直観主義は通常の数学(古典数学とここでは呼ぶことにする)を批判し、独自の数学を展開する対抗数学である。

直観主義数学は排中律(任意の命題Pについて「PであるかPでないかどちらかである」とする主張)を否定する数学と紹介されることがあるが、排中律を否定するのはその主張の一部であって、他の古典数学の主張も否定されたり、古典数学とは相容れない独自の主張がなされることもある。また、気まぐれに排中律を否定しているわけではなく、その背景には理由付けが存在する。

直観主義数学にもさまざまな立場がある。狭義にはブラウアーの展開した数学を指すが、ブラウアーの数学は難解かつ独自性が強い。例えば、ブラウアーは古典数学と対立する原理を積極的に採用する。一方で、直観主義数学は、広義には構成的数学と呼ばれる立場全体全体を指す。今日は後者の立場を取りたい。なお、マルティン・レーフの直観主義的型理論(ITT)が、現在における直観主義数学の定式化の主流であるように筆者は思っている。ITTにもどのような公理を認めるかでバリエーションがあるが、バリエーションがある事自体は直観主義の立場からは何も問題はない。

なお、古典数学の立場に立ちながら、直観主義数学の体系を古典数学の対象として研究することが可能である。このような立場の数学者も多いが、私は直観主義数学を古典数学に対して全く新しい数学理念を提示するものと捉えている。

直観主義数学は大雑把に言って「具体的に操作可能なもの」だけを対象とする。よって計算機科学と親和性が深く、実際、定理支援証明系の理論的な基盤になったり、プログラミング言語理論に影響を与えたり、検証付きのプログラム生成手法の理論になったりしている。

直観主義数学が大切にするもの – 証明

直観主義数学が古典数学と最も違うのは、直観主義数学で基本となる概念が「証明」であることだ。古典数学でも「証明」は基本のように思うかもしれないが、古典数学では数学の命題が「証明できるかどうか」とは独立に「真偽」が決まっていて、証明は真偽を確立する手段である。例えば、

命題P「4以上の偶数は2つの素数の和でかならず書ける」

は今のところ証明も反証もないが、真か偽かのどちらかであることは決まっていると考える。

一方、直観主義数学では、命題Pは証明も反証も未だないので、命題Pの真偽は定まっていないと考える。というより、人間が行う証明という活動を離れた命題の真偽というものは意味がないのである。しかし、直観主義数学の証明とはそもそも何か、疑問に思うかもしれない。答えは「直観主義数学においては、証明は命題を意味づけるプリミティブな概念である」というものである。もう少し詳しく言うと、例えばITTでは命題を一般化した「判断」とその証明は相互再帰的に定義される。

そうすると排中律

PまたはPではない

が真でないことが(すくなくとも素直に「または」を解釈する限り)分かる。上の命題が真であるのは、Pが真であるか、「Pでない」が真であるかのどちらかである。しかし、Pの証明もPの反証も知られていない。よって、上の排中律は真ではない。実は純粋に論理的な部分だけに限って言うと、直観主義数学の論理は古典論理から排中律を除いたものになっている

直観主義数学はそんなに弱くない

しかし、排中律が成り立たないとすると、直観主義数学はとても証明能力が弱い数学ではないだろうか。というのも、排中律は背理法を成り立たせるために必要で、背理法は頻繁に数学の中で使われるからだ。

しかし、実はそうでもない。否定による解釈というものが知られていて、古典論理で証明可能な命題Pをある別の命題P’に翻訳すると、P’が直観主義の論理で証明できる。否定による解釈はたくさんのバリエーションがあるが、ここではゲーデルが考えたものを紹介する。

  • 原子命題(「ならば」などの論理結合子を含まない、それ以上分析できない文)pを二重否定文\neg \neg pに置き換える
  • または「a \lor b」を「\neg (\neg a \land \neg b)」に置き換える
  • 存在する「\exists xA(x)」を「\neg \forall \neg xA(x)」に置き換える

こうすると、解釈の前の命題が古典論理で証明できれば、解釈の後の命題は直観主義論理で証明できる。

特に、算術(自然数についての形式的な体系のことを数理論理学ではこう呼ぶ)では、証明は複雑なので略すが、原子命題について\neg \neg p \to pが成り立つ。直観主義論理ではp \to \neg \neg pが成り立つので、算術では原子命題についてはp\neg \neg pが等価である。よって実際には、上の解釈は単に「または」と「存在」を解釈し直したものとなる。また、算術の公理系には「または」や「存在」は明示的には含まれていない。よって、算術の公理に否定による解釈をほどこしても、やはり算術の公理になっている。

結局何がわかったかというと、Aが算術の古典論理による定理だとすると、Aの否定による解釈A’は算術の直観主義論理による定理になっている。A’はAと古典論理のなかでは等価であることに注意しよう。つまり、算術の範囲では、直観主義数学は古典数学と等価で、むしろそこにより細かい区別(構成的な選言と存在)を持ち込んだとみなすことができる。

同様の操作は高階の算術についても成り立つので、いわゆる19世紀的な古典的数学は直観主義数学で問題なくコードできる。(9/27追記:嘘です。)

ただし、20世紀的な集合論に基づく数学は、このような操作は少なくともそのままではうまくいかない。というのも、公理に存在「∃」が含まれているからだ。このあたりうまく行かせることはできないか、面白い研究テーマだと思う。

更に興味のある人は

直観主義数学の基本的な考え方は

  • Per Martin-Löf, On the meanings of the logical constants and the justifications of the logical laws
  • Per Martin-Löf, Intuitionistic type theory

を。後者は直観主義的型理論の解説でもある。

否定による解釈は論理学の教科書ならば載っていることが多いが、例えば

集合論の直観主義数学による解釈については

  • Peter Aczel, The type theoretic interpretation of constructive set theory

ZFの構成的バージョンであるCZFがITTで解釈できることを示している。CZFに排中律を加えるとZFになることも示しており、CZFの中で排中律がどこまで解釈できるか研究すると興味があるかもしれない。

直観主義数学の計算機科学への応用については

とか良い?