自分自身を含まない集合 {x | ￢x∈x} などという集合の存在を認めてしまうと矛盾が生じる。カリーのパラドクスは、このラッセルのパラドクスとよく似ている*1。論理学では、否定命題￢Pを「P→⊥」という形で定義することがある。この定義を用いると、ラッセルのパラドクスは {x | x∈x → ⊥} という集合にまつわるパラドクスといえる。これに対し、カリーのパラドクスは {x | x∈x → A} という集合にまつわるパラドクスである。ここで、Aは任意の命題が入る。⊥も入りうるので、その場合にはラッセル集合である。この集合がパラドクスを引き起こすのは、{x | x∈x → A} という集合の存在を認めると、Aが証明されるからである。Aは任意の命題なので、任意の命題が同じ論法で証明できてしまうので、実質的には矛盾である。
実際に、Aを証明してみよう。問題の集合をXと名付け、X∈Xと仮定することからはじめてみる。X∈Xなので、Xの定義から、X∈X → Aである。X∈X → AとX∈Xから、modus ponensによりAである。X∈Xの仮定からAが導かれたので、X∈X→Aである*2。これで仮定が落ちた。さて、Xの定義とX∈X→Aから、X∈Xである。よって、modus ponensによりAである。
自己言及がこうしたパラドクスの元凶だとみなすならば、自己言及を何らかの仕方で禁じねばならない。一つのやり方（タイプ理論）は「x∈x」のような表現を文法違反だと主張すること。別のやり方（公理的集合論）は、{x | ￢x∈x} のような集合を作らせないため、包括原理などの集合に関する原理を捨てる（制限する）ことである。
自己言及は集合に関してのみ生じるわけではない。嘘つき文「この文は真でない」はラッセルのパラドクスの真理述語バージョン、「この文が真ならば、A」はカリーのパラドクスの真理述語バージョンといえる*3。真理述語に関しては「Pが真であるのは、Pときそのときに限る」という基本的な原理がある。この原理を否定するのは厳しいので、一般的には、自己言及そのものを文法違反として退ける。
カリーのパラドクスは1940年頃に発見された。カリーのパラドクスは、ラッセルのパラドクスや嘘つきパラドクスほど有名でないが、知っておく価値はある。数理論理学を勉強していると、このパラドクスは思わぬところで出没する。
例えば、レープの定理の標準的な証明はカリーのパラドクスと似ている。レープの定理とは、PAのような算術理論で可証性述語Provを定義するとき、任意のφについて、Prov(φ) → φ がPAで証明できたとすると、PAでφも証明できるという定理。いったいどの辺でカリーのパラドクスがでてくるのか。私の理解する限りでは、だいたい以下のような感じだ。
レープの定理の標準的な証明は、Prov(x) → φという一項述語を作って、不動点定理により、ψ ≡ Prov(ψ) → φ という双条件が成り立つということから出発する。ψは「この文が証明できるならφ」と言っているように読めるので、カリーのパラドクスとよく似ている。もっとも、ここからφを証明するまでの手順はずっと複雑だけれども*4。
関連記事
*2:厳密にいえば、X∈Xを二回仮定しているので、このように結論するには縮約規則（contraction）を使う必要がある。
*3:このバージョンは「ギーチのパラドクス」と呼ばれることもある（三浦『論理パラドクス：論証力を磨く99問』文庫版pp.66-68）。これは、Geach, "On insolubilia" 1954に由来。
*4:これとは別の証明法は、ゲーデルの第二不完全性定理から出発する（cf. フランセーン『ゲーデルの定理』p.140）。レープの定理と第二不完全性定理は同値といってよく、実際、標準的な証明でも可証性述語に関するヒルベルトとベルナイスの可導性条件を利用することになる。
