分出公理

${\displaystyle x}$、${\displaystyle w_{1}}$、...、${\displaystyle w_{n}}$、${\displaystyle A}$ を自由変数とする集合論の言語における論理式 ${\displaystyle \varphi }$ ごとに、公理図式のインスタンスが一つずつ含まれる（公理図式の中の一つの公理が含まれる）。ゆえに ${\displaystyle B}$ は ${\displaystyle \varphi }$ において自由変数でない。集合論の形式言語において、この公理図式は下記のように表される。

任意の集合 ${\displaystyle A}$ について、${\displaystyle A}$ のある部分集合 ${\displaystyle B}$ が存在し、${\displaystyle A}$ の任意の元 ${\displaystyle x}$ について、${\displaystyle \varphi }$ が ${\displaystyle x}$ で成り立つ場合かつそのときに限り ${\displaystyle x}$ は ${\displaystyle B}$ の元である。

${\displaystyle \forall w_{1}\ \dots \ \forall w_{n}\ \forall A\ \exists B\ \forall x\left[x\in B\Leftrightarrow \left[x\in A\land \varphi \left(x,\,w_{1},\,\dots ,\,w_{n},\,A\right)\right]\right]}$

そのような述語 ${\displaystyle \varphi }$ それぞれに対して一つの公理が存在することに注意。つまり、これは公理図式である。

この公理図式を理解するために、集合 ${\displaystyle B}$ は ${\displaystyle A}$ の 部分集合である必要があることに注意しよう。つまり、公理図式の実際の主張は、集合 ${\displaystyle A}$ と述語 ${\displaystyle P}$ に対して、${\displaystyle A}$ の部分集合であって、その元が ${\displaystyle P}$ を満たす ${\displaystyle A}$ の元となる集合 ${\displaystyle B}$ が見つかる、ということである。外延性の公理より、${\displaystyle B}$ に相当する集合は唯一つ定まり、${\displaystyle \left\{C\in A\,|\,P\left(C\right)\right\}}$（集合の内包表記）と表記される。結局、この公理の本質はこういうことである：

述語で定義される集合のどの部分クラスも集合である。

分出公理は、一般的な集合論 ZFC に関連する公理的集合論のシステムに特徴的なものであるが、根本的に異なる代替集合論のシステムではほとんど見られない。例えば、新基礎集合論や en:positive set theory では、素朴集合論の内包公理という、異なる制限が用いられる。Vopenka の代替集合論では、準集合（semiset）（英語版）と呼ばれる、集合の真部分クラスを認めることの正しさを主張する。 ZFC に関連したシステムにおいても、en:Kripke-Platek set theory with urelementsのように、分出公理は有界量化子の式で制限されることがある。

分出公理はほとんど置換公理から導出である。

まず、置換公理を思い出そう。${\displaystyle A}$、${\displaystyle B}$、${\displaystyle C}$、${\displaystyle D}$ 以外のシンボルで表される一変数の任意の関数述語 ${\displaystyle F}$ についても成り立つというものである。

${\displaystyle \forall A\ \exists B\ \forall C\left[C\in B\Leftrightarrow \exists D\left[D\in A\land C=F\left(D\right)\right]\right]}$

分出公理に適切な述語 P を考え、写像 F を P(D) が真なら F(D) = D 、偽なら F(D) = E と定義する。ここで、 E は P(E) が真となる A の任意の元である。すると、置換公理によって、集合 B がまさしく分出公理に必要な集合 B であるとみなせる。唯一の問題は、そのような E が存在しないときである。しかしそのような場合は、分出公理に必要な集合 B は空集合となり、分出公理は置換公理と空集合の公理から導かれる。

こうした理由で、分出公理はツェルメロ＝フレンケル公理系の現代的なリストからはしばしば省かれる。しかし、歴史的経緯や、以下の節に示す集合論の代替的公理との比較を考えると、分出公理はやはり重要である。

無制限の内包公理とは、以下のものである。

元がまさしく述語 ${\displaystyle \varphi }$ を満たす対象すべてである（元と述語 ${\displaystyle \varphi }$ を満たす対象が一対一対応する）集合 ${\displaystyle B}$ が存在する。

${\displaystyle \forall w_{1}\ \dots \ \forall w_{n}\ \exists B\ \forall x\left[x\in B\Leftrightarrow \varphi \left(x,\,w_{1},\,\dots ,\,w_{n}\right)\right]}$

${\displaystyle B}$ に相当する集合は一意に定まり、ふつう {x : φ(x, w₁, ..., w_b)} と表される。

この公理図式は、厳密な公理化がなされる前の初期の素朴集合論で暗黙に使われていた。残念なことに、${\displaystyle \varphi \left(x\right)}$ に ¬(x ∈ x) （集合 x が自身の元ではないという属性）をとると、直接ラッセルのパラドックスが導かれてしまう。そのため、集合論において無制限の内包公理を扱える実用的な公理化は存在しない。ラッセルのパラドックスは直観主義論理でも成り立つため、古典論理から直観主義論理に切り替えても同じ問題が生じる。

分出公理のみを許容することが公理的集合論の始まりであった。他のほとんどのツェルメロ＝フレンケル公理（外延性の公理、正則性公理、選択公理を除く）は、内包公理を分出公理に置き換えるために失われる一部を補うために必要であった。これらの公理は特定の集合について、存在を主張するとともに、その元が満たすべき述語によって定義する。すなわち、これは内包公理の特別な場合である。

新基礎集合論（後述）の階層化された論理式のみの使用や en:positive set theory の positive 式（論理積、論理和、量化、原子式のみからなる式）のみの使用というように、適用される式を制限することで、無制限の内包公理から矛盾を生じないようにすることもできる。しかし positive formulae は、ほとんどの理論で表現できる特定の事柄を表現できない。例えば、positive set theory には補集合や相対的補集合が存在しない。

フォン・ノイマン＝ベルナイス＝ゲーデル集合論においては、集合とクラスが区別される。クラス C は、あるクラス E の元であるとき、またそのときに限り集合である。この理論においては、以下の定理スキーマが存在する。$${\displaystyle \exists D\forall C\,([C\in D]\iff [P(C)\land \exists E\,(C\in E)])\,,}$$すなわち、

クラス C が P を満たす集合のとき、またそのときに限って、どのクラス C もクラス D の元であるようなクラス D が存在する 。

この定理スキーマによって、述語 P の量化子は集合に制限される。

この定理スキーマ自体は内包公理の制限された形であり、C が集合という制限によってラッセルのパラドックスを防ぐ。すると、集合に対する分出公理は以下のように1つの公理で記述できる。$${\displaystyle \forall D\forall A\,(\exists E\,[A\in E]\implies \exists B\,[\exists E\,(B\in E)\land \forall C\,(C\in B\iff [C\in A\land C\in D])])\,,}$$すなわち、

任意のクラス D と任意の集合 A に対して、元がまさしく A と D の元である集合 B が存在する。

もしくはもっと簡潔に、

クラス D と集合 A の共通部分は集合 B である。

この公理では、述語 P がクラス D で置き換えられ、量化子の範囲をクラス D にできる。同じ効果のより簡潔な公理としては$${\displaystyle \forall A\forall B\,([\exists E\,(A\in E)\land \forall C\,(C\in B\implies C\in A)]\implies \exists E\,[B\in E])\,,}$$すなわち、

集合の部分クラスは集合である。