思弁的実在論は科学の基礎を与えるか II – 無矛盾律の導出について

フランスの哲学者メイヤスーの「思弁的実在論」が、主張されているように現代の科学の基礎を与えるものであるかどうか3回に分けて考える。今回は「事実性の原理」から「無矛盾律」を導くメイヤスーの議論を考え、「事実性の原理」が自己論駁的ではないか、という疑問を提出する。

以前の投稿

  1. 思弁的実在論は科学の基礎を与えるか I ‐ 事実性の原理の導出について

事実性の原理から無矛盾律へ

まずメイヤスーの議論を確認する。事実性の原理は次のようなものだった。

あらゆる事物そして世界全体が理由なしであり、かつ、この資格において実際に何の理由もなく他のあり方に変化しうる

(カンタン・メイヤスー「有限性のあとで」p94)

メイヤスーはここから、次の「非理由に関する2つの存在論的言明」を導く(同p115)。

  1. 必然的存在者は不可能である。
  2. 存在者の偶然性は必然的である。

そして、矛盾した存在者がこの言明に反することを主張する。というのも、矛盾した存在者Xがあるとすると、Xはあらゆる矛盾した性質が成立するから、もしXが存在しなくなったとしても、Xが矛盾していることによりXが存在していることも同時に導かれる。よってXは常に存在することになり、必然的存在者である。しかし、これは上の1.に反する。(同p119の議論を改変)

事実性の原理の自己論駁性

上記のメイヤスーの議論を明確化することは難しいと思うが、そのことにはとりあえず関わらないで、そのまま認めてしまうことにしよう。つまり、われわれは事実性の原理から無矛盾律が導かれると仮定する。

ところで、無矛盾律は必然的になりたつのだろうか?

もし必然的に成り立つのだとすると、これは事実性の原理に抵触する。と言うのも、無矛盾律も世界のあり方には違いないからである。事実性の原理によれば、世界のあり方はなんの理由もなく他のあり方、つまり無矛盾律が成り立たない世界に変化し得るはずである。

この難点を回避するには、2つの道があるように思う。一つは事実性の原理を存在論的言明に限定することであり、もう一つは無矛盾律の必然性を拒否することである。

存在論的言明に限定された事実性の原理

上記の事実性の原理の自己論駁性は、無矛盾律に事実性の原理が適用される、と考えたことから生じる。しかし、上記同p115ではメイヤスーは事実性の原理は存在についての原理であるかのように語っている。つまり、事実性の原理は必然的存在者を排除する原理であって、必然的命題を排除するわけではないと考えているようである。無矛盾律が何かの存在者の存在を主張するわけではないから、事実性の原理を存在論的言明に限定すれば、事実性の原理の自己論駁性は回避される。

しかし、存在論的言明だけでは十分な強さの無矛盾律を導くには不十分である。上記の無矛盾律の導出では、矛盾した対象はあらゆる性質を同時に持つとし、特に存在と非存在の性質を同時に持つとした。さて、「弱い」矛盾した対象Yを考え、Yは存在に関しては矛盾していないが、それ以外の性質についてはあらゆる矛盾した性質を持つとする。すると、Yに上記の無矛盾律の導出を適用することはできない。しかし、Yはほぼ矛盾した存在であり、このような対象が存在した状況を無矛盾律が成立しているということは難しいだろう。

なお、Yが性質Pとその否定を持つことから矛盾を導き、いわゆる爆発則からYの存在と非存在を同時に導くことが考えられるかもしれない。しかし、爆発則は無矛盾律を前提にしたものである。

無矛盾律の必然性

もう一つ、難点を回避する道がある。それは、無矛盾律が必然的に成り立つことを拒否することである。つまり、無矛盾律は今この世界では成り立っているが、次の瞬間には成り立たなくなり世界はカオスへと転落するかもしれない、と仮定する。

しかし、この仮定は上の1.に反する。というのも、1.は必然的存在者は不可能である、と主張している。よってどのような世界であっても、上の論証が成り立つ限り1.は無矛盾律を導いてしまう。つまり、無矛盾律は常に成り立つから必然命題である。

これを避けるには、必然的存在者はたまたま存在しないが、可能性としては存在する、と考えることはできる。しかし、必然的存在者が可能性としてのみ存在する、ということがあり得るだろうか。ある可能性のもとで必然的存在者が存在したとすると、それは必然的存在者であるからどのような状況でも存在してしまうのではないだろうか。

ややテクニカルだが、この疑問はS5という様相論理の体系では正当だ。S5の世界では、必然的存在者は存在する可能性があれば自動的に存在する。ただ、S5が成り立つかどうかは、メイヤスーが想定している必然性が何であるかに依存する。例えば、時間の問題に置き換えると、「時間にかかわらず存在する」といったものであればS5が成り立つが、「不壊性」のようなものであれば、不壊な対象がある時点で存在し始める可能性があっても、その時点以前では不壊な対象は存在しないかもしれない。

もう一つの問題として、そもそもメイヤスーの動機は祖先以前的な言明に意味を与えることだった。無矛盾律が必然的ではないとすると、これは可能だろうか。祖先以前的な言明を解釈するには、無矛盾律が人類が存在しないはるかな過去、人類が存在しなかったであろう世界線といったもの、要するに科学が言及するあらゆる事柄について無矛盾律が成り立つことが要求される。

すると、無矛盾律は無条件には必然的ではないかもしれないが、科学の領域では必然的である必要がある。これが事実性の原理の自己論駁を引き起こさないためには、事実性の原理が言及する必然性は無条件の必然性であり、科学の領域に関する必然性ではない、とするしかない。

しかしそうすると、今度は科学の領域においては無矛盾律の導出が機能しないことになる。というのも、無矛盾律の事実性の原理からの導出は、その領域において必然的な存在者ないし性質が存在しないことを前提にしていたからだ。これはメイヤスーの企てが失敗していることを示している。

まとめ

本稿では、メイヤスーの事実性の原理が自己論駁的ではないか、という疑いを考えた。また、この自己論駁性を回避する方法として、

  1. 事実性の原理を存在論的言明に限定する
  2. 無矛盾律の必然性を要求しない

の2つの方法を考えた。しかし、いずれの方法を採用したとしても、メイヤスーが要求するような、科学の基礎づけとなるような無矛盾律は得られないことを示した。

自分自身の無矛盾性が証明できる強い自然数の理論体系

通常言われるゲーデルの第2不完全性定理の内容はこうだ。

ある程度強い(正確にはロビンソン算術を含む)自然数(をコードできる)体系は自分自身の無矛盾性を証明できない

今日は、非常に強い自然数の理論体系(数理論理学の用語で「算術」と呼ばれる)で、自分自身の無矛盾性を証明できるものを与える。もちろん、上と矛盾しないように仕掛けがしてあるのだが、言いたいことは、第2不完全性定理の成立には体系の強さが問題であるかのような言い方は問題がある、ということだ。

2階論理と竹内予想

まず2階論理というものを導入する。これは通常の一階述語論理が量化(すべての〜について・ある〜が存在して)の範囲が個体であるのに対し、2階述語論理は個体の他に性質に対する量化が存在する。つまり

  1. 個体変数 x_1, x_2, \ldots
  2. 述語変数 X_1, X_2, \ldots
  3. 個体量化子 \forall^i, \exists^i
  4. 述語量化子 \forall^p, \exists^p

と関数記号、プリミティブな述語から命題が構成される。例えば、\forall X \forall x \forall y\ x = y \implies Xx \iff Xyなど。ただし、量化子の上のpiは今後省略する。

さて、推論規則はシーケント計算を用いるが、述語量化子については次のようにルールを変える。

\phi(\lambda x.\psi(x)/X)の意味は、φの中のどんなXtもψ(t)に置き換える、という意味だ。

2階算術の無矛盾性証明と竹内予想

さて、2階論理を推論に使う算術を2階算術と言う。2階算術はたいへん強い体系と考えれている。例えば2階算術は「古典的」な数学(集合論に訴えない19世紀的な数学)をそのままコードできる。また、証明論(証明の機械的操作について研究する分野)による解析能力をほぼ超えた理論であると考えられている。

2階算術の特徴は、数学的帰納法を明示的に公理としておく必要がないところだ。なぜかと言うと、次のような命題を定義する。

N(x) \equiv \forall X~[X0 \land \forall n(Xn \implies X(n+1)) \implies Xx]

この命題は、任意の0を含み、+1という操作で閉じている性質Xにxが含まれている、と言っている。このようなxに対して数学的帰納法を用いることができるのはすぐに分かるだろう。よって、ある自然数論の命題、例えばx+y = y+xN(x) \land N(y) \implies x+y = y+xと書き直すことによって、数学的帰納法を公理として立てなくても用いることができる。

さて、シーケント計算にはカットルールというルールがある。

名称未設定

一階述語論理では、このルールは不要だ。つまり、このルールがあってもなくても証明できることは変わらない。ただし、この性質(カット除去定理)の証明はそれなりに難しいため、最初はカットルールを入れておくことが通例である。

では、2階論理ではカット除去定理はなりたつだろうか。つまり、2階論理でもカットルールがあってもなくても証明できることは変わらないのだろうか。2階論理でのカット除去定理を竹内外史が予想したことから竹内予想と呼ぶ。

竹内予想は次のような意義がある。まず、\mathbf{Ax}をすべての算術の公理を∧で結んだものとしよう(ただし数学的帰納法は除く)。もし2階算術が矛盾していたとすると、\neg\mathbf{Ax}が純粋な2階論理の定理である。ところで、カットなしで2階論理を定式化できたとする。すると、証明の途中に現れる命題に述語量化子が含まれたとすると、それはその後除去することができない。一方、\neg\mathbf{Ax}は個体量化子しか持っていないのでそれはありえない。つまり、\neg\mathbf{Ax}は1階述語論理の定理となる。よって、1階算術がすでに矛盾しているはずである。

つまり、竹内予想は2階算術の無矛盾性を1階算術の無矛盾性に還元する。1階算術の無矛盾性は(頑張る必要があるが)2階算術の中で証明できる一方で、もちろん2階算術の無矛盾性は2階算術では証明できない。よって、竹内予想に2階算術の無矛盾性証明の難しさが含まれていることになる。

竹内予想はW. Taitにより証明されている(W. Tait, A non constructive proof of Gentzen’s Hauptsatz for second

order predicate logic, Bull. Amer. Math. Soc. 72(1966), 980-983.)ので成立する定理であるが、今でも竹内予想といわれることが多い。

カットなし2階算術とその無矛盾性

ここで、最初からカットルールなしの2階論理を使って証明を行う算術を考えよう。これをカットなし2階算術と呼ぶことにする。竹内予想により、カットなし2階算術は通常の2階算術と同じ定理を持つ。一方で、上の議論からカットなし2階算術が矛盾すると、1階算術も矛盾する。このことは2階算術の中で簡単に証明できる。一方、1階算術の無矛盾性は2階算術で証明できる。カットなし2階算術は通常の2階算術と同じ定理を証明するから、カットなし2階算術の無矛盾性はカットなし2階算術で証明できる。つまりカットなし2階算術は自分自身の無矛盾性が証明できる算術の体系である。

なぜ第2不完全性定理がなりたたないか

これは第2不完全性定理に反しているように見える。しかし、第2不完全定理は第1不完全性定理から、対象の理論TがLöbの条件と呼ばれる3条件

  1. T \vdash \phiならばT \vdash \mathrm{Prov}(\lceil \phi \rceil)
  2. T \vdash \mathrm{Prov}(\lceil \phi \to \psi \rceil) \land \mathrm{Prov}(\lceil \phi \rceil) \to \mathrm{Prov}(\lceil \psi \rceil)
  3. T \vdash \mathrm{Prov}(\lceil \phi \rceil) \to \mathrm{Prov}(\lceil \mathrm{Prov}(\lceil \phi \rceil) \rceil)

を満たしていることを仮定して導かれる。カットなし2階算術はこのうち2.が成り立っていない。細かく言うと、T \vdash \ldotsの右側は真なのだが、カットなし2階算術では証明することができない。というのは、\phi \to \psiの証明と\phiの証明から\psiの証明を得る簡単なやり方はカットルールを使うことだが、カットなし2階算術はカットルールを持たないためこのやり方が使えないからだ。カットルールを使わずに\psiの証明を得る方法は、実質的に竹内予想の証明と同じである。

教訓

最初に述べたが、第2不完全性定理は次のように紹介されることが多い。

ある程度強い(正確にはロビンソン算術を含む)自然数(をコードできる)体系は自分自身の無矛盾性を証明できない

これは誤りではないのだが、上記のように使う論理の定式化に手を加えると「強さ」を保ったまま第2不完全性定理が成り立たないようにできる。他方、「弱い」体系で不完全性定理が成り立たない例としてPresburger算術(足し算のみの算術)が挙げられる。Presburger算術は完全(その言語で記述できる任意の定理が証明可能)である。しかし、これは第1不完全性定理が成り立たないことに過ぎない。第2不完全性定理はPresburger算術でも成り立たない。というのは、掛け算を使わずにゲーデル数化を行うことはできず、Presburger算術の言語では無矛盾性をコードすることすらできないからである。

よって、第2不完全性定理の成立にその体系の「強さ」が問題であるかのように考えるのは不適切である。では他にゲーデルの第2不完全性定理を特徴づける簡単な性質がないかというと、「自己言及」しかないように思う。実際、自分自身の証明概念をコードしそれについての最小限度の性質が証明できる(自己言及ができる、と言っても良い)体系であれば、強さにかかわらず第2不完全性定理が示せる。そういう意味で、よく言われる「ゲーデルの不完全性定理は自己言及の限界を示している/自己言及により数学の限界を示した」はそれほど的はずれな主張ではない。

制御系の検証を強化学習を用いて行う

今日はFalsification of Cyber-Physical Systems Using Deep Reinforcement Learning(arXiv版)という私が共著した論文を紹介する。今年のFM(形式検証の国際会議)で発表されたショートペーパーだ。内容は、制御系の検証(必要な性質を満たしているか確かめること)を強化学習を使って行うというものだ。

制御系の検証は難しい。まず、制御の対象は普通物理系なので、微分方程式を解かないといけない。もちろん微分方程式を調べるにはいっぱい数学の理論があって、それを使えば良いわけだが、難しいのは今どきの制御系は往々にしてデジタルだ、ということだ。離散的にモードが変化したりする。こういう離散系と微分方程式が混ざったシステムはハイブリッドシステムと言われるが、解くのがとても難しい。

ハイブリッドシステムを検証する方法だが、完全な検証はごく単純なものしかできず、また計算も大変であることが分かっている。というわけで、普通にテストするしかないわけだが、複雑なシステムだとテストをデザインするのは難しいし、欠陥を見落としてしまうかもしれない。

そこで、自動的にテストを生成することが考えられる。特に、与えられた性質をシステムが満たさないことを示すテスト(反例)を探索することをFalsificationと呼ぶ。今回紹介する論文は、Falsificationを深層強化学習を用いてする手法を開発し、ベンチマークを行った研究である。

ロバストネスによる反例発見

いくつかの性質を考えよう。一つは安全性だ。出力の適当な不等式で書ける性質Pについて、「つねにPが成り立つ」が安全性だ。

ロバストネスによる反例発見とは、これらの性質にロバストネスという数値を定義し、ロバストネスを最小にするような入力を探索することにより反例を見つける手法だ。ロバストネスは、性質がどれだけロバストに成り立つかを表す数値で、マイナスになるとその性質は成り立たないように定義する。

例えば、Pを単純にy \leq cとする。ここでyは出力、cはある定数とする。このとき、Pについての安全性は\min c - yと定義される。定義から分かるように、ある時点でyがcを上回れば、ロバストネスはマイナスになる。

本当は安全性だけでなく、任意のMTL(Metric Temporal Logic)という論理式で書ける性質についてロバストネスが定義できるが、複雑になるので説明はしない。

いろいろな最適化技法(たとえば焼きなまし法)を用いてロバストネスを最小化する入力を探索する手法が、 Robustness guided falsificationだ。これまでいろいろな研究が行われてきたが、残念ながらまだ実用的な技術とは言えないだろう。一つの理由は、最適化の1ステップごとにシステム全体を最初から最後まで実行する必要があり、計算時間がかかってしまうからだ。他に、局所最適解に落ち込みがちという問題もある。

強化学習によるロバストネス最小化

そこで、最適化に強化学習を用いることを考える。強化学習はオンラインで、つまりシステムの実行が途中の状態で、学習を進め最適な解に近づくような入力を生成できるからだ。

しかし、問題がある。強化学習は\gammaは割引き率、r_iは時刻iでの利得とすると、

\sum \gamma^i r_i

の期待値を最大化しようとする。一方、ロバストネスは最小値により定義されており、合計ではない。

そこで、次のような近似を用いる。

\max (a_1, \ldots, a_n) \sim \log \sum_{i = 0}^n e^{a_i}

この近似を用いると、

\min c - y = - \max -(c - y) \sim - \log \sum e^{-(c-y)}

と書けるので、

\sum e^{-(c-y)}

を最大化すればよいが、これはe^{-(c-y)}を利得とする強化学習問題になっている。

実装と実験

実装は制御系のシミュレーションをMATLAB/Simulinkで、強化学習の実装はChainerRLを用いており、全体をPythonのスクリプトで結合している。対象にした制御系はHoxhaらの論文にあるものを用いている。(S-Taliroに付いてくる)。強化学習アルゴリズムはA3CとDDQN+NAFを用いた。

実験は9つの性質についてA3C, DDQNと比較対象としてS-TaLiroに実装されているSA(Simulated Annealing, 焼きなまし法)とCE(Cross Entropy法、クロスエントロピー法)を用いて実験を行った。それぞれの方法について、対象の系のシミュレーションを最大200回まで行ってよいこととし、200回シミュレーションを行っても反例が見つからなければ実験を打ち切ることとした。これを20回を繰り返し、200回以内に反例を発見できた割合(Success rate)と反例発見に要した回数の中央値(numEpisode)を求めた。また、入力データをどれくらいに時間刻みで変化させるかで違った結果が出るため、シミュレーション中の時間で1秒、5秒、10秒と時間刻みを変化させて実験をし、Success rateが最も良いもの、それで決まらなければnumEpisodeが良いものをそれぞれのアルゴリズム毎に選んだ。(ただし、実験によっては、1秒のものは何日かけても終わらなかったので省いてある)

実験結果を上の表に示す。ΔTは選ばれた時間刻みだ。横に示されたSuccess rateやnumEpisodeはベストなΔTのものである。黒字で示された数字は4つの手法間でベストなもの、*やがついた数字はベースラインと比較して(あるいは提案手法と比較して)差が有意である場合を示している。*はp < 0.05を、はp < 0.001を示している。

大雑把な傾向としては、強化学習の方が良い成績を収めていることが分かる。ただし、CEは性質によっては強化学習と匹敵するかそれを超える性能を出している。しかし、CEは性能が極端に悪い場合も多い。

課題

実は、強化学習を利用した実装は現状、大変遅い。ほとんどの実行時間がSimulinkのシミュレーターのものなので、これは強化学習の問題ではなく、PythonからSimulinkを呼ぶ方法に問題があるようだ。また、φ5のfalsificationが簡単すぎてバグがあるように見える。また、強化学習は生成した入力は階段関数になっているが、S-TaLiroはスプライン補間をしており、これは実験結果に影響があるかもしれない。

実装と実験データはこちらに公開されている。

https://www.dropbox.com/s/e1rxokcl8t7nw2c/RL.tar.bz2?dl=0

思弁的実在論は科学の基礎を与えるか I ‐ 事実性の原理の導出について

フランスの哲学者メイヤスーの「思弁的実在論」が、主張されているように現代の科学の基礎を与えるものであるかどうか3回に分けて考える。今回はメイヤスーの議論の核となる「事実性の原理」について、その導出を検討する。

思弁的実在論と相関主義

ここでは、思弁的実在論とは

対象の数学化可能な性質は…その性質は私がその対象と関係を持とうと持つまいと、私が思考するその対象の中に実際に存在している

(メイヤスー「有限性の後で」p13)

という立場を擁護するメイヤスーの議論のこととする。思弁的実在論という言葉は、ここから意味が拡大して、これまでの大陸哲学の人間中心主義的な傾向を批判すると称する哲学者一般を指すこともあるが、ここではメイヤスーの議論に意味を限定したい。

思弁的実在論が目指すのは、「相関主義」の批判だ。メイヤスーは相関主義を次のように定式化する。

相関主義とは、主観性と客観性の領域をそれぞれ独立したものとして考える主張を無効にするものである。私たちは主体との関係から分離された対象「それ自体」を把握することは決してできないと言うのみならず、主体はつねにすでに対象との関係に置かれているのであって、そうでない主体を把握することは決してできないということも主張する。

(同p16)

簡単に言うと、相関主義とは人間と独立した客観的事実はない、と考える立場である。一見客観的に見える科学的事実は、単に「権利上誰もが実験によって検証な可能な」(同p15)事実であって、(科学者)共同体の一致によって定義されており、やはりその存在が人間の存在に依存している。

メイヤスーは現代哲学はこの相関主義によって覆い尽くされていると考えている。分析形而上学などは実在論的な傾向が強いので、これは当てはまらないのではないかと思うが、それはここで議論したいことではないので省く。

相関主義批判 ― 祖先以前性の問題

メイヤスーはこの相関主義を批判する。批判の鍵になる概念が「祖先以前性」である。ある事実が祖先以前的とは「人間という種の出現に先立つ ― また、知られうる限りの地球上のあらゆる生命の形に先立つ ―」(同p24)ことを言う。現代の科学は例えば「地球は46億年前に誕生した」などの、祖先以前的な事実に関する言明を大量にしているのだが、そのような言明を相関主義は正当に解釈できるだろうか。

メイヤスーは、相関主義は「地球は46億年前に誕生した」という事実そのものを認めることはできないと考える。というのは、事実は人間とは独立したものではないからだ。そこで、相関主義に立てば、上の命題は「現在の科学者たちの共同体は、地球は46億年前に誕生した、と考えるに足る客観的な理由を持っている」と解釈される。(同p32を一部改変)

メイヤスーはこの解釈は「明らかに支持できない」とする(同p34)。科学者は「ある測定が科学者全員に対して妥当なものであるかを証明するために測定を行うのではない」(同p35)。もし地球形成年代それ自体が意味をもたない、とすると「測定の客観性は、意味も利得もない空っぽのものとなり、もはやそれ自身をしか指示しなくなる」(同p35)。

この議論が妥当であるかはここでは議論しないが、いずれにせよメイヤスーはある問題提起をする。それは「私達がいようがいまいが存在するものを知ること」(同p51)が可能であることを示す(メイヤスーによれば、過去2世紀の哲学がそのような可能性を否定していたにもかかわらず)という問題である。

事実性の原理

では、メイヤスーはどのようにして「私達がいようがいまいが存在するものを知ること」が可能であることを示すのか。それは「事実性の原理」というある原理が「絶対的」つまり「私達がいようがいまいが」成り立つことを示すことによって、そしてここに全科学を基礎づけることによってである。

では「事実性の原理」とはなにか。それは

あらゆる事物そして世界全体が理由なしであり、かつ、この資格において実際に何の理由もなく他のあり方に変化しうる

(同p94)

という主張である。当然に起こる疑問として

  1. このような主張がどのようにして絶対的に(つまり人間の存在と無関係に)成り立つと言えるのか
  2. この原理が科学の基礎にどのようにしてなり得るのか
  3. 何の理由もなく世界が他のあり方に変化しうるのなら、物理法則はどうなってしまうのか

などがありそうだ。1.に関しては今回の投稿で検討する。2.については、実際には人間とは無関係な「事物」が存在するということ、また無矛盾律(矛盾した主張は成り立たないという論理学の法則)をメイヤスーは導いているに過ぎない。これについては今後の投稿で議論する。3.をメイヤスーはヒュームの問題と呼んでいるが、この問題についてメイヤスーが与えている解決についても今後、論じていきたい。

相関主義から事実性の原理へ

では、メイヤスーは事実性の原理をいかにして(しかも人間の存在がその成立とは無関係であるやり方で)導出するのだろうか。

メイヤスーは死後の世界の存在に関する問題に置き換えてこの問題を論じる(同p95)。まずメイヤスーは死後の世界を認める論者と、認めない論者の二人を想定し、論争させる。次に相関主義者を登場させる。相関主義者によれば、そもそも私の存在しない世界についてなにか知ることはできない。よって、死後の世界の存在は決定不可能である。

しかし、この議論には疑問がある。というのも、この議論は死後には私は消滅すると仮定しているからだ。つまり暗黙のうちに死後の世界を認めない前提に立っている。というわけで新しい論者が登場する。「主観的観念論者」である。主観的観念論者は相関主義者の立場を批判してこう考える。私の存在しない世界は思考できない。とくに私が存在しない、という自体を思考することはできない。よって、私が存在しなくなるという事態も思考するはできない。よって、私は不死である。

もちろんこの議論は(特に相関主義者にとっては)受け入れがたい。相関主義者が主観的観念論者に反論するとすれば、よって「私が存在しなくなること」は思考可能でなくてはならない。そのためにメイヤスーが持ち出すのが事実性の原理である。

私は自分を、存在している理由を欠くものとして、このように存続している理由を欠くものとして思考している

(同p98)

つまり、「私の存在の理由のなさ」を私は思考している。「私が存在しなくなることがどんなことか」は思考できないが、「私が存在しなくなること」自体は、「私が存在している」ことの理由のなさを通じて思考している、というわけである。

しかし、ここで最後の論者である「思弁的哲学者」が登場する。思弁的哲学者によれば、この事実性の原理は単に我々の無知を表わしているのではなく、絶対的な(私の存在と無関係に成り立つ)ある事実を表わしている。それは「私の状態が他のどんな状態にでも変わるという、理由を欠いた可能性の移行」(同p99)である。したがって、私は全く理由なく任意に、存在することもできるし、消滅することもできる。これは私が知らないだけでなく、現実的な変化としてそうである。

なぜこう主張できるのだろうか。それは相関主義者が主観的観念論者に論駁するのが「私たちを無にしたり根本的に変化させたりできる<別様である可能性>を思考できる、という事実によって」 (同p99)である。この別様である可能性が私に相関的であることはあり得ない。というのは、この可能性には私が存在しない可能性も含まれており、この事実が私の存在に依存しているならば、このような可能性自体が成り立たないためである。

こうして、われわれは絶対的な事実、つまり「事実性の原理」にたどり着くことができた。

論証の検討

と、議論をたどってきたわけだが、これはどのような種類の論法だろうか。というのも、通常の演繹的な推論であるとは考えられないからだ。あらかじめ受け入れられた前提から出発する、というスタイルはとっていない。もちろん帰納的推論でもないし、アブダクションでもない。あり得るとすれば、ギリシャ的な意味での弁証法であると思う。つまり、相手の暗黙の想定を問答によって明示し、それに批判または同意を求めていくというスタイルだ。

つまり

  1. 有神論者 vs 無神論者 (最初の二人)
  2. 相関主義者(不可知論者) ― 死後の世界の可知性が前程されていることを指摘し、二人を批判する。
  3. 主観的観念論者 ―相関主義者が矛盾している、つまり私が存在しない世界の思考可能性を仮定してしまっていることを批判する
  4. 強い相関主義者 ― 主観的観念論者に私が存在する外部の理由がないことを指摘し、「私が存在する理由がない (事実性の原理)」ことの思考可能性から、私が存在しないことの思考可能性を主張する。
  5. 思弁的哲学者 ― 強い相関主義者が仮定する事実性の原理が、認識の可能性に関するものではなく、実際の可能性(形而上学的可能性)であることを指摘する。

しかし、この論法には問題があるように思う。ソクラテスが美について智者たちと問答し、結果として美を規定する本質が得られなかったという話がある。では、美には本質がないのだろうか。ソクラテスはむしろ智者と称していた人は本当は智者ではなく、美について無知だったと考えた。メイヤスーの問答では、相関主義者は相関主義者が受け入れがたい結論、つまり絶対的な事実の存在、を受け入れざるを得なくなった。このことは、事実性の原理が絶対的な事実であることの論証というよりも、相関主義者が智者ではなかった、つまりこの議論は単なる相関主義者の論駁である、と捉えることべきであるように思う。

ここでの疑いは、メイヤスーは簡単な誤謬推理に陥っているのではないだろうか、ということだ。つまり、背理法を試みながら、背理法の結論をそのまま議論の結論としてしまっているのではないか、という疑いである。

背理法とは、次のように行われる。まず反駁したい主張Xがあるとする。すると

  1. Xを仮定する
  2. YがXから含意される
  3. YはXに反する
  4. よって、Xは誤りである

と議論が進むのが背理法の一つの形である。しかし、簡単な誤謬推理として

  1. Xを仮定する
  2. YがXから含意される
  3. YはXに反する
  4. よって、Xに反するYが(無限定に、仮定抜きで)示された

というものがある。

メイヤスーの場合も次のような議論を行っている疑いがある。

  1. 相関主義を仮定する
  2. 事実性の絶対化が相関主義から含意される(同104ページ)
  3. よって事実性の原理が絶対的に示された

しかし、事実性の原理は相関主義とは矛盾するはずである。したがって、ここで言えたのは事実性の原理ではなく、相関主義が誤っていることの証明である。正しく背理法を用いると、

  1. 相関主義を仮定する
  2. 事実性の絶対化が相関主義から含意される(同104ページ)
  3. 事実性の絶対性は相関主義と相入れない
  4. 相関主義は誤りである

もちろん、メイヤスーが誤謬推理に陥っているとは、必ずしも断定できない。相関主義の主張の一部、特に「強いモデルの第2原理」(同p68)には同意しており、そこから事実性の絶対性を導いている可能性があるからだ。しかし、強いモデルの第2原理はあらゆる絶対性を否定しているのだから、これまた矛盾した主張にすぎない。メイヤスーは「事実性の絶対性」を「強いモデルの第2原理」に起源を持つものの、別個の考えとして提示しているのだ、と考えることもできる。例えば、素朴実在論や主観的観念論者を論駁する際には、ある種の「決断主義」を持ち出している(同p67, p104など)。これらをわれわれは取らないことにすると決める、というわけだ。しかし、これは何の議論にもなっていない。

私の個人的意見としては、相関主義者は最初から間違っており、死後の世界は実際に存在するかしないかのどちらかだと考える。また、メイヤスーが行っている議論は

  1. 何を知り得るか、という知識に関する様相
  2. 何が将来起こり得るか、という時間に関する様相
  3. 何が必然的に起こるか、という形而上学的な様相

の3つがややこしい仕方で混同されているように思う。

事実性の原理そのものの検討へ

今回は、事実性の原理の導出について検討した。次(の哲学テーマの投稿)では事実性の原理そのものが自己論駁的ではないか、という疑いについて論じる。

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つ目のドメイン、つまり間主観的な対象のドメインに入る。正義は人間社会に存在が依存している。

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

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

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

謝辞

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