(最近、精神的に疲労困憊し、しばらく寝込んでしまいました。不安を和らげる薬を生れてはじめて飲んで、心を落ち着かせようとしているところです。以下に掲げる文章は、寝込んでしまう前に大部分を書きました。ただし心穏やかでない時期に書いておりますので、推敲を経ておりません。そのため、ほとんど思い付きと言ってよいような文章です。間違っておりましたら大変すみません。)
Unrestricted Comprehension Principle を保持したまま、Russell Paradox からの矛盾導出を防ぐ手段として、structural rules の一つを落とすということが、有望な手立てとして考えられています。その落とされる structural rules の一つには例えば contraction があります。これを落とせば確かに矛盾の導出は block できます*1。
しかし、直観的には contraction は当然成り立つと思われる規則ですので、これを落として推論規則としての使用を全面的に禁止してしまうことには心理的抵抗を感じます。
とはいえ、心理的抵抗を感じるとしても、contraction がないことに慣れてしまえば、心理的抵抗も減じ、痛痒を感じなくなるでしょうから、あえて contraction を落としてしまうことを厭わない方々もおられるかもしれません*2。
ですが、心理的抵抗を感じようが感じまいが、contraction を落とすことによって、contraction 以外の重要な実質をも失われてしまうことになるのならば、話は別です。
Stephen Read 先生によると、contraction を落とすと、(直観主義的観点からの) 背理法*3も失われ、その証明法を使用することの正当性が失われるとのことです。
直観主義的観点からの背理法とはいえ、背理法の一種とされるものが使えないとなると、これはゆゆしきことかもしれません。
けれども、contraction を落とすと背理法も使えなくなるという Read 先生の主張は、私の考えでは間違っていると思います。ですので、contraction を落としても、Read 先生が言うように背理法が使えなくなるということはなく、失うものはないと思われます*4。
しかし、先日何気なく次の文献の conclusion の section を眺めていると、(かつその section だけを読んでいると)
- Seiki Akama and Sadaaki Miyamoto ''Curry and Fitch on Paradox,'' in: Logique et Analyse, vol. 51, no. 203, 2008,
ちょっと驚くことが書いてありました。そこに書かれていたのは、contraction を落とすと二つの大切な事柄が失われる、という話です。私は特に二つ目の事柄が失われることに驚いてしまいました。昔からよく知られていることなのかもしれませんが、不勉強なため私は知りませんでしたので、読んでいてちょっと不意を突かれたような気がしました。
長くなりますが、Section 5, Conclusions, pp. 280-281 の部分と、文献情報 pp. 282-283 の部分を引用してみます。私が上に述べた、失われてしまう二つの大切な事柄とは、下記引用文中では、初めの辺りで 'two problems' と呼ばれているもののことです。
Contraction-free logic, which belongs to the family of the so-called substructural logics, can generally act as a formal ground of naive set theory. There seem at least two problems. One is that in naive set theory based on contraction-free logics the defined notion of a ''set'' using comprehension schema is not a set but a multiset (also called bag) due to the lack of contraction.
As is well known, in set theory, the set {a, a, b} is considered equivalent to the set {a, b}. In other words, duplication of elements plays no role here. On the other hand, the multiset {{a, a, b}} is not equivalent to the multiset {{a, b}} in that duplication of elements is meaningful. From a logical (or computational) point of view, duplication is closely related to the notion of resource. For example, Girard's [9] linear logic is also regarded as a contraction-free logic to handle resource as a multiset. This seems to reveal that intuitive theory of element and collection is based on multiset theory rather than set theory. From a different point of view, such an observation may lead us to work out a foundation for multiset theory based on contraction-free logics; see Bunder [5] for details.
The other problem, which is also related to the first conceptual difficulty, is that we cannot define induction principle with implications not satisfying contraction. Induction can be expressed as the formula of the form (A(0) ∧ ∀n(A(n) → A(n + 1))) → ∀nA(n). A natural deduction proof of the formula representing induction is to prove the formula of the form (A ∧ (A → B)) → B. We here omit applications of (∀E) and (∀I) for simplicity. The proof requires the use of contraction as illustrated as follows.
Here, the last step of (→ I) discharges two occurrences of the assumption A ∧ (A → B), but it violates the restriction on (→ I) mentioned above. This implies that induction does not hold in naive set theory based on a contraction-free logic. We believe that induction is one of the important principles for mathematics, and we are not right to discard it. Of course, to accommodate to the obstacle, we could introduce another implication for induction satisfying contraction, but it appears ad hoc (cf. White [21]).
[5] Bunder, M.: BCK-predicate logic as a foundation of multiset theory, University of Wollongong, 1985.
[9] Girard, J.-Y.: Linear logic, Theoretical Computer Science, 50 (1987), 1-102.
[21] White, R.: The consistency of the axiom of comprehension in the infinite value predicate logic of Lukasiewicz, Journal of Philosophical Logic, 8 (1979), 509-534.
数学的帰納法を式で表した場合、その式を証明しようとすると contraction が必要になってくることが、上記引用文中の証明図により、一目瞭然です。びっくりしました。Contraction がないと数学的帰納法を正当化できないのでしょうか？ もしも本当にできないのだとすると、これは計り知れない損失になりそうです。Contraction を落とすことは、そう軽々しくはできないことになりそうな感じですね。これはまいったな。
しかし、もしもですが、もしも contraction がなくても上記の数学的帰納法の式を証明できるとしたらどうでしょうか？ あるいはさらに、そもそも上記の式を証明できないとしても、公理として立ててしまえばどうでしょうか？ そのようなことも考えつくかもしれませんが、おそらくそれは無駄なあがきになるかもしれません。
というのも、問題の式を 'MPA' と名付けて、もう一度書き出してみますと、
MPA: (A ∧ (A → B)) → B
ですが、これを見て私は思い出したのですけれど、これは結構有名な式だと思います。Relevance/Relevant Logics に詳しく、かつこの論理に基づいて、素朴集合論や素朴な真理論を展開しようとされている方ならば、みんな知っている式だろうと思います。つまり、昔から Modus Ponens Axiom とか Assertion と呼ばれてきた式です。
この式を証明したり、またはこの式を公理として立てている論理では、この式と、あとわずかな論理的装置で、あっと言う間に Curry's Paradox が再発してしまうことが大分前から知られています。
ですから、上記の式 MPA があると、その理論は Curry's Paradox によりどんな式でも証明できてしまうので、理論的価値を失ってしまいます。*5
私たちは dilemma を突き付けられているのでしょうか？ すなわち、一方で、問題の式を証明するなり公理として立てるなりして、手に入れることができなければ、数学的帰納法が失われてしまうのかもしれません。他方で、問題の式が手に入ったとしても、それなりの強さを持った理論では、Curry's Paradox が再発して、trivial なものとなってしまうのかもしれません。
どうしたらいいのでしょうか？ どうしたらいいのか、ちょっと考えてみます。と言っても、私に答えなど出そうにありませんが…。
ここまで書いた後で、次の論文を眺めていると、とても興味深いことが記されていました。
- Graham Priest ''Old Wine in (Somewhat Leaky) New Bottles: Some Comments on Beall,'' in: The Australasian Journal of Logic, vol. 13, no. 5, 2016.
この論文の pp. 90-91 を見ると、MPA と contraction が deductively equivalent であることが簡略な形で証明されています。ここでその証明の詳細を私のほうで補って自然演繹を使って掲げてみましょう。なお、pp. 90-91 では MPA が PMP と呼ばれています。またその証明ではいくつかの論理的真理が援用されています。
一枚の証明図にすると大きくなりすぎるので、分割して証明します。まず、
(1)
<1> が出ました。次に、
(2)
<2> が出ました。これで <1> と <2> を合わせて条件法除去則により、以下のごとく A → B が出てきて、
(3)
(1) の右上にある [A → (A → B)] を落とし、条件法を導入すれば、(3) のごとく Contraction の証明の完成です。
ここでも分割して証明します。まず、
(1)
<1> が出ました。続いて、
(2)
<2> が出ました。最後に、<1> と <2> を合わせて条件法を除去すれば、((A → B) ∧ A) → B が出て、
(3)
(1) の二つの [(A → B) ∧ A] と (2) の一つのそれを落とし、条件法を導入して、それから推論規則として Contraction を使えば、MPA/PMP である ((A → B) ∧ A) → B が導出されます。
Contraction から MPA/PMP の証明では、contraction が公理ではなく推論規則として使われていますが、公理としても証明可能です。しかしそのようにすると証明図が大きくなりすぎて、ここに収めるのが大変なので、便宜上、推論規則としての contraction で代用しています。(Priest 先生も contraction を推論規則として扱っておられます。)
最後に、Stephen Read 先生の、contraction を落とすと直観主義的観点からの背理法が使えなくなるという主張と、それに対する私の疑念をここで簡単に記しておくことに致します。
先生は次のご高著の該当ページで、
- Stephen Read Thinking About Logic: An Introduction to the Philosophy of Logic, Oxford University Press, OPUS Series, 1995, p. 162,
contraction の話を持ち出し、以下のように述べておられます。私訳/試訳も付けます。
[I]f we reject it [i.e., contraction], then whatever rationale we give for its rejection will probably mean rejecting reductio and consequentia mirabilis as well [...]
もしもそれ [すなわちコントラクション] を拒絶すれば、その拒絶にどんな理由を与えるとしても、その結果がおそらく意味することは、背理法の拒絶であり、コンセクエンティア・ミラビリスの拒絶でもあるだろう。
つまり、一言で言えば、contraction の拒絶は背理法の拒絶となる、ということです。
根拠は何でしょうか？ 同じページから引用し、私訳/試訳を付けます。
Now, reductio is closely linked to contraction. Its basic form is that of consequentia mirabilis, 'if A then not-A; so not-A'. 'Not-A' in turn is equivalent to 'if A then absurdity' ('0=1' or some other unacceptable proposition − 'snow is black', perhaps). So consequentia mirabilis expands into, 'If A then if A then 0=1; so if A then 0=1', and that is an instance of contraction. [...]
さて、背理法はコントラクションと密接な関係がある。その基本形はコンセクエンティア・ミラビリスの形式である。つまり、「もし A ならば A でない、ならば A でない」である。次に「A でない」は「もし A ならば不合理である」に相当する ([不合理なものとしては]「0=1」または何か他の受け入れがたい命題、おそらく「雪は黒い」を取ればよい)。そうするとコンセクエンティア・ミラビリスは展開されて、「もし A ならば、もし A ならば 0=1, ならば A ならば 0=1」となり、これはコントラクションの一事例である。[...]
先生はここで背理法として、直観主義でも許されるものをお考えであり、それは次のように式の形式で表されます*6。
(A → (B ∧ ¬B)) → ¬A
矛盾 'B ∧ ¬B' を「人」で表せば、今の式は以下のようになります。
(A → 人) → ¬A
先生によると、この背理法の式は contraction と密接な関係にあるということです。先生による、その理由を記します。
まず、先生は例の背理法の「基本形」が consequentia mirabilis の形をしていると言います。先生が言及されている consequentia mirabilis を式で表せば、次のようになります。
(A → ¬A) → ¬A
さらに、「A でない」という否定の定義は、先生も述べておられるとおり、一般には次のようになります。
¬A =def. A → 人、または A → 0=1, または A → 雪は黒い、など。
そこで、先生がされているように、consequentia mirabilis を否定の定義で「展開」してやれば、不合理なものとして 0=1 を使うと、
(A → (A → 0=1)) → (A → 0=1)
になります。これは確かに contraction を式の形式で表した場合の一事例になっています。
まとめると、背理法の「基本形」は consequentia mirabilis の形式を持っており、consequentia mirabilis を否定の定義によって「展開」してやると contraction の一事例になるので、背理法は contraction と密接な関係にある、ということです。
そして先生によると、先生の文章として最初に上げた引用文に基づくならば、以上により、contraction の拒絶は背理法の拒絶になる、ということです。
こうして、先生によるならば、contraction を落とすと背理法が使えなくなるのです。ただ、私にはよくわからないのですが、背理法の「基本形」が consequentia mirabilis の形式を持っているということがどういうことなのか、はっきりしません。はっきりしないのは、私の脳みそが足りないせいかもしれませんが…。
今問題にしている背理法
(A → 人) → ¬A
と、consequentia mirabilis
(A → ¬A) → ¬A
とが、よく似ているのは私にもわかるのですが、両者の関係が私にははっきりしません。
ところで今の consequentia mirabilis を自然演繹で証明してやると、次のような証明図として書くことができます。
そして、この証明図の一番下の式 (A → ¬A) → ¬A より上の部分だけを取り出して簡略に記せば、以下のようになります。
これを見るとわかるのは、この図では、式 A → ¬A を前提した上で、A を仮定し、矛盾を導くことでその否定 (¬A) を引き出す (直観主義的な) 背理法となっている、ということです。
ここからわかることは次のことです。つまり、A → ¬A を前提した上で、A を仮定して矛盾を引き出し、それにより ¬A を導く背理法を使ったならば、その後で前提の A → ¬A を仮定として落としてやると、それは consequentia mirabilis の証明となる、ということです。
少し一般的に言いますと、(直観主義的な) 背理法では、あることを仮定し、何らかの前提を使って矛盾を引き出せば、その最初の仮定の否定を結論として導いてよいのですが、この際の「何らかの前提」として取られているのが、Read 先生の話においては、A → ¬A であり、これをも仮定として証明の最後に落としてやれば、それは consequentia mirabilis の証明となる、ということです。
よくはわからないのですが、Read 先生が背理法の「基本形」を consequentia mirabilis の形だとするのは、以上のようなことなのではなかろうか、と私は推測しています。
しかし、だとすると、consequentia mirabilis の証明図を見ればわかりますが、その証明図では consequentia mirabilis の証明に (直観主義的な) 背理法を使っています。この背理法の証明に、その「基本形」であるとされる consequentia mirabilis を使うのではなく、まったく逆に、consequentia mirabilis の証明に背理法を使っています。
ということは、背理法の「基本形」が consequentia mirabilis なのではなく、consequentia mirabilis のいわば「基本形」が (直観主義的な) 背理法なのではないでしょうか？
もしもそうであるならば、Read 先生は (直観主義的な) 背理法の「基本形」は consequentia mirabilis だと述べておられますが、それは間違っていることになると思います。その逆が正しいのではないでしょうか？
なお、先生の上記一番目の引用文を再度掲げてみますと、
[I]f we reject it [i.e., contraction], then whatever rationale we give for its rejection will probably mean rejecting reductio and consequentia mirabilis as well [...]
とありますが、ここで先生は contraction の拒絶は、背理法の拒絶を「たぶん(probably)」意味するだろうと言っておられます。この 'probably' という言葉を使っておられることから、先生は contraction の拒絶が背理法の拒絶を本当に意味するのか、おそらく確信がなかったのではないでしょうか？ 確たる証拠を手にしておられなかった可能性があります。Contraction の拒絶は背理法の拒絶だ、とする先生のご意見は、ひょっとすると先生の勇み足だったのかもしれません。
なお、Read 先生に対する私の疑念の、さらに詳細な説明は、本日記、2016年1月2日、項目 ''Is Consequentia Mirabilis a Basic Form of Reductio ad Absurdum?'' にございます。
以上で終わります。精神的にひどく不安定な時期に書かれた文章ですので、誤解や無理解や、激しい勘違いや省察不足が多数散見されるようでしたら誠に申し訳ございません。また Read 先生のお話を私が理解していないようでしたら謝ります。何卒お許しくださいますようお願い申し上げます。
*1:この件に関し、日本語で読める文献としては、例えば次を参照してみてください。照井一成、「素朴集合論とコントラクション」、『科学哲学』、第36巻、第2号、2003年。
*2:ところで、contraction を落とすことは、新たな論理の採用となるのだろうか？ あるいは今ある論理の改訂ということになるのだろうか？ しかしそもそも論理を採用したり改訂したりすることはできるのだろうか？ 論理の採用や改訂ということを整合的に詳しく説明することは可能だろうか？ それは一体何をしていることになるのだろうか？ 大体、論理とは何だろうか？ 論理的真理の集合だろうか？ それとも妥当な推論規則の必要にして十分な集合のことだろうか？ あるいは論理とは妥当な推論を行なう人間の能力のことなのだろうか？ それとも論理とは思考の道具のことなのだろうか？ 私は今までにもしばしば contraction を落とした論理がどうしてこうしてというような話をしてきましたが、いつも心のなかで引っかかっていたのは、以上のような疑問であり、これらの疑問は contraction を落とした論理がどうのこうのというよりも、より基本的で、より重要な問題だろうと思ってきました。しかし、より基本的でより重要な問題というものは、しばしば取り組むのに困難があり、それよりも、より個別的で比較的短い時間と少ない労力で回答可能な問題に取り組んだ方が何かと得策であり、問題がはかどるものですから、ムズカシイ問題は避けてきました。ですが、やはり避け難いものがあります。論理を採用したり改訂したりすることは可能なのかという点に関して、参考になる文献をわずかばかり上げるなら、私が最近読んでいたものに限るとすると、(それはちょっと限定しすぎでしょうけれども) 次の本の該当ページが興味深いです。飯田隆、『規則と意味のパラドックス』、ちくま学芸文庫、筑摩書房、2016年、202-208ページ。ここでは Kripke さんの考えを紹介しながら論理の採用や改訂に人はより慎重になるべきことが論じられています。これを論じる際、飯田先生は次の論文を参考にされています。Alan Berger, ''Kripke on the Incoherency of Adopting a Logic,'' in his ed., Saul Kripke, Cambridge University Press, 2011. この論文は四部構成を取っており、私はそのうち、ひとまず第一部と結論である第四部を読みました。この論文も論理の採用や改訂という試みに懐疑的です(p. 177)。その種の試みを考える上で、本論文もためになりそうです。他方で、新たな論理の採用や論理の改訂を積極的に支持する動きももちろんあります。おそらく最も急進的、根底的、かつ精力的にこの種の動きを見せているのが Graham Priest さんだと思われます。現在、Priest 先生こそが最も積極的に極端と見える alternative な logic の採用を世界のあちこちで宣伝して回っておられると思われます。そこからして、論理の採用や改訂を支持する強力な見解を保持しているのが Priest 先生ではないかと推測されます。先生は多作な方ですから、たぶん色々なところでその見解を開陳しておられるのだと思うのですが、つい最近の論考でその種の話題をまとまった形で展開しておられる論文は、次のものだろうと考えられます。Graham Priest, ''Revising Logic,'' in Penelope Rush ed., The Metaphysics of Logic, Cambridge University Press, 2014. この論文は短いものですから、早速一通り読みましたものの、私個人としては十分説得されたという感じがしませんでした。あるいは私は先生を誤解しているのかもしれませんが。いずれにせよ Priest 先生の見解は、この論文にあるままではなく、先生のその他の論考に見られる見解で補強することにより、その効力を十分発揮することになるだろうと思います。
*3:直観主義的な観点からの背理法とは、ある文 A を仮定し、そこから矛盾が導かれたなら、その文の否定 ¬A を結論してよいとする論法。一方、通常の背理法とは、ある文 A を証明したい場合、その文の否定 ¬A を仮定し、そこから矛盾が導かれたなら、その否定文 ¬A の否定 ¬¬A を結論してよく、さらにここからこの否定文の否定 ¬¬A、すなわち証明したかったその文の肯定 A を結論してよいとする論法です。このように背理法には二種類あることが、次でも簡単に触れられています。岩本敦、「論理と数学における構成主義 ある議論」、飯田隆編、『知の教科書 論理の哲学』、講談社選書メチエ 341, 講談社、2005年、124ページ。
*4:以上の、contraction を落とすと直観主義的観点からの背理法が使えなくなるというRead 先生の主張と、私によるその主張への疑念については、最後に少し説明したいと思います。
*5:以上、Modus Ponens Axiom と Curry's Paradox については、次の古典的な論文を参照ください。Robert K. Meyer, Richard Routley, J. Michael Dunn, ''Curry's Paradox,'' in: Analysis, vol. 39, no. 3, 1979. 特にその pp. 127-128. また、Modus Ponens Axiom を Assertion と呼んでいるのは Graham Priest 先生です。See his In Contradiction, Second Edition, Oxford University Press, 2006, pp. 83-84. さらに Priest 先生は、Modus Ponens Axiom/Assertion を推論の形式に直したものに対し、しばしば Absorption と呼んでおられます。Ibid., p. 83.
*6:Read, p. 251.
