価値相対主義に対するあまりうまくいかない反論

確かAeonマガジンで読んだと思うのだけど(正確な出典は見つけられなかった)、ある倫理学講師は倫理学の授業の初めに、倫理が相対的だ、あるいは存在しないと思う学生に手を挙げさせるそうだ。そして手をあげた学生を教室から追い出してしまう。そこで学生が抗議すると、講師は学生たちに、もし倫理が相対的なら彼らが抗議する基盤がないことを指摘する。そして、倫理を議論する基盤としての倫理学へと導入していくのだそうだ。

さて、この価値相対主義への反論はうまくいっていないと思う。学生たちは倫理は存在しないと思っているけれど、講師は存在すると思っている。そして多分講師の倫理規範には、学問的な場ではあらゆる主張が公平に取り上げられなければならない、が含まれているだろう。もちろん講師は相対主義者は倫理学の授業を受けるべきでない、と本気で思っている可能性もあるが、ここでの講師の振る舞いは相対主義を論駁しようとするものだから、もしそうだとすると論点先取だ。すると、少なくとも学生たちは講師の自己矛盾を突いていることになる。

あまり練れていない見解なんだけど、倫理はやはりどのような事実でも存在者でもあり得ないという意味で存在しないと思う。ウィトゲンシュタインが言うように「どんな道標も誤解されうる」から。もちろんウィトゲンシュタインは「通常の状態で機能する道標が道標なのだ」みたいなことを言っていて、これが常識倫理のようなものなのだろう。

Problems of Empirical Software Engineering Studies

Empirical studies are nowadays, mainstream approaches in software engineering research. This can be witnessed by the Google Scholar journal/conference ranking among the “Software System” subcategory. According to the ranking obtained on Jan 10, 2020, The journal “Empirical Software Engineering” has a higher ranking (7th) than “IEEE Transaction on Software Engineering” (8th), which is traditionally considered as the best journal in this field. Further, many presentations at other top conferences (ICSE, FSE, and ASE) are empirical natures and an emerging conference, MSR (“Mining Software Repositories”), precisely aims to empirical studies of software repositories which now wildly available thanks to Github and other alternatives.

So, what is wrong with this? Surely, Science is a study of empirical nature, isn’t it? “Induction” from the empirical data is a primary method of Science, isn’t it? However, the idea that Science is based on mere “induction” is a misconception.

Suppose we have data which suggest such, and such code metrics correlate the number of bugs. But is this correlation a fundamental/universal law? The correlation may depend on a particular programming language, programming paradigm, methodologies vogue only a handful of years, programming communities, application domains, etc. Of course, we can empirically study the factors which affect the correlation we just discover. However, whatever the results of further empirical studies are, we still have further doubt about universalities of these studies. This shows mere “induction” from data cannot prove any useful law.

Usually, most of (empirical, but not limited to) software engineering studies pose research questions based on a hypothesis. Then, these research questions are (in most cases) investigated empirically. For example, if someone thinks the length of function names affects the number of bugs, data from, say, a bug repository of Java programs are empirically studied, and the hypothesis is tested by statistical mean.

Unfortunately, a hypothesis considered by software engineering research is often “one-shot” in nature and does not form a systematic theory. Being a one-shot hypothesis, we cannot be sure about its scope, as stated above. Examining Java code repositories may not be sufficient, but there is no way to tell because of no background theory. Even a systematic theory is presented, they are not like theories of other fields of engineering in which rigorous mathematical formulations are employed. Therefore, rigorous verification nor falsification of a theory proposed is almost impossible.

Is there no way to improve this situation? I don’t think so, because the software has rich background theories. Software (development) has two aspects. The first aspect is that it is about computer programs. We have mature and rich mathematical theories of programs and their computation. Further, software development is all about the human being. Therefore, we can employ phycology, sociology, economics, and other social science and humanities to study software development.

An interesting (so I think) possibility: code mutation is widely used for a “proxy” of bugs introduced by human programmers. It would be interesting if we investigate the effects of code mutation on program behaviors theoretically, so we no longer rely on empirical data to understand the results of code mutation. Then, the task remained is empirically test the hypothesis that code mutation has similar behavior to human bugs.

科学に関する虚構主義と祖先以前性の問題

本論では、カンタン・メイヤスーが著書「有限性の後で」(人文書院2016年)で提起した「祖先以前性の問題」を、科学に関する虚構主義への批判と解釈し直すことを試みる。

メイヤスーの考える「相関主義」と祖先以前性の問題

メイヤスーは現代哲学を広範に覆うとされる「相関主義」を批判し、人間その他の認識主体の存在によらず成立する事実があることを「思弁的」に論証しようとする。相関主義とは

私たちは主体との関係から分離された対象「それ自体」を把握することは決してできないと言うのみならず、主体はつねにすでに対象との関係に置かれているのであって、そうでない主体を把握することは決してできないということも主張する。

(同p16)

立場であり、カントの批判哲学、超越論的現象学、生活世界論などを包含するとされる。本当にこれらの哲学上の立場がメイヤスーのいう相関主義に当てはまるのか議論があるが、本稿ではその問題には関わらない。しかし、「ある種の事実の成立にはかならず認識主体の存在が前提となっており、そのような事実が何らかの意味で本来的な事実である」と相関主義を定式化すれば、上記のような哲学的立場が通俗的に流布されるときに使われがちなまとめとして、また厳密には主張されてはいないかもしれないが背景にある考えとして、それほど的外れではないと考える。

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

メイヤスーが指摘するように、ほとんどの相関主義者は科学の言明の正当性を受け入れる。しかしそれは、分析哲学的な言い方をすると、虚構化オペレーターの内側に科学の言明を入れることによってである。

「出来事Xは人間の出現より何年も前に早く起こった」。(略)相関主義者の哲学者はーおそらく心の中で行うだろうがー簡単な遺言補足の但し書きのような、いつも同じものを、こっそりと文の最後につけ加えるだろう。すなわち、出来事Xは人間の出現より何年も前に早く起こったー人間にとっては(さらに言えば、科学者にとっては)

(同p29)

つまり、相関主義者は「科学というフィクションの中では『地球の誕生は46億年前であった』」と科学言明をパラフレーズすることにより、それを受け入れる。

しかし、これをメイヤスーは受け入れない。理由の一つは分析哲学で言われるところの「態度問題」である。科学者はフィクションを探求しているわけではなく、事実を探求しているのであり、そうでなければ科学の意義を説明できない。

しかし本論ではこの議論ではなく、同p37以降に展開される相関主義者のメイヤスーへの反論を論じるなかの議論を取り上げ、それをより形式的な形にまとめたい。

認識主体の存在の必然性と偶然性

まず、相関主義の主張を明確化しよう。メイヤスーはテキストにおいて明示していないが、相関主義者はなんらかの「直接的・本来的に有意味な言明の集合」を想定していると考えられる。ただし、ここで「言明」は広い意味での言明であって、実際に言語記号に基づいている必要はない。相関主義は、本来的に有意味な言明Pについて

  • Pならば認識主体Iが存在してIがPを認識する(相関主義の公準

を主張する。メイヤスーの上掲p16の引用ではPの把握だけが問題にも見えるが、それでは主張が自明になってしまうので、このようにまとめる。

これに対して、科学言明の多くは「直接的・本来的に有意味な言明の集合」に含まれてはおらず、ただそれらから何らかの意味で構成されたり検証されたりするだけの「概略的な所与」(同p30)である。本論では簡単のためPがSに含まれていると考える。というのも、科学は直接・本来的に有意味ではないかもしれないが、最終的には我々にとってのある種「直接的に与えれた」所与についての何らかの言明を行うと考えられるからだ。相関主義者は科学の主張を受け入れるから

  • 本来的に有意味な言明Pを科学が主張するならば、P(移行原理)

を受け入れる。

さて、祖先以前的な言明、例えば「生命はRNAの偶然的な組み合わせから発生した」を考えよう。メイヤスーによればこの言明のポイントは、この言明の持つ所与からの「隔たり」でもなければ、同時にこの事実を観測する主体が存在しなかったことでもなく、「所与それ自体が非存在から存在へと移行する時間」(上掲p41)という問題を提起することである。とはいえ、このメイヤスーの言明は簡単には理解しがたい。というのは、我々はすでに所与が存在している時点に生きているからである。そして、相関主義者は、所与が存在する以前には、厳密には事実は存在しなかったと考えている。ここには矛盾はないように思える。

我々はこう考えたい。所与それ自体が非存在であった時があったすれば、そもそも所与は与えられなかった可能性があるということである。例えば、ビッグバン時の時空の膨張速度がわずかに違えば、認識主体はこの宇宙に存在し得えなかった、といったような。我々は、祖先以前性の問題は、それが過去に関わるからではなく、認識主体が偶然的な起源を持つこと、よってその存在は偶然的であることをしめすことだと考える。

さて、科学が認識主体の存在が偶然的であることを主張することは、どのような帰結を持つだろうか。もし認識主体の存在は直接的に把握可能な事実であると思われるので、移行原理は認識主体の存在が偶然的であることを示すように思われる。

その一方、相関主義の公準はトートロジーであれ何であれ必然的な事実が存在する限り、認識主体の存在は必然的であることを示しているように思われる。よって、相関主義の公準と移行原理は両立し得ない。

科学の様相と根源的な様相

この結論から逃れる一つの方法は、偶然性や必然性にかんする言明には移行原理は適用できない、とすることだ。科学における偶然性や必然性は、本来的な意味での偶然性や必然性とは関係ない、と考えると上記の問題は回避できる。

しかし、この解決は行き過ぎた結論を導くように思われる。例えば次のような科学的言明を考えよう。

  • 高電圧電流に触れると死亡する

この言明は厳密含意であり、必然性を述べている。しかし、偶然性や必然性についての言明に移行原理を適用しないのだとすると、この言明から

  • この(今目にしている)高圧線に触れると、死の危険がある

という推論を行うことができない。それどころか、なにか本来的に有意味な必然性命題がある限り、相関主義の公準から認識主体の存在が必然的であることが導かれる。私は高圧線に触れても死なないのである。この立場は、メイヤスーの言うところの「主観的観念論」(同p97)である。

このような立場に対するメイヤスーの批判は同p46以下で展開されている。一言でまとめれば、主観的観念論は超越論的主観性の「受肉」の可能性の問題を引き起こす。次のような言明を考えよう。

  • (かくかくしかじかの)脳活動が行われていれば、その生物は超越論的主観性を持つ

これはやはり厳密含意である。しかし移行原理が適用できないことから、ここから

  • 人間は超越論的主観性が存在する

を導出することができない。

これは一見、反自然主義者であれば好ましい状況であるように思われる。しかし、問題は移行原理が適用できないことにより、両者が全く無関係になることである。したがって、意識活動に相当する脳活動が存在するにもかかわらず、超越論的主観が存在しないこともありえてしまうし、頭におがくずが詰まっているのに超越論的主観性がある、という状況もありえる。

したがって、メイヤスーの祖先以前性の問題は相関主義者にたいして、少なくとも様相に関わる移行原理の明確化という課題を提起しているように思う。

まとめ

本論では、メイヤスーが提起する「祖先以前性の問題」についてのある種の解釈を提起した。この解釈では、メイヤスーの議論は認識主体の存在を必然的に含意する「相関主義の公準」と、認識主体の存在の偶然性を含意する「移行原理」からなる。この2つが両立しないことから、科学に対して虚構主義的な解釈を行う相関主義を批判した。さらにこの問題を回避するため様相命題が移行原理の対象にならない、という仮定を検討し、この問題は超越論的主観性の受肉の条件を説明できない、という難点がある。

思弁的実在論は科学の基礎を与えるか 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つがややこしい仕方で混同されているように思う。

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

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