ＺＦＣの圏論での「代替」には意味があるのか？

たまには、数学の「歴史」の話をしようかと思う。
ご存知のように、数学の「基礎」はカントールによって危機に陥れられた。つまり、（素朴）集合論によって。あらゆる集合を含む集合は、自分自身を含むだろうか？　この答えは含むと言っても矛盾だし、含まないと言っても矛盾。正解は「それ」は「集合ではない」というものであった。では、なにが集合なのだろう？　そこから、公理的集合論は始まる。
バートランドラッセルが提案した「プリンキピア・マセマティカ」は、上記のパラドックスに「直接」、パッチを当てる、という意味では、素直な発想だったと言えるであろう。コンピュータの世界では今では一般的になった「型」という考えを使ってこの問題にアプローチする方法であったわけだが、興味深いのは、この頃の「哲学者」はまだ、真面目に「数学」をやっていた、ということであろう。
しかし、この問題はそれ以降はより、エレガントに議論されるようになる。つまり、数学基礎論（＝論理学）と、公理的集合論として。しかし、そこで問題となったのは「後者」であった。なぜ、公理的集合論が問題なのか？　それは、一言で言えば、この「公理系」が「直感的」ではないことなのだ。
公理的集合論についての、一般的な通俗本としては、

新装版 集合とはなにか―はじめて学ぶ人のために (ブルーバックス)

があり、公理的集合論の詳しい入門書としては、日本語では次が優れている。

現代集合論入門 (日評数学選書)

この本がいいところは、なぜ公理的集合論が「変」なのか。というか、どうしてこんなことになっているのかを、かなり細かく（つまり、啓蒙的に）書いてくれていることで、細かい証明を辿っていけば、「なるほど、こんなことになっているんだな」というのを理解してくれると思う。
（ちなみに、ここで採用されているのがＺＦＣと呼ばれるもので、ツェルメロ・フレンケルの公理系と選択公理を合わせたものであるが、この本を読めば分かるように、この公理系の「外」に、慣用的な表現として「クラス」を導入することで、順序数などを説明することになる。じゃあ、最初からこの「クラス」を公理系の中に入れるとするとどうなるか、といった公理系として、ゲーデル・ベルナイスの公理系というものがあるが、これについては

ゲーデルと20世紀の論理学 4 集合論とプラトニズム

に詳しい説明が載っている。）
ここで大事なポイントは、「これ」が「数学の基礎」として提示されているところにある。ようするに、あまりに「人工的」な印象を受けるわけである。もっと言えば、この公理は

• 強すぎる

のではないのか、という疑いが強いわけである。なぜ、こんな公理が用意されたのか？　それは、上記の「矛盾」を回避するためであった。つまり、いろいろと分かっている「矛盾」を回避しながら、かつ、

• 今ある「全て」の数学を成立させる

ための「基礎」となる公理はなんなのか、として「探された」結果として、この姿があるわけで、少しも「直感的」な理由から選ばれていないわけである。
もちろん、このＺＦＣが矛盾がないのであれば、それでいいと言えるのかもしれない。しかし、矛盾がないことはゲーデルの不完全性定理から、それが言えると考えることには限界があることが分かっている。しかし、とりあえず今のところは矛盾は見付かっていない。だったら、これでいいんじゃないかと考えるかもしれないが、ようするに

• これが「数学の基礎」と言うには、あまりに「人工的」なんじゃないのか？

という、気持ち悪さが残っているわけである。
この問題に対して、おそらく数学の「歴史」は、今までのところ、あまりはかばかしい達成をあげていないんじゃないのかと思っている。ただ、一つ。まあ、昔から知られている結果ではあるが、おもしろいアプローチが知られている。それが、

• カテゴリー（圏論）

である。つい最近、以下の本を読んでいたら、第３章が「集合論について」となっている。

集合論の圏論的な公理のうち評判のよいものを一つ選ぶと、形式ばらない要約は次のようになる。

1. 関数の合成は結合的で恒等射をもつ
2. 終対象が存在する
3. 元のない集合が存在する
4. 関数は元への効果で決定される
5. 集合ＡとＢについて、積Ａ×Ｂが構成できる
6. 集合ＡとＢについて、ＡからＢへの関数の集合を構成できる
7. ｆ:Ａ→Ｂとｂ∈Ｂについて、逆像ｆ^−１｛ｂ｝を構成できる
8. Ａの部分集合は、Ａから｛０、１｝への関数と対応する
9. 自然数たちが集合をなす
10. すべての全射は切片をもつ

この非形式的な要約は、「元」や「逆像」といった用語を用いているが、それは集合、関数、合成という基本概念を使って定義できるものだ。たとえば、集合Ａの元は終集合からの射として定義される。
これらの公理は確実に都合よく、圏論の言葉で表現できる。たとえば、最初の公理は集合と関数が圏をなすといっており、１０個すべてを合わせたものは、圏論通の専門用語で「集合と関数は自然数対象と選択をもつwell-pointedトポスになる」と表現される。しかし公理を述べるためには、いかなる圏論の再燃にも訴える必要はなく、集合と関数の言葉で表現できる。詳細は Lawvere-Rosebruch(2003) あるいは Leinster(2014) を参照されたい。

ベーシック圏論 普遍性からの速習コース

ここで引用した個所が上記までの議論とどんな関係があるのか、という話なのだが、

The relation between our axioms and ZFC is well understood. The ten axioms are weaker than ZFC; but when the eleventh is added, the two theories have equal strength and are 'bi-interpretable' (the same theorems hold). Moreover, it is known to which fragment of ZFC the ten axioms correspond: 'Zermelo with bounded comprehension and choice'. The details of this relationship were mostly worked out in the early 1970s [2, 14, 15]. Good modern accounts are in Section VI.10 of [7] and Chapter 22 of [9].
（Tom Leinster. Rethinking set theory.(2014)）
[1212.6543] Rethinking set theory

上記の公理のより詳しい説明は、Leinster(2014)によくまとまっている。
ようするに、上記の引用にある圏論的な公理は

• 集合論ではない（「集合」と「属する」という「無定義用語」によって、公理系を記述していない。あくまで「圏論」流に、「対象Ａから対象Ｂへの射」という「無定義用語」しか本質的に使っていない。一見、「集合論」的な無定義用語は出現するが、それはあくまで「定義」という、用語上の簡易性から導入されているにすぎない。）
• 直感的に、これらの公理が「大きすぎない」（ＺＦＣのように、直感的に言い過ぎていると思われるような主張がない。）
• ＺＦＣより「弱い」公理系であるが、これにある「公理」を加えれば、ＺＦＣと相当な内容だと解釈できる。

ちなみに、最後のＺＦＣとの相等性については、以下の論文で議論されていて、

Gerhard Osius. Categorical set theory: A characterization of the category of sets. (1974)
Categorical set theory: A characterization of the category of sets - ScienceDirect

また、以下の教科書では、上記の圏論的な枠組みの中で、実数の構成まで記述されている。

S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic. (1994)
Sheaves in Geometry and Logic

つまり、この公理系が魅力的なのは実際にその主張内容が、「私たちに直感的に理解可能なもの」しかないが、他方において、ＺＦＣの弱い主張と解釈できるとするなら、これを

• 数学の「基礎」

とすることは、どこまで可能なのか、ということになる、というわけである。つまり、圏論的な道具の中で、なにがＺＦＣと「同一」の主張であるのか、といった衒学的な議論を超えて、こういった「弱い」主張はそれなりの数学の「安全さ」や「健全さ」を示している可能性がある、と考えられないか、というわけである...。