"The strength of extensionality I ― weak weak set theories with infinity" （佐藤憲太郎）
Annals of Pure and Applied Logicのオンライン出版*1、こちらから入手可能。
この論文は、集合論 ZF に関する証明論的分析として、非常に重要なものであると考えます。ZFの上で数学を展開することにではなく、ZFがベースとする集合概念（およびZFと言う体系そのものの証明論的性質）について興味を持たれる方全てに一読をお勧めします（特に数学の哲学に興味を持たれる方は必読ではないでしょうか）。
注意：
本エントリーは、佐藤氏の論文の解説ではなく、私が佐藤氏の結果を評価する理由の解説となっております。
この点、ご注意のほどを。
まず、ZFがベースとする集合概念についておさらいをしましょう。おおざっぱな話をすると、ZFの公理は以下の二つのグループに分けることが出来ると思います。
- 集合の存在保証原理： 包括的な集合の存在保証公理であった包括原理（the comprehension principle）が矛盾を導くため、包括原理を弱め、集合を帰納的に定義していく。
- 外延性公理。上のやり方で構成された集合について、集合の間の同一性関係を定義する。
以上のように、外延性公理は、集合の存在を保証するわけではないという点で、他の公理と異なる性格を持っています。
外延性公理は、「集合はそのメンバーのみによって構成される」という至極もっともなことを主張しています。そのため、ブーロス*2は、外延性公理は「ZFの他の公理にはない、特殊な認識論的身分を有している」とか、外延性公理が成立しないような理論は集合論とは言えない（もしくは「そう呼べるとしてもお情けで呼んでもらっているようなものだ」）とか、「集合という概念…が外延性公理に従うのは、それらの概念を用いるということの中心的な特性なのだ」と言いました。でも、ここで疑問なのですが、外延性公理ってそんなに自明な公理なのでしょうか。
さて、公理が自明であるかどうかのバロメーターの一つが、その公理を加えることで理論がどれくらい強くなるのかでしょう（自明であれば、公理を加えても理論は強くはならないはずです）。外延性公理の場合、外延性公理を仮定しない理論 T に比べて、Tに外延性公理を加えた理論はどれくらい強くなっているのでしょうか。
この問題に関して、フリードマンの結果により、直観主義論理上で、ZFから外延性公理を除去した体系の任意のモデルでは、そのモデル上のメンバーシップ関係
から新しいメンバーシップ関係
を定義することができ、なんと
は外延性公理のモデルになることが知られています。この結果は、外延性公理は（それ自身として新しい結果を付け加えることがない）自明な公理であることを示している、ように思われました。
でも、それはZFの他の公理が、外延性公理を分析する枠組みとしては強力すぎるからではないのか。というわけで、この論文では、集合論の非常に弱い体系 Basic *3を導入し、外延性公理*4の証明論的強さはどのくらいかを、証明論的順序数を使用して検討しています。
結果は驚くべきものでした。まず、証明論的順序数に関し、理論 T の証明論的順序数を で表現することにします。このとき
と、外延性公理を加えることで、体系の証明論的順序数が跳ね上がることを佐藤氏は示しました。同時に、分出公理の弱いバージョンである -SEP （
論理式にのみ分出公理の適用を認める公理） を考えると、
と、その証明論的順序数は外延性公理と同等になります。すなわち、これは上記の公理の分類（集合の存在保証原理 vs 外延性公理）の構図を破り、外延性公理は、弱い集合論上では、ある種の集合の存在保証原理と（証明論的順序数の意味において）同じくらいの強い仮定であることを意味します。
最後に個人的感想を。佐藤氏からこの結果を聞いたとき、最初に思ったことは「その発想はなかったわ」*5というものでした。
外延性公理の自明性に関しては、私自身も関心を持っていました。しかし、哲学者の曖昧性の定義という、集合論の外部からの興味だったため、佐藤氏の純粋に集合論の枠内で証明論的手法で外延性公理の論理的強さを考えるという姿勢そのものに強い感銘を受けました。
