現代数学では、集合論 ZFC を基礎として、理論を展開しています。
もちろん、数学基礎論の分野では、様々な形式的体系が扱われますが、
その点は、私はあまり詳しくありません。
ここに、二冊、本があります。
超限論的選択関数を論理体系の中に組み込み、
選択公理が定理として証明されるようになっています。
論理式の記述の豊かさに於いては、
通常使用される形式的体系としての
ZFC よりも豊かです。
現代、普通に使われている順序数の定式化もありません。
その代わり、整列集合に関する記述は
詳しく、素晴らしいものがあります。
ここで、私自身の覚書も兼ねて、集合論初心者のために、
書いておきます。
まず、良く知られた結果から。
ZFC の保存拡大である。
（ここで、保存拡大の意味は、超限論的選択関数なしで表現できる論理式
（変数を表す文字と ∈、＝、⇒、￢、∧、∨、∀、∃の組み合わせで書ける論理式）
については、ブルバキ集合論＋正則性公理に於いて証明可能であることと、
ZFCに於いて証明可能であることとが、同値になるということです。）
２） 集合論 BGE (集合論 BG に強選択公理を付け足したもの)
は、ZFC の保存拡大である。
（ここでの保存拡大の意味は、集合についてのみ主張する論理式
については、BGE で証明可能と ZFC で証明可能は同値になると
いうことです。）
この辺の結果を速やかに知りたい方は、MathSciNet で、文献を探して読んでください。
キーワードしだいですが、必ず見つかります。
尤も、強制法を学習し、慣れた人ならば、自力で証明を与えられると思います。
私は、「U. Felgner 」の論文：
Comparison of the axioms of local and universal choice,
Fund. Math. 71 (1971), 43-62.
を参考にして、強制法とゲンツェンの LK を使い、
２）に有限の立場での証明を与えたことがあります。
その時のノートが以下になります:
そのときは、すでに他の人が証明して30年以上経った後だったんですけどね。苦い思い出です。
(Felgner の論文では、超限論的な証明を与えています。
1971年当時は、有限の立場での証明が可能かどうかは、未解決でした。)
次に、マイナーな結果
３）ブルバキ集合論は、ZFC から正則性公理をのぞいた形式的体系
の保存拡大にはなっていない。
この結果は、私は検証していませんが（無責任？）、
Sets and Classes (Paul Bernays) に書いてあります。
以上のことから、ブルバキ集合論を数学の道具として使う立場の人は、
正則性公理も追加して、お使いになられると良いでしょう。
そのほうが、ZFC との関係がすっきりしますし、
順序数の定式化も楽ですから。
文責: Dr. Kazuyoshi Katogi
