Skinerrian's blog

論理学・哲学・科学史・社会学などに興味があるので、その方面のことを書きます。更新は不定期。

カリーのパラドクス

数理論理学をかじったことのある人は、自己言及がパラドクスを引き起こす可能性をもつことを知っている。例えば、ラッセルのパラドクスは、自分自身を含まない集合 {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」はカリーのパラドクスの真理述語バージョンといえる。真理述語に関しては「Pが真であるのは、Pときそのときに限る」という基本的な原理がある。この原理を否定するのは厳しいので、一般的には、自己言及そのものを文法違反として退ける。

カリーのパラドクスは、ラッセルのパラドクスや嘘つきパラドクスと比べるとそれほど有名でないが、知っておく価値はある。数理論理学を勉強していると、このパラドクスは思わぬところで出没する。最近聞いた話だが、レープの定理の標準的な証明はカリーのパラドクスと似ている。レープの定理とは、PAのような算術理論で可証性述語Provを定義するとき、任意のφについて、Prov(φ) → φ がPAで証明できたとすると、PAでφも証明できるという定理。いったいどの辺でカリーのパラドクスがでてくるのか。私が理解した限りでは以下のような感じだと思われる。

レープの定理の標準的な証明は、Prov(x) → φという一項述語を作って、不動点定理により、ψ ≡ Prov(ψ) → φ という双条件が成り立つということから出発する。このψは「この文が証明できるならφ」と言っているように読めるので、カリーのパラドクスとよく似ている。もっとも、ここからφを証明するまでの手順はずっと複雑だけれども*3

関連記事

*1:カリーのパラドックス - Wikipedia

*2:厳密にいえば、X∈Xを二回仮定しているので、このように結論するには縮約規則(contraction)を使う必要がある。

*3:これとは別の証明法は、ゲーデルの第二不完全性定理から出発する(cf. フランセーン『ゲーデルの定理』p.140)。レープの定理と第二不完全性定理は同値といってよく、実際、標準的な証明でも可証性述語に関するヒルベルトとベルナイスの可導性条件を利用することになる。