"Curry's Revenge: the costs of non-classical solutions to the paradoxes of self-reference" (Greg Restall)

"The Revenge of the Liar" (ed. JC Beall, Oxford University Press)に掲載予定。論文ファイルはこちらから入手可能。
上の記事でも取り上げましたが、カリーのパラドックスにより、古典論理上では、算術上で全域的な真理述語を仮定するか、もしくは包括原理を仮定すれば矛盾が導出されます。で、上に上げたような解決策がある訳なんですが、さて、それらの「解決策」のコストはどれぐらいなのでしょうか。Restallは、非古典論理を採用し包括原理を救おうというプログラムの代償は、あまりに大きいと論じています。
そして、その論法ですが、「非古典論理を採用すると、こんなに自然な論理操作ができなくなってしまう」ということを示します。

Revenge Problem

さて、上で「カリーのパラドックスは『ならば』（→）についてである」と書きました。しかし、→を別の論理結合子で表現する方法も、いくつか知られています。

古典論理での方法： A→B を、¬A∨Bと同一視する立場。これはパラドックスの原因であり、古典論理を捨てる際に同時に捨てられます。
直観主義での方法：A→B を、 Aの証明をBの証明に変形する関数と考える。といっても、直観主義論理ではカリーのパラドックスはやはり矛盾が起こるので、 "explicitに" このやり方を採用することはできない*1。
Infinitary disjunction による方法：実はもう一種類、他の結合子を使って→を表現する方法があります。それは B→C を ∨{A : A&B \vdash C} （ただし \vdashは論理的導出関係）と、無限個の論理式のdisjunctionとして表現する、というやり方です（論理的導出関係を定義の中で使っているのは、演繹定理の先取りでずるい気もしますが）。実はこの定義も、→の満たすべき性質を満たすことが知られています。

さて、最後のやり方で→を無限disjunctionに還元した場合、

包括原理、もしくは全域的真理述語と算術を持つ体系で、
無限個の文のdisjunctionを取ることを許し、
その無限disjunctionと&が分配則を満たす(distributiveである、つまり A&(∨{Bi : i∈I}) \vdash ∨{A&Bi : i∈I} ）場合、

カリーのパラドックスが導出されてしまいます。
従って、矛盾を避けるためには、上の三つのうちどれかを否定しなければならない。これが「カリーの逆襲問題」です。

無限disjunctionって・・・

まず、無限個のdisjunctionなんか認めなければよい、という考えもあるかもしれません。ですがこの操作は、我々の論理学の研究の中で欠かせない操作と結びついています。論理に代数的意味論を与える場合、欠かせないのが代数内でイデアルをとることですが、このイデアルの意味は、まさしく無限disjunctionです。例えば、命題 A,B,C （面倒なのでその代数的値も同じ記号で書きます）に関して、{A,B,C}を含む最小のイデアルは、文 A∨B∨C を導出するような前提全体の集合となります。従って、イデアルの要素の命題が全て真であれば、従って A∨B∨C も真だということになり、この意味でイデアルはdisjunctionに対応します。
さらに、代数的意味論においては、イデアル自体が命題であるかのように振る舞います。そしてこのイデアルIを、Iを構成する命題の無限disjunctionと見なすことができます。もし無限disjunctionを排除するなら、この代数的意味論における「自然な」類推のどこに問題があるのかはっきりと言う必要が出てきます。

選択

というわけで、選択は限られています。

無限disjunctionをあきらめる：実は、未だにこの方向でのちゃんとした研究はないそうです。ついでに、そういう解決がどんなものになるのか、ちょっと想像できないでしょう。
分配則をあきらめる：縮約規則を持たない部分構造論理や量子論理の解決法がこれです。が、問題は、だれもそういう論理でどうして分配則をあきらめる必要があるのか、ちゃんと説明していないことです。
→の推移性をあきらめる：原理的には可能ですけど、ちょっとやり過ぎのような気が・・・。
包括原理をあきらめる：結局それかい。

という訳で、結論は、

Each approach has its cost. None are straightfoward. There is much work left to do, if we wish to give any account of the paradoxes, including those which involve revising logical theory.

だそうです。そりゃそうだ。

どうでもいい感想

哲学的論理学で論理法則の正当化をするときに、その法則（無限disjunction）には代数的意味論で重要なイデアルが対応するので、その論理法則も、却下するなら説明が必要だ、という論の進め方には感銘を受けました。

*1:素人考えですが、BCKを採用したらどうだろうとか思うのですが。