さて、今回は、「集合論の公理系」 として ZF と BG の公理系を扱ってみましょう。

　「ラッセル の パラドックス」 が論点になった以後、集合の全体 （すべての集合をひとまとめにした モノ） を集合と呼んではいけないことになった。そこで、集合があまり大きくならないように、集合の生成方法が 「公理 （axiom）」 として扱われることになった。それを公理的集合論という。

　ツェルメロ （Zermelo, E.） は、{ x | x ∈ A } の代わりに、{ x ∈ a | A (x) } の形を集合とすることを提示した。
　これを分出公理という。

　すなわち、もう 1つの集合 （集合 a） を介在して、あまり大きくならない集合 （集合 a よりも小さい集合） を導入した。
　言い換えれば、{ x ∈ a | A (x) } は集合 a の部分集合である。そのために、分出公理のことを 「内包の公理」 とか 「部分集合の公理」 ともいう。この集合 { x ∈ a | A (x) } を セット と云う。

　集合 X の メンバー x について、判断 f (x) があって、真を 「1」 とし偽を 「0」 として、真理集合 S ＝ { 0, 1 } をとれば、f は S への関数として考えることができる。そこで、f (x) ＝ 1 となる メンバー を集めれば集合になる [ Y ＝ { x ∈ X | f (x) ＝ 1 ｝] というのが分出公理である。分出公理は述語論理式を使って表現すれば、以下のようになる。

　　　∀a ∃b ∀x [（x ∈ b） ⇔ （x ∈ a） ∧ Ａ (x) ].

　ところが、分出公理からは、{ a, b } とか a∪b とか集合族などを導出することができないので、他のいくつかの規約が公理 （前提） として扱われることになった。その公理系を大成した人物が ツェルメロ であるが、その公理系のなかに、フレンケル （Franckel, A.） が 1つの公理を加えて、「矛盾が起こらないように」 集合を扱うことができるようになったので、その公理系が集合論の安全基準として使われてきた。
　その公理系を Zermelo-Franckel の集合論といい、「ZF」 というふうに省略することが多い。ZF の公理系には以下の特徴がある。

　　（1） 等号をふくむ第一階述語論理を使って形式化されている。
　　（2） 9つの公理をもつ形式的体系である。
　　（3） ∈ 以外の述語を使わない。

[ 参考 ]
　等号の公理 （axiom of equality） というのは、任意の a, b に対して、∀x [ a ＝ b ⇒（a ∈ x ⇔ b ∈ x）] が成立することをいう。
　（述語論理式という言いかたに対して） 集合論的論理式という言いかたをすることもあるが、集合論的論理式というのは、∈ （メンバー である） という述語だけを使って作成される論理式のことをいう。
　なお、ZF のそれぞれの公理について、詳しく知りたいなら、集合論や数学基礎論の文献を読んでください。

　
　ZF の公理系は、単純に言えば、集合の構成法を提示して、どのような モノ が集合として考えられるか、という点を明晰にした体系である。

　フォン・ノイマン （Neumann, J.L.V.） は、記号論理の手法を使って、いっそうの形式化をして集合論を拡張した。
　そして、ベルナイス （Bernays, P.） と ゲーデル （Godel, K.） が、ノイマン の形式化を単純な形に整理した。
　形式的に拡張された集合論を Bernays-Godel の集合論といい、「BG」 というふうに省略することが多い。
　BG では、A (u) を任意の集合論的論理式とする。{ u | A (u) ｝ の存在は、ZF から得られない。
　{ u | A (u) } を クラス （class） と呼ぶ。

　第一階述語論理のなかで、集合論的論理式は、クラス に関する束縛変数を含まない論理式をいう。
　すなわち、A (u) を任意の集合論的論理式とするとき、以下を公理に加える。
　　　∃X ∀u { u ∈ X ≡ A (u) }.　　（X は クラス に関する変数とする。）

　なお、ZF で証明される論理式は BG で証明されるし、BG で証明される集合論的論理式は ZF で証明できる。 □