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の中で排中律がどこまで解釈できるか研究すると興味があるかもしれない。

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

とか良い?

ソフトウェア工学に文句をつける

本稿ではソフトウェア工学の論文を1つ例として取り上げ、その内容に文句をつけたいと思う。取り上げる論文は、ソフトウェア工学の論文としてきちんとしたもので、ソフトウェア工学のトップ会議の一つであるISSTAで発表されたものである。

Milos Gligoric et al., Comparing non-adequate test suites using coverage criteria, ISSTA’13

PDF

論文の解説

ソフトウェアがちゃんとできているか、確かめるよくあるやり方はテストである。ソフトウェアにやってきそうな入力をいくつか用意し、実際にソフトウェアに入力してみる。そしてその結果をみて、ソフトウェアが期待通りに動くか確かめる。

ここで問題は、あらゆる可能な入力に対応するテストを用意することは、ほとんどの場合、不可能であるということだ。というのも、ソフトウェアが受け付ける入力の数は膨大なものになってしまうことが多いので。

というわけで、不完全なテストの「良さ」を評価するために「カバレッジ」という概念が登場する。ソフトウェアテストのカバレッジの概念は多数提案されていて、例えば

  • コードカバレッジ:テストによって実行されるコード(例えばプログラムの文)が全体のどれだけか。この論文ではステートメントカバレッジと呼んでいる。
  • ブランチカバレッジ:プログラムの中に含まれる分岐のうち、どれだけが実行されたか
  • パスカバレッジ:プログラムの中に含まれる実行パスがどれだけ実行されたか

などなど。これらのカバレッジ基準によって、テストが評価できる…わけだが、評価基準がたくさんあるので、評価基準自体の評価が必要になる。それをしましょう、というのがこの論文。ただし、カバレッジ基準が完全に満たされている(100%のとき)場合は先行研究があるので、基準が完全に満たされない場合を考えた、というのがこの論文の新しさ。カバレッジ基準が100%満たされることはめったにないので、この論文のやっていることは意義が大きい。

さて、どのようにカバレッジ基準の妥当性を評価するか。テストは究極的にはバグを見つけるためのものなので、そのテストがバグを発見できる確率とカバレッジ基準の達成度合いの相関を見る。バグは人為的にコードをランダムに変化させることにより生成する。テストによるランダムな生成によるバグの発見率と、人間が作るバグの発見率は、相関していることが知られているので、このような評価で問題ない。

さて、この論文の結論は本稿の目的とはあまり関係ないが、一応書いておくと、ブランチカバレッジが、他の複雑な基準を押しのけて、一番良い。ただし、テストが十分行える状況ではAIMP (acyclic intra-method paths)カバレッジという基準が良いらしい。

文句をつける

さて、この論文、動機づけも明確で良いし、実験もきちんと行われていて興味深い結論を引き出している。考察も示唆的だと思う。良い論文だと思う。

それでも文句をつけたくなる。

  1. 理論的な基盤の欠如:この論文の結論の正当化には、直感に訴えた議論はあっても理論的なものはない。
  2. 特定のデータセットやツールに依存している
  3. 特定の言語(Java)とプログラミングパラダイム(オブジェクト指向言語)に限定された研究である

ランダムなバグを検出するのにどのようなテストを行えばよいか、というのは原理的には純粋に理論的な課題なはず。もちろん実際は難しいかもしれないが、近似的な議論とか、なにかできないのだろうか。大量なデータを用いた経験的な研究を行うのが最近のソフトウェア工学研究のトレンドだが、理論的な正当化が不十分であるように思う。そして、理論的な正当化が不十分であるために、次に述べるように、結果の一般性に疑念が生じる。

2.は言いがかりのように聞こえるかもしれない。実験をする以上、何かのデータセットやツールに依存せざるを得ないのは明らかではないだろうか。しかし、ソフトウェア工学分野の研究では、比較を公平にするためもあるのだろうが、同じデータセットやツールが複数の研究で繰り返し用いられている。つまり、研究分野自体が特定のデータセットに過学習しかねないように思う。

さらに言えば、現在のソフトウェア工学のほとんどがJavaプログラムを対象にしている(CやC++が対象になることもある)。これは不健全な状況だと思う。別のプログラミング言語やパラダイムが主流になったとき、またすべての研究を一からやり直すのだろうか。

ではどうすればよいか

あまり大した提言はできないのだが、まず大量データを解析して経験的に結論を下すだけではなく、なぜそれが成り立つか、理論的な考察が必要だ。理論的な考察があって初めて、得られた結果が一般性を持つのかどうか、異なったプログラミングパラダイムに適応可能か、といったことが分かるはず。

もう一つは、Javaだけではなく、異なった言語・パラダイムの研究を行うべきだということ。静的型付けがあるのとないのとではどう違うか。型推論はどのような影響を与えるか。オブジェクト指向と関数型言語ではどう違うか。などなど。

まあ、お前がまずやれ、という話になりそうだが…

正義の実在性について

 

正義の実在性のある論証

本稿では「正義が実在する」という主張を考える。実在するとは、人間から独立して存在する、ということとする。また「存在する」がどういうことかはここでは深く考えないことにする(が分析形而上学の「標準理論」によって、我々がコミットしている理論の量化の範囲に入っているもの、と考えてもらって良い)。また、実在する、という立場に対立する立場として、唯名論(人間の作り出した単なる名前に過ぎない、つまり名前が指す実体はない)という立場を考える。

正義の実在性を主張する論拠はいろいろあるが、ここで考えてみたいのは次のような議論だ。

もし正義が実在せず、単なる記号であるとするなら、そのような正義に従おうとする人々の気持ちは薄れてしまうだろう。つまり正義の正当性が毀損されてしまう。よって正義は実在する。

しかしこの論証にはいくつかの問題がある。

問題点1 – 規範言明からの事実言明の導出

まず、「正義は従われなければならない」という規範に関する言明から「正義は実在する」という事実に関する言明を導いている、という問題がある。通常、規範に関する言明と事実に関する言明は独立していると考えられる。例えば、「殺人はあってはならない」から「殺人は存在しない」は導かれない。「人は猿から進化した」と考えると人間の尊厳が失われるから、進化論は誤りだ、という主張もそうである。上述の議論は、これらと同様の議論の構造を持っている。

問題点2 – 「実在」と「存在」の混同

また仮に、もし「正義は従われなければならない」から「正義は存在する」が導かれたとしよう。しかし、「存在する」から「実在する」は必ずしも導かれない。「正義は存在するが、人間社会にその存在が依存している」だとしても、人々が人間社会の存在を重要視している限り、その重要性は毀損されないはずである。

問題点3 – 「実在」と「不変性」の混同

ではなぜわざわざ「実在している」と主張しないと、正義が毀損されてしまうように感じるのだろうか。おそらくここで「実在」と「不変性」が混同されている。つまり、正義の存在が社会に依存しているとすると、社会が有り様を変えれば、正義は変わってしまうように思われるし、もしかすると、社会の恣意的な決定によっても、正義が変更されるように感じられる。そのような正義にはコミットする気が起きないかもしれない。

確かに、例えば人間社会に存在が依存しているとすれば、人間社会が消滅すれば正義は消滅することになる。しかし、人間社会が消滅した未来で正義が毀損されたとしても、何も問題はないであろう。一方で、正義が人間社会に存在が依存していることは、正義の中身が人間社会の意のままに変更できる、ということではない。例えば、私が自転車に乗るスキルは、私にその存在が依存している。しかし、一旦獲得されたこのようなスキルは、原則として忘れられることはないし、変更も効かない。同様に、私の母語に関する知識などもそうであろう。

間主観的な対象としての正義

さて、「正義は実在である」という議論を批判してきたわけだが、では正義はなんなのだろうか。ここでは存在を、存在が主観に依存する主観的対象、複数の主観に依存する間主観的な対象、そして主観に依存しない客観的な対象の3つのドメインに分けようと思う。(このような考えは哲学では歴史あるものだと思うが、誰によって広められたかよく分からないので、教えてほしい。ドメインという言葉は生物学から借りてきた。)明らかに、正義は2つ目のドメイン、つまり間主観的な対象のドメインに入る。正義は人間社会に存在が依存している。

さらに、正義は唯名論的に理解できると思う。つまり、人間社会があって、一定の仕方で「正しい」という言葉を使っていたとすると、それで人間社会に正義の概念を帰属するに十分である。記述の便法として正義という存在者を仮定してもよいが、究極的には記号とその運用能力だけを仮定すれば良い。

このような仮定をおいたとしても、正義にコミットする動機が失われるわけではない。正義が人間社会の存続に不可欠である限り、また人間社会の存在にコミットするべきである限り、正義にコミットする動機が存在する。

一応追加で述べておくと、正義の存在論的身分にかかわらず、正義にコミットしないことを決めている「ニヒリスト」を想定することができる。このような人にとっては、正義は最初から毀損されており、正義の実在論は無力である。

謝辞

本稿は阿蘇の史さんとの個人的議論から出発している。ここに感謝する。もちろん内容はすべて私が責任を負うものである。また、分析形而上学については倉田剛「現代存在論講義」を参考にした。