Asinus's blog

西牟田祐樹のブログです。

早すぎたアイデア: W. Kneale & M. Kneale, "The Development of Logic"を読む

数理論理学 線形論理

W. Kneale & M. Knealeのアイデア

W.Kneale & M. Kneale, The development of Logic, Clarendon Press, 1962という論理学史の本についてほとんど知られていないであろう内容を書き記しておく1。

この本は古代ギリシアからヒルベルト辺りまでを詳細にカバーしているという恐るべき労作である。そしてこの本には現代論理についても出版当時ではオリジナルであったアイデアを少なくとも一つ含んでいた。

それは彼らの作った自然演繹のシステムについてである。以下のような推論規則を持っている。

Kneale&Knealeの自然演繹 (p.542)

私が指摘しておきたいことはこの(5)と(6)の規則は後に線形論理で使われることになる推論規則と同じ形をしているということである。1987年の線形論理最初の論文で創始者であるジラールは次のような推論規則を用いている2。

古典線形(命題)論理の推論規則 (p.22)

用いている記号は異なるが、Logical Axiomsは(5)に対応し、Cut ruleはコンテキストとなる変数を取り除くと(6)に対応する。Kneale達の*は何もないことを示しているようである。

推論規則を図的に表現したproof-netsというものを見ると類似性はさらにはっきりとする。(5)と(6)の推論線をlinkと呼ばれる辺のように書くと次のようになるだろう。

proof-netsでの表現

実際にproof-netsは線形論理の自然演繹と考えられている3。

https://www.sciencedirect.com/science/article/pii/0304397587900454

この類似、そして両者が結論複数の自然演繹のようなものを考えたのは偶然だろうか？そうでないことをこれから見ていく。

ジラールの発想

ジラールは2010年のサーヴェイ

https://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=&ved=2ahUKEwix2I-i-qrwAhUBMN4KHT-nD5AQFjACegQIBhAD&url=http%3A%2F%2Fgirard.perso.math.cnrs.fr%2FSynsem.pdf&usg=AOvVaw3CwjsPOLpjXzlB1BBDxtZZ

で自然演繹の限界として重要なものに限ると以下のことを指摘している。

  1. 古典的な(古典論理の)対称性を扱えていない。これは自然演繹では結論が高々一つに限られるということが原因である。

  2. 含意の導入規則と選言の除去規則は論理式ではなく、証明全体に適用されるので規則がグローバルなものとなっている。(つまり規則を適用するためには直前の前提だけではなく証明図の全体を確かめなければならない。)

  3. 選言の除去規則では結論に前提には現れていない論理式(e.g. C)が現れている。このことによって正規化のcommutation stepが複雑となる。

上のジラールの用いた推論規則で論理式がすべて \vdashの右側に集められていたのは1.の対称性により否定の規則を使って論理式を後件(または前件)にいつでも移動させることが可能だからである。

ジラール共著の"Proofs and Types"

https://people.mpi-sws.org/~dreyer/ats/papers/girard.pdf

では10.1 "Defects of the system"(自然演繹の欠点)で選言除去規則の代わりとなる素朴な別の推論規則例として A \lor B/ A B を挙げている。これはKneale達のアイデアと一緒である。

実際古典線形論理で素朴に自然演繹を考えようとすると乗法的選言("&"をひっくり返したもの)の良い規則を見つけることができない。

線形論理はこれらの欠点を克服する論理として提示されている。

W. Kneale & M. Knealeの発想

これを踏まえKneale達の発想を見ていく。Kneale達はゲンツェンの自然演繹はフレーゲやラッセル&ホワイトヘッドの論理体系よりも自然であると評価しつつも(p.539)、選言の除去規則、否定の導入規則、含意の導入規則、存在の除去規則はある仕方で他の規則に依存しているとして扱いづらい点があると評価している(p.540)。これはより明確にするならばジラールの指摘する限界の2.に該当すると理解できる。グローバルな規則はその内に他の規則が現れるので間接的に他の規則に依存していると考えることができる。Kneale達は、なぜゲンツェンはこのような複雑な仕組みを導入したかということを考察している。そこで正しくも連言と選言の規則に着目することで自然演繹が結論を一つしか持てないことを複雑さの原因として述べている4。

ここで注目すべき点はKneale達はthe algebra of logic (論理代数)では連言と選言が双対であることに注意し、ゲンツェンの選言除去規則が連言の導入規則と双対的になっていないことを述べている5。これはジラールの指摘する1.に該当する。algebra of logicはVI. 3 Boole and the Algebra of Logicの章で扱われており、そこでの古典的な双対性の観点をKneale達は自然演繹に突き合わせている。これは彼らが論理学の歴史的内容を単に収集しただけではなく、そこから得た視点を別の論理体系を考察する際に利用するという作業を行なっている査証である。そしてその上で双対となるような自分たちの自然演繹を提示している。

ジラールの指摘する3.については必ずしも満たされていない。Kneale達の(7b)ではPとQは無関係であり得る。もちろん選言の除去規則は3.を満たしている。

これらより、類似は偶然ではなく、自然演繹の持つある意味では不自然な点を両者は克服しようとして類似したモチベーションから両者は一部では類似している仕組みを作り出したのである。しかし作り出した体系の出来には雲泥の差があり、Kneale達の体系には致命的な欠点があった。

なぜ早すぎたのか

推論規則の組み合わせに問題があり、この体系で矛盾と任意の論理式を導出することができるからである。もちろん通常の自然演繹と証明能力が同等とはならない。 (7.a)で \botと \bot\to\botを始式として、(8)で \botを導出することができる6。さらに同様に含意の導入の後に除去を行うことで(Qとして)任意の論理式Aを結論することができる。よって体系は潰れており、含意の規則には問題があると言わざるを得ない。

何が不足していたのだろうか？ Prawitzによる自然演繹の研究がまだ出版されておらず、反転原理(inversion principle)を知らなかったことであるだろう7。

この不足によってどのような推論規則を採用すべきかについての十分な考察が困難であったという点で彼らのアイデアは早すぎたのである。

複数の結論がある自然演繹のアイデアはmultiple-conclusion natural deductionとして後に実現されることになる8。ただし独立に発見されたものであり、W. Kneale & M. Knealeの姿はそこにはない。

  1. 以下の論文にわずかに言及がある。
    Olivia and Queiroz, Geometry of Deduction Via Graphs of Proofs, in Logic for Concurrency and Synchronisation, Springer, 2003, pp.3-88.↩

  2. この記事で用いた図はすべてそれぞれの本あるいは論文から引用したものである。線形論理には後件を高々一つの論理式に制限したものである直観主義線形論理があるので古典線形論理と書いている。↩

  3. “Since the framework is classical, it is necessary, in order to get a decent proof-theoretic structure, to consider proof-nets which are the natural deduction of linear logic; ie a system of proofs with multiple conclusions, which works quite well.” (p.3).↩

  4. “Gentzen’s system seem to be forced on him by the obvious fact that an inference cannot have more than one conclusion thought it may have two or more premises.” (p.540).↩

  5. “The answer can be found from a comparison between the rules for conjunction and those for disjunction. It is well known that in the algebra of logic the conjunction and disjunction signs are dual to each other, and yet rule (4), which provides for elimination of the disjunction sign, does not correspond to rule (1), which provides for introduction of the conjunction sign, …” (p. 540).↩

  6. 他の方法でも矛盾を導出することができる。↩

  7. もう一つはW.Kneale & M. Knealeの頃にはまだ構造規則、つまりweakening規則とcontraction規則、に対する研究の蓄積が(十分に)なかったことである。論理学の歴史的研究の内にひっそりとアイデアが提示されていたことにより彼らの体系の重要性は見過ごされた。↩

  8. Branislav R. Boričić, On Sequence-Conclusion Natural Deduction Systems, Journal of Philosophical Logic, vol. 14, No.4, 1985, pp. 359-377. 選言の規則はKneale達と同じだが、含意の規則はゲンツェンのものと同じとなっている (p.367)。なのでKneale達のモチベーションの元では2.が満たされておらず受け入れられない。↩