分出公理
分出公理はほとんど置換公理から導出することが可能である。
まず、置換公理を思い出そう:
∀ A ∃ B ∀ C ( C ∈ B ⟺ ∃ D [ D ∈ A ∧ C = F ( D ) ] ) {\displaystyle \forall A\,\exists B\,\forall C\,(C\in B\iff \exists D\,[D\in A\land C=F(D)])}
上記命題が、A, B, C, D 以外のシンボルで表される1変数の任意の関数述語 F についても成り立つというものである。分出公理に適切な述語 P を考え、写像 F を P(D) が真なら F(D) = D 、偽なら F(D) = E と定義する。ここで、 E は P(E) が真となる A の任意の元である。すると、置換公理によって、集合 B がまさしく分出公理に必要な集合 B であるとみなせる。唯一の問題は、そのような E が存在しないときである。しかしそのような場合は、分出公理に必要な集合 B は空集合となり、分出公理は置換公理と空集合の公理から導かれる。
こうした理由で、分出公理はツェルメロ-フレンケル公理系の現代的なリストからはしばしば省かれる。しかし、歴史的経緯や、以下の節に示す集合論の代替的公理との比較を考えると、分出公理はやはり重要である。
無制限の内包公理とは、以下のものである:
すなわち:
元がまさしく述語 φ を満たす対象すべてである(元と述語 φ を満たす対象が1対1対応する)集合 B が存在する。
この集合 B はまた唯一定まり、ふつう {x : φ(x, w1, ..., wb)} と表される。
この公理型は、厳密な公理化がなされる前の初期の素朴集合論では暗黙のうちに使われていた。残念なことに、φ(x) に ¬(x ∈ x) (集合 x が自身の元ではないという属性)をとると、直接ラッセルのパラドックスが導かれてしまう。そのため、集合論において無制限の内包公理を扱える実用的な公理化は存在しない。ラッセルのパラドックスは直観主義論理でも成り立つため、古典論理から直観主義論理に切り替えたとしても同じ問題が生じる。
分出公理のみを許容することが公理的集合論の始まりであった。