分出公理

主な公理的集合論の多くにおいて、分出公理（英: axiom schema of specification）、部分集合公理、制限された内包公理とは、公理型の一つである。本質的に、どの集合の定義可能な部分クラスも集合であることを主張する。

分出公理を内包公理（axiom schema of comprehension）と呼ぶ数学者もいるが、後述のように無制限の内包（unrestricted complehension）と呼ぶ者もいる。

制限された内包公理はラッセルのパラドックスを回避できるため、ツェルメロ、フレンケル、ゲーデルといった数学者は、集合論の最重要な公理と考えた。

主張

x, w₁, ..., w_n, A を自由変数とする集合論の言語における論理式 φ ごとに、公理型のインスタンスが1つずつ含まれる（公理型の中の1つの公理が含まれる）。ゆえに B は φ において自由変数でない。集合論の形式言語において、この公理型は以下のように表される：

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

すなわち：

どの集合 A に対しても、以下を満たす集合 B が（A の部分集合として）存在する：どの集合 x に対しても、x が A の元でかつ φ が x で成り立つ場合かつそのときに限り x が B の元である。

そのような述語 φ それぞれに対して一つの公理が存在することに注意。つまり、これは公理型である。

この公理型を理解するために、集合 B は A の 部分集合である必要があることに注意しよう。つまり、公理型の実際の主張は、 集合 A と述語 P に対して、A の部分集合であって、その元が P を満たす A の元となる集合 B が見つかる、ということである。外延性の公理より、この集合は唯一つ定まる。この集合はよく、 {C ∈ A : P(C)} といった集合の内包表記を用いて表される。結局、この公理の本質はこういうことである：

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

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

置換公理との関係

分出公理はほとんど置換公理から導出することが可能である。

まず、置換公理を思い出そう：

$\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 は空集合となり、分出公理は置換公理と空集合の公理から導かれる。

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

無制限の内包公理

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

$$\forall w_{1},\ldots ,w_{n}\,\exists B\,\forall x\,(x\in B\Leftrightarrow \varphi (x,w_{1},\ldots ,w_{n}))$$

すなわち：

元がまさしく述語 φ を満たす対象すべてである（元と述語 φ を満たす対象が1対1対応する）集合 B が存在する。

この集合 B はまた唯一定まり、ふつう {x : φ(x, w₁, ..., w_b)} と表される。

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

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

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

NBGクラス理論において

フォン・ノイマン＝ベルナイス＝ゲーデル集合論においては、集合とクラスが区別される。クラス C は、あるクラス E の元であるとき、またそのときに限り集合である。この理論においては、以下の定理スキーマが存在する。

$$\exists D\forall C\,([C\in D]\iff [P(C)\land \exists E\,(C\in E)])\,,$$

すなわち、

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

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

この定理スキーマ自体は内包公理の制限された形であり、C が集合という制限によってラッセルのパラドックスを防ぐ。すると、集合に対する分出公理は以下のように1つの公理で記述できる。

$$\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 にできる。同じ効果のより簡潔な公理としては

$$\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])\,,$$

すなわち、

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

高階述語論理において

述語を量化できる型付き言語において、分出公理は簡潔な公理になる。これは前節のNBG公理系で使った、述語をクラスで置き換えてクラスを量化できるようにする手法とまさしく同じものである。

高階の意味論(semantics)を含む二階述語論理や高階述語論理において、分出公理は論理的に妥当であり、理論中に陽的に含まれている必要はない。

クワインの新基礎集合論において

クワインが始めた、集合論に対する新基礎集合論のアプローチでは、与えられた述語に対する内包公理は無制限の形となるが、この公理型で使われうる述語は制限されている。述語 (C は C に含まれない) は、同じシンボル C が所属関係シンボルの両辺に現れるために（異なる「相対型」についても同様に）禁止されている。つまり、ラッセルのパラドックスは回避される。しかし、P(C) を (C = C) とすると（これは許容されている）、すべての集合の集合を作れてしまう。詳細は階層化を参照。