カリーのパラドックス

カリーのパラドックスとは、任意の主張F が、それ自身について「もしCならばF 」と述べている文Cの存在のみから証明されるというパラドックスである。このパラドックスは、一見無害な論理的演繹規則をいくつか必要とするだけである。Fは任意であるため、これらの規則を持つ論理であれば、あらゆることを証明できる。このパラドックスは、自然言語や、集合論、ラムダ計算、組合せ論理などの様々な論理で表現できる。

このパラドックスは、 1942年にこのパラドックスについて論文を書いた論理学者ハスケル・カリーにちなんで名付けられました。 ^{[ 1 ]}また、レーブの定理との関係から、マルティン・ヒューゴ・レーブにちなんでレーブのパラドックスとも呼ばれています。 ^[²^]

自然言語で

「 AならばB 」という形式の主張は条件文と呼ばれます。カリーのパラドックスでは、以下の例に示すように、特定の種類の自己言及的な条件文が用いられます。

この文が真実であれば、ドイツは中国と国境を接していることになります。

ドイツは中国と国境を接していませんが、例文は確かに自然言語文であるため、その文の真偽を分析することができます。この分析からパラドックスが導き出されます。分析は2つのステップで構成されます。まず、一般的な自然言語証明手法を用いて、例文が真であることを証明します（以下のステップ1～4）。次に、例文の真偽を用いて、ドイツが中国と国境を接していることを証明します（ステップ5～6）。

この文は「この文が真であれば、ドイツは中国と国境を接している」と書かれています。 [正式な証明と互換性のあるステップ番号を取得するために定義を繰り返します]
もしその文が真ならば、それは真である。 [明白、すなわちトートロジー]
この文が真であれば、ドイツは中国と国境を接している。 [「真である」を文の定義に置き換えてください]
この文が真実であれば、ドイツは中国と国境を接している。 [契約の繰り返し条件]
しかし、4. は文中に書かれているとおりなので、確かに真実です。
この文は[5.により]真であり、[4.により]真である。もし真ならば、ドイツは中国と国境を接している。したがって、ドイツは中国と国境を接している。 [法則]

ドイツは中国と国境を接していないため、証明手順の1つに誤りがあったことが示唆されます。「ドイツは中国と国境を接している」という主張は、他のいかなる主張に置き換えても証明可能です。したがって、すべての文は証明可能であるように見えます。この証明は広く受け入れられている演繹法のみを用いており、これらの方法はどれも誤りではないように見えるため、この状況は逆説的です。^{[ 3 ]}

非公式な証明

条件文（「 AならばB 」という形式の文）を証明するための標準的な方法は「条件付き証明」と呼ばれます。この方法では、「 AならばB 」を証明するために、まずAを仮定し、次にその仮定のもとでBが真であることを示します。

上記の2つの手順で説明したカリーのパラドックスを生成するには、この方法を「この文が真であれば、ドイツは中国と国境を接している」という文に適用します。ここで、 A（「この文は真である」）は文全体を指し、B（「ドイツは中国と国境を接している」）は文全体を指します。したがって、A を仮定することは、「もしAならば、B」を仮定することと同じです。したがって、 Aを仮定することで、 Aと「もしAならば、B 」の両方を仮定したことになります。したがって、Bは前件法（ modus ponens）により真であり、通常の方法、つまり仮説を仮定して結論を導くことで、「もしこの文が真であれば、『ドイツは中国と国境を接している』は真である」ということを証明したことになります。

さて、「この文が真ならば、『ドイツは中国と国境を接している』は真である」という主張が証明できたので、再び法則を適用することができます。なぜなら、「この文は真である」という主張が正しいことが分かっているからです。このようにして、ドイツは中国と国境を接していると推論できます。

形式論理学では

文論理

前のセクションの例では、形式化されていない自然言語推論が使用されました。カリーのパラドックスは、形式論理のいくつかの変種にも見られます。この文脈では、形式文 ( X → Y ) があり、X自体が ( X → Y )と等しいと仮定すると、形式証明によってY を証明できることを示しています。このような形式証明の一例を以下に示します。このセクションで使用されている論理記法の説明については、論理記号一覧を参照してください。

X := ( X → Y )
仮定、出発点は「この文が真ならば、Y」と同等である。
X → X
同一性の法則
X → ( X → Y )
2の右辺を代入する。XはX → Yと1を足したものと等しいからである。
X → Y
3から短縮形
X
4を1で置き換える
はい
5と4からmodus ponensにより

パースの法則を用いた別の証明もあります。X = X → Yならば、 ( X → Y ) → Xとなります。これにパースの法則 (( X → Y ) → X ) → Xとモーダスポネンスを合わせると、 Xが成立し、続いてY が成立することが示されます（上記の証明と同様）。

上記の導出は、Yが形式体系において証明不可能な命題である場合、その体系において、Xが含意 ( X → Y )と等価となる命題Xは存在しないことを示しています。言い換えれば、前の証明のステップ1は失敗しています。対照的に、前のセクションでは、自然言語（非形式化言語）においては、あらゆる自然言語命題Yに対して、自然言語における( Z → Y )と等価となる自然言語命題Zが存在することを示しています。つまり、Zは「この文が真ならばY」です。

素朴集合論

たとえ基礎となる数学的論理が自己言及的な文を一切許容しないとしても、ある種の素朴集合論は依然としてカリーのパラドックスの影響を受けやすい。無制限の理解を許容する集合論においては、集合を調べることで任意の論理命題Yを証明できる。すると、という命題がと同値であることが容易に示される。このことから、上記の証明と同様に、が推論される。（「」は「この文」を表す。） $X\ {\stackrel {\mathrm {def} }{=}}\ \left\{x\mid (x\in x)\to Y\right\}.$ $X\in X$ $(X\in X)\to Y$ $Y$ $X\in X$

したがって、整合集合論においては、偽のYに対しては集合は存在しない。これはラッセルのパラドックスの変種と見ることができるが、同一ではない。集合論に関するいくつかの提案は、内包規則を制限するのではなく、論理規則を制限することで、それ自体の要素ではないすべての集合の集合の矛盾性を許容することで、ラッセルのパラドックスに対処しようと試みてきた。上記のような証明の存在は、そのような作業がそれほど単純ではないことを示している。なぜなら、上記の証明で用いられた演繹規則の少なくとも1つは省略または制限する必要があるからである。 $\left\{x\mid (x\in x)\to Y\right\}$

制限された最小論理によるラムダ計算

カリーのパラドックスは、含意命題計算によって強化された型なしラムダ計算で表現できる。ラムダ計算の構文上の制約に対処するため、2つのパラメータを取る含意関数をで表すものとする。つまり、ラムダ項は通常の挿入記法と同等となる。 $m$ $((mA)B)$ $A\to B$

任意の式は、ラムダ関数とを定義することで証明できる。ここではカリーの不動点コンビネータを表す。そしてとの定義により、上記の文論理の証明は計算においても同様に証明できる。^[⁴^]^[⁵^] $Z$ $N:=\lambda p.((mp)Z)$ $X:=({\textsf {Y}}N)$ ${\textsf {Y}}$ $X=(NX)=((mX)Z)$ ${\textsf {Y}}$ $N$

${\begin{array}{cll}\vdash &((mX)X)&{\mbox{ 最小論理公理 }}A\to A\\\vdash &((mX)((mX)Z))&{\mbox{ }}X=((mX)Z) であるため\\\vdash &((mX)Z)&{\mbox{ 最小論理の定理 }}(A\to (A\to B))\vdash (A\to B){\mbox{ により }}\\\vdash &X&{\mbox{ }}X=((mX)Z)\\\vdash &Z&{\mbox{ 次式により }}A,(A\to B)\vdash B{\mbox{ }}X{\mbox{ と }}((mX)Z) から }}\\\end{array}}$

単純型ラムダ計算では、固定小数点コンビネータは型付けできないため、許可されません。

組み合わせ論理

カリーのパラドックスは、ラムダ計算と同等の表現力を持つ組み合わせ論理でも表現できます。任意のラムダ式は組み合わせ論理に翻訳できるため、カリーのパラドックスの実装をラムダ計算に翻訳するだけで十分です。

上記の用語は組み合わせ論理ではと翻訳され、したがって^[⁶^] $X$ $(r\ r)$ $r={\textsf {S}}\ ({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))\ ({\textsf {K}}Z);$ $(r\ r)=((m(rr))\ Z).$

議論

カリーのパラドックスは、基本的な論理演算をサポートし、かつ自己再帰関数を式として構築できる言語であれば、どのような言語でも定式化できます。このパラドックスの構築を支える2つのメカニズムは、自己参照（文中から「この文」を参照する機能）と素朴集合論における無制限の理解です。自然言語は、他の多くの言語と同様に、ほぼ常にこのパラドックスの構築に使用できる多くの機能を備えています。通常、言語にメタプログラミング機能を追加することで、必要な機能が追加されます。数理論理学では、一般的に自身の文への明示的な参照は認められませんが、ゲーデルの不完全性定理の核心は、異なる形式の自己参照を追加できるという点にあります（ゲーデル数を参照）。

証明の構築に用いられる規則は、条件付き証明における仮定規則、縮約規則、そして可能性規則である。これらは、一階述語論理など、ほとんどの一般的な論理体系に含まれます。

いくつかの形式論理への帰結

1930年代には、カリーのパラドックスと、それに関連してカリーのパラドックスが発展したクリーネ・ロッサーのパラドックス^{[ 7 ]}^{[ 1 ]}が、自己再帰的な表現を許す様々な形式論理体系が矛盾していることを示す上で大きな役割を果たした。

無制限内包の公理は現代の集合論ではサポートされておらず、したがってカリーのパラドックスは回避されます。

参照

参考文献

^ ^a ^bカリー、ハスケル・B. (1942年9月). 「ある形式論理の矛盾」.記号論理学ジャーナル. 7 (3): 115– 117. doi : 10.2307/2269292 . JSTOR 2269292. S2CID 121991184 .
^バーワイズ、ジョン、エチェメンディ、ジョン(1987). 『嘘つき：真実と循環性に関する試論』ニューヨーク：オックスフォード大学出版局. p. 23. ISBN 0195059441. 2013年1月24日閲覧。
^スタンフォード哲学百科事典にも同様の例が説明されている。シャピロ、ライオネル、ビール、Jc (2018)「カリーのパラドックス」を参照。ザルタ、エドワード・N. (編)スタンフォード哲学百科事典。ISSN 1095-5054。OCLC 429049174。
^ここでの命名は文論理の証明に従っていますが、Curry の固定小数点コンビネータとの混同を避けるために、 「 Y 」ではなく「 Z」が使用されています。 ${\textsf {Y}}$
^ Gérard Huet (1986年5月).計算と演繹のための形式構造. プログラミング論理と離散設計計算に関する国際サマースクール. マルクトバードルフ. 2014年7月14日時点のオリジナルよりアーカイブ。{{cite book}}: CS1 メンテナンス: 場所の発行元が見つかりません (リンク)こちら：p.125
^ $(rr)$ $=$ $({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))$ $\to$ $({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}})({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {K}}Z({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))$ $\to$ $({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}})({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))Z)$ $\to$ $({\textsf {K}}m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {S}}{\textsf {I}}{\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))Z)$ $\to$ $(m({\textsf {S}}{\textsf {I}}{\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)$ $\to$ $(m({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))Z)$ $\to$ $(m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {I}}({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z))))Z)$ $\to$ $(m({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)({\textsf {S}}({\textsf {S}}({\textsf {K}}m)({\textsf {S}}{\textsf {I}}{\textsf {I}}))({\textsf {K}}Z)))Z)$ $=$ $((m(rr))\ Z)$
^カリー、ハスケル B. (1942年6月). 「数理論理学の組合せ的基礎」.記号論理ジャーナル. 7 (2): 49– 64. doi : 10.2307/2266302 . JSTOR 2266302. S2CID 36344702 .