分出公理

**分出公理図式**（）または**分出公理**とは、ツェルメロ＝フレンケル集合論などの集合論の公理系を構成する公理図式の一つである。**部分集合公理**、**制限された内包公理（図式）**ともいう。本質的に、どの集合の定義可能な部分クラスも集合であることを主張する。

**内包公理（図式）**（）と呼ばれることもあるが、この語は後述のように**無制限の内包**（）の意味で用いられる場合がある。

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

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

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

\forall w_1\ \dots\ \forall w_n\ \forall A\ \exist B\ \forall x\left[x\in B\hArr\left[x\in A\land\varphi\left(x,\,w_1,\,\dots,\,w_n,\,A\right)\right]\right]

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

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

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

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

## 置換公理との関係

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

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

\forall A\ \exist B\ \forall C\left[C\in B\hArr\exist 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* は空集合となり、分出公理は置換公理と空集合の公理から導かれる。

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

## 無制限の内包公理と、ラッセルのパラドックス

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

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

:\forall w_1\ \dots\ \forall w_n\ \exist B\ \forall x\left[x\in B\hArr\varphi\left(x,\,w_1,\,\dots,\,w_n\right)\right]

B に相当する集合は一意に定まり、ふつう  と表される。

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

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

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

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

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

この定理スキーマ自体は内包公理の制限された形であり、  が集合という制限によってラッセルのパラドックスを防ぐ。すると、集合に対する分出公理は以下のように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* である。 

この公理では、述語  がクラス  で置き換えられ、量化子の範囲をクラス  にできる。同じ効果のより簡潔な公理としては\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)を含む二階述語論理や高階述語論理において、分出公理は論理的に妥当であり、理論中に陽的に含まれている必要はない。

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

## 参考文献