ラッセルのパラドックス：傾向と対策 (3.1.7) : 証明論的アプローチへの補足；Fitchの "demonstrably consistent" な set theory F
以前、ラッセル・パラドックスへの証明論的アプローチ（グリシン論理など）を取り扱った際に忘れていた話を紹介いたします。もう一つ、古典論理を認めるものの、ある特別な種類の証明図（正規化できない証明）を証明として認めないことにより、ラッセル・パラドックスが矛盾を導かないような体系が作れるのです。
この話題を扱うときの問題は、普通この話をするときは自然演繹(Natural Deduction)で行うのですが、hatenaでは自然演繹の証明図がかけないことです。なんとか努力しますが、分かりにくい話となってしまいました。ご了承ください。
証明の正規化とは
定理を証明する際、普通は最も効率よく証明することを目指します。しかし、遠回りして証明してしまうこともよくあります。それに、わざと回りくどい証明をすることだってできます。
例：論理式Aを証明する際
- まず A を証明する
- 次に別の論理式 B を証明する
- 上の1,2から A&B を証明する
- 上の3よりA&B が証明されたので、それから Aを証明する
すでに1の段階で式 A を証明しているのに、わざわざ論理記号 & を導入し(3)、そして除去しています(4)。アホらしい。
という訳で、こういう面倒な証明図を書き換え、2-4のプロセスを省いて1のみの証明図にすることで、論理式 A の証明図を簡単にすることができます。こういう作業のことを「簡約」といいます（この場合は & を除去するので「& に関する簡約」と言います）。
そして無駄のない、これ以上簡約をすることができない証明を「正規な証明図」と呼びます。
ラッセル・パラドックスの導出と簡約
さて、古典論理に抽象化ルール、つまり P(t) implies t∈{x:Px} と、その除去ルールを足した論理体系を考えましょう。当然、ラッセル・パラドックスにより矛盾が導かれます。問題は、その証明図を簡約することができるかどうか、です。
実は、簡約が不可能で、簡約を続けると有限回のループで元の証明図に戻ってしまうことが知られています。・・・で、これをどうhatenaで説明したものか悩んでいたのですが、ネット上で照井一成氏が授業の資料としてアップしたらしい pdf ファイルを見つけましたので、勝手にリンクをさせていただきます（問題があれば削除しますので、ご一報ください）。p.3-4にかけて証明図があります。
Fitchの "A demonstrably consistent set theory" F
さて、証明図の形に注目して、包括原理をもつ無矛盾な集合論を作ろうとしたのは、Fitch (1952) が初めてのようです。Fitchの体系をプラヴィッツが再定式化した体系 F は、抽象化ルールとその除去ルールを持つ体系で、その体系は二種類のdeductionを持ちます。
その場合、ラッセル・パラドックスなどの集合論的パラドックスは皆、正規化できないため、擬-演繹ではあっても演繹にはならず、したがってこの体系では演繹によって矛盾を証明できません（その意味で「無矛盾」です）。
Fitchの体系は、これとは似ていますが、擬ー演繹に矛盾をさけるためにいくつかad hocな制限を加えたものになっています。Fithchはまた、その体系で古典数学のそれなりの部分が展開可能であることを示しています。
問題点
この体系の問題点は、プラヴィッツの指摘*1によれば「Aと A→B が（正規証明によって）証明可能であっても、Bが証明可能とは限らない（Bは擬-証明しか持たないかもしれない）」ということです。論理体系としては、結構致命的な欠陥のようにも思えます。
今後の予告
一見、話はここで終わったようですが、実は集合とその項の正規化の話は、型理論の中に集合論を翻訳して埋め込むという研究の中で大きな役割を果たします。このような研究のモチベーションは型理論の中でどれだけ数学を展開できるかということの探求ですが、結果的には、Miquel, Werner, Coquandらが示したように、計算機上の定理証明支援系 Coq にZFC を埋め込んだりとか、ZFCに関してカット除去を行ったりとか、不思議なことができるようになります。そのうち紹介したいと思いますので、期待しないでお待ちください。
（12月21日補足）
プラヴィッツの体系 F と、Fitchのオリジナルな体系との関係について、いくつか事実誤認がありました。お詫びとともに訂正させていただきます。
*1: Dag Prawitz. Natural Deduction. p.95
