Skinerrian's blog

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

チャーチのラムダ計算

wikipediaの「ラムダ計算」によると

元々チャーチは、数学の基礎となり得るような完全な形式体系を構築しようとしていた。彼の体系がラッセルのパラドックスの類型に影響を受けやすい(例えば論理記号として含意 → を含むなら、λx.(x→α) にYコンビネータを適用してカリーのパラドックスを再現できる)ということが判明した際に、彼はそこからラムダ計算を分離し、計算可能性理論の研究のために用い始めた。

チャーチの元の体系は論理結合子を含んでいて、それゆえ矛盾した、というこの話はよく聞くが、今までまともに考えたことはなかった。おおよそ次のような具合だろうか。二つのステップに分けて述べる。 

1. 任意のラムダ項αについて、X = X→αとなるようなラムダ項Xが存在することを示す。

  • 任意のαについて、x→α、λx.(x→α)もラムダ項
  • 不動点定理によれば、任意のラムダ項Fについて、X = FX となるようなラムダ項Xが存在する*1。Fにλx.(x→α)を代入すると、X = FX =  λx.(x→α)X = X→α

2. 含意(ならば)の論理法則を用いて、X = X→αからαを導く。

  • 公理系λαに、ならばの導入則と除去則を付け加える。
  • Xを仮定。
  • Xを同値であるX→αと置き換える。
  • X→αとXからαを導く(ならばの除去則)
  • 仮定Xからαが導かれたので、X→α(ならばの導入則)
  • X→αを同値のXと置き換える。
  • X→αとXからαを導く(ならばの除去則)。すでに仮定はすべて落ちているので、αが証明できた。

歴史的な背景も含めた詳しい説明が以下にありそう(まだ読んでない)。

Paradoxes and Contemporary Logic (Stanford Encyclopedia of Philosophy)

関連記事

*1:Yコンビネータを使って、X = YFと表現される。