仕様の公理図式

公理的集合論の多くの一般的なバージョンでは、仕様の公理図式^{[ 1 ]}（分離の公理図式（Aussonderungsaxiom ） [ ^{2 ] [ 3 ] 、}部分集合公理^{[ 4 ]}、クラス構成の公理[ ^{5 ]}、または制限付き内包公理図式^{[ 6 ]}とも呼ばれる）は公理図式である。本質的に、それは集合の定義可能な部分クラスはすべて集合であると述べて^いる。

一部の数学者はこの公理を「理解の公理図式」と呼ぶが、他の数学者はその用語を無制限の理解にのみ用いる。この公理は無制限の理解の「制限付き」バージョンである。理解を制限することでラッセルのパラドックスを回避できるため、ツェルメロ、フランケル、ゲーデルを含む数人の数学者はこれを集合論で最も重要な公理とみなした。^{[ 7 ]}

各数式 につき、スキーマのインスタンスが1つ含まれています。${\displaystyle \varphi }$⁠自由変数を含む集合論の言語では、${\displaystyle x,w_{1},w_{2},\ldots ,w_{n},A}$⁠。したがって、セットは⁠${\displaystyle B}$⁠、その存在は公理によって主張されているが、 ⁠には自由には現れない${\displaystyle \varphi }$集合論の形式言語では、公理図式は次のようになります。

${\displaystyle \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がBの要素であるのは、x が A の要素であり、かつ⁠の場合に限る。${\displaystyle \varphi }$⁠ xに対して成り立つ。

すべての述語に対して1つの公理が存在することに注意してください。${\displaystyle \varphi }$したがって、これは公理図式です。

この公理図式を理解するには、集合B がAの部分集合でなければならないことに注意してください。したがって、この公理図式が実際に言っていることは、集合Aと述語が与えられたとき、${\displaystyle \varphi }$⁠ 、 Aの部分集合Bを見つけることができ、その要素はAの要素のうち、 を満たすものだけである。${\displaystyle \varphi }$外延性の公理により、この集合は一意です。通常、この集合は集合構成記法を用いて次のように表されます。${\displaystyle B=\{x\in A\mid \varphi (x)\}}$したがって、この公理の本質は次のとおりである。

述語によって定義される集合のすべてのサブクラスは、それ自体が集合である。

前述の分離形式は、1930 年にThoralf Skolemによって、Zermelo による以前の非一階^{[ 8 ]形式を改良したものとして導入されました。 [ 9 ]}仕様の公理図式は、通常の集合論ZFCに関連する公理的集合論のシステムの特徴ですが、根本的に異なる代替集合論のシステムでは通常現れません。たとえば、新基礎論と正定値集合論は、素朴集合論の理解公理の異なる制限を使用します。Vopenkaの代替集合論は、半集合と呼ばれる集合の適切な部分クラスを許容するという特定の点を強調しています。ZFC に関連するシステムでも、この図式は、クリプキ-プラテック集合論の urelementsのように、有界量化子を持つ式に限定されることがあります。

仕様の公理図式は、置換の公理図式と空集合の公理によって暗示される。^{[ 10 ] [ a ]}

置換の公理図式によれば、関数が${\displaystyle f}$式で定義できる${\displaystyle \varphi (x,y,p_{1},\ldots ,p_{n})}$すると任意の集合に対して${\displaystyle A}$集合が存在する${\displaystyle B=f(A)=\{f(x)\mid x\in A\}}$:

${\displaystyle {\begin{aligned}&\forall x\,\forall y\,\forall z\,\forall p_{1}\ldots \forall p_{n}[\varphi (x,y,p_{1},\ldots ,p_{n})\wedge \varphi (x,z,p_{1},\ldots ,p_{n})\implies y=z]\implies \\&\forall A\,\exists B\,\forall y(y\in B\iff \exists x(x\in A\wedge \varphi (x,y,p_{1},\ldots ,p_{n})))\end{aligned}}}$[ ^{10 ]​}

仕様の公理図式を導出するために、${\displaystyle \varphi (x,p_{1},\ldots ,p_{n})}$公式であり、${\displaystyle z}$セットを定義し、関数を定義します${\displaystyle f}$そのため${\displaystyle f(x)=x}$もし${\displaystyle \varphi (x,p_{1},\ldots ,p_{n})}$真実であり、${\displaystyle f(x)=u}$もし${\displaystyle \varphi (x,p_{1},\ldots ,p_{n})}$偽である、${\displaystyle u\in z}$そのため${\displaystyle \varphi (u,p_{1},\ldots ,p_{n})}$が真である。すると、セットは${\displaystyle y}$置換の公理図式によって保証されるのはまさに集合である${\displaystyle y}$仕様の公理図式で必須。${\displaystyle u}$存在しない場合${\displaystyle f(x)}$仕様の公理図式には空集合があり、その存在（すなわち、空集合の公理）が必要となる。^{[ 10 ]}

このため、仕様の公理図式は、ZF（ツェルメロ・フレンケル集合論）のいくつかの公理化から除外されている^{[ 11 ]}が、冗長性があるにもかかわらず両方を含める著者もいる^{[ 12 ]} 。いずれにせよ、仕様の公理図式は、フレンケルが1922年に置換公理を発明する前の、ツェルメロの1908年の公理リストに含まれていたため注目に値する^{[ 11 ]。}さらに、ZFC集合論（つまり、選択公理を持つZF）から置換公理と集合公理を削除し、仕様の公理図式を残すと、 ZC（つまり、ツェルメロの公理に選択公理を加えたもの）と呼ばれるより弱い公理系が得られる^{[ 13 ] 。}

無制限内包の公理図式は次のようになる。

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

つまり：

この集合Bもまた一意であり、通常は{ x  : φ ( x , w ₁ , ..., w _b )} と表記されます。

非公式なレベルでは、この公理図式は、任意の性質または条件φ (集合の述語) に対して、集合が存在する、と説明できます。${\displaystyle \{x|\varphi (x)\}}$φ を満たすすべての対象のみで構成される。^{[ 14 ] [ 15 ]}例えば、φがトートロジーである場合、結果として得られる集合Bは普遍集合である。

この公理図式は、厳密な公理化が採用される以前の素朴な集合論の初期には暗黙のうちに用いられていました。しかし、後に、 φ ( x )を¬ ( x∈x ) （すなわち、集合xがそれ自身を要素としない性質）とみなすことで、ラッセルのパラドックスに直接つながることが判明しました。したがって、集合論の有用な公理化において、無制限内包表記を用いることはできません。古典論理から直観主義論理に移行しても、ラッセルのパラドックスの証明は直観主義的に妥当であるため、この問題は解決しません。  

仕様の公理図式は、この公理図式の「制限された」バージョンと見なすことができ、φ は別の集合Aの要素に対してのみ真となり、したがって普遍集合のような「大きすぎる」集合の構成を禁じます。仕様の公理図式のみを受け入れることが、公理的集合論の始まりでした。その後、ツェルメロ・フレンケル公理​​のほとんど (ただし、外延公理、正則性公理、選択公理を除く) は、理解の公理図式を仕様の公理図式に変更することによって失われたものを補うために必要になりました。これらの公理はそれぞれ、ある集合が存在することを述べ、その集合の要素が満たすべき述語を与えることによってその集合を定義します。つまり、それは理解の公理図式の特殊なケースです。

また、スキーマの矛盾を防ぐために、適用できる式を制限することも可能である。例えば、新基礎論（下記参照）では階層化された式のみ、正集合論では正式（論理積、論理和、量化、原子式のみを含む式）のみに適用できる。しかしながら、正式は一般的に、ほとんどの理論で表現できる特定の事柄を表現できない。例えば、正集合論には補集合や相対補集合は存在しない。

フォン・ノイマン＝ベルナイズ＝ゲーデルの集合論では、集合とクラスが区別される。クラスCは、あるクラスEに属する場合に限り集合となる。この理論には、次のような定理図式 がある。$${\displaystyle \exists D\forall C\,([C\in D]\iff [P(C)\land \exists E\,(C\in E)])\,,}$$

つまり、

ただし、述語Pにおける量化子は集合に限定されるものとする。

この定理図式自体は、 Cが集合であるという要件によってラッセルのパラドックスを回避する、制限された形式の内包表記である。そして、集合自体の仕様は単一の公理として記述できる。 $${\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])])\,,}$$

つまり、

あるいはもっと簡単に

この公理では、述語Pは量化可能なクラス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])\,,}$$

つまり、

述語を量化できる型付き言語では、仕様の公理スキーマは単純な公理になります。これは、前のセクションのNBG公理で使用された手法とほぼ同じで、述語をクラスに置き換え、そのクラスに対して量化を行いました。

二階述語論理および高階意味論を伴う高階述語論理においては、仕様公理は論理的妥当性であり、理論に明示的に含める必要はない。

WVO Quineが先駆的に提唱した集合論のNew Foundationsアプローチでは、与えられた述語に対する理解公理は無制限の形式をとりますが、スキーマで使用できる述語自体は制限されています。述語 ( CはCに含まれない) は禁止されています。なぜなら、同じ記号C がメンバーシップ記号の両側に現れるため (したがって、異なる「相対型」に現れる) 、ラッセルのパラドックスが回避されるからです。しかし、P ( C )を( C = C )とすることで、すべての集合の集合を形成できます。詳細は、階層化を参照してください。^{[ 16 ]}