カリーのパラドックス

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

カリーのパラドックスを、上記の2つのステップで説明したように、この方法を「この文が真ならば、ドイツは中国と国境を接している」という文に適用します。ここで、 A「この文は真である」は文全体を指し、Bは「ドイツは中国と国境を接している」です。したがって、Aを仮定することは、「 Aならば、B 」を仮定することと同じです。つまり、Aを仮定することで、Aと「Aならば、B」の両方を仮定したことになります。したがって、モーダス・ポネンスによりBは真であり、仮説を仮定して結論を​​導き出すという通常の方法で、「この文が真ならば、『ドイツは中国と国境を接している』は真である」が証明されました。

さて、「この文が真ならば、『ドイツは中国と国境を接している』は真である」という命題を証明したので、再びモーダス・ポネンスを適用できます。なぜなら、「この文は真である」という主張が正しいことがわかっているからです。このようにして、ドイツは中国と国境を接していると推論できます。

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

1. X  := ( X → Y )
   仮定、出発点、「この文が真であれば、Y」に相当する。
2. X → X
   同一性の法則
3. X → ( X → Y )
   式2の右辺を代入する。なぜなら、XはX → Yに1を加えたものと等しいからである。
4. X → Y
   3から縮約によって
5. X
   4を1に置き換える
6. Y
   モーダス・ポネンスによる5と4から

別の証明方法として、パースの法則を用いる方法がある。X = X → Yならば、( X → Y ) → Xとなる。これとパースの法則 (( X → Y ) → X ) → Xおよびモーダス・ポネンスを組み合わせると、 Xが導かれ、続いてY が導かれる(上記の証明と同様)。

上記の導出は、形式体系においてY が証明不可能な命題である場合、その体系において、 ( X → Y )と同値となる命題X は存在しないことを示している。言い換えれば、前の証明のステップ 1 は失敗する。これに対し、前の節では、自然言語 (非形式化) においては、すべての自然言語命題Yに対して、自然言語において( Z → Y ) と同値となる自然言語命題Zが存在することを示している。すなわち、Zは「この文が真ならばY」である。

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

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

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

任意の式${\displaystyle Z}$ラムダ関数を定義することで証明できる${\displaystyle N:=\lambda p.((mp)Z)}$、 そして${\displaystyle X:=({\textsf {Y}}N)}$、 どこ${\displaystyle {\textsf {Y}}}$はカリーの不動点コンビネータを表す。すると${\displaystyle X=(NX)=((mX)Z)}$定義により${\displaystyle {\textsf {Y}}}$そして${\displaystyle N}$したがって、上記の命題論理の証明は、計算体系で複製することができます。^{[ 4 ] [ 5 ]}

$${\displaystyle {\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)から}}}$$

単純型ラムダ計算では、不動点コンビネータは型付けできないため、認められません。

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

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

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

無制限理解の公理は現代の集合論では支持されておらず、したがってカリーのパラドックスは回避される。