仕様の公理スキーマ

公理的集合論の多くの一般的なバージョンでは、仕様公理スキーマ^[1]、分離公理スキーマ（Aussonderungsaxiom）^[2]、 部分集合公理^[3]、クラス構築公理^[4]、または制限付き理解公理スキーマは公理スキーマです。本質的には、集合の 定義可能なサブクラスはすべて集合であると述べています。

一部の数学者はこれを「理解の公理スキーム」と呼んでいますが、他の数学者はこの用語を以下で説明する「無制限の理解」に対して使用します。

理解を制限することでラッセルのパラドックスを回避できるため、ツェルメロ、フランケル、ゲーデルを含む多くの数学者はそれを集合論の最も重要な公理とみなしました。^[5]

集合論の言語では、を自由変数とする各式 に対して、スキーマのインスタンスが 1 つ含まれています。したがって、 はでは自由に出現しません。^{[3] [2] [6]}集合論の形式言語では、公理スキーマは次のようになります。 ${\displaystyle \varphi (x)}$${\displaystyle x}$${\displaystyle S}$${\displaystyle \varphi (x)}$

${\displaystyle \forall A\,\exists S\,\forall x\,{\big (}x\in S\iff (x\in A\wedge \varphi (x)){\big )}}$^{[3] [1] [6]}

または言葉で言うと:

を式とする。任意の集合に対して、が成り立つようなすべての要素からなる集合が存在する。^[3]${\displaystyle \varphi (x)}$${\displaystyle A}$${\displaystyle S}$${\displaystyle x\in A}$${\displaystyle \varphi (x)}$

このような述語 ごとに1つの公理が存在することに注意してください。つまり、これは公理スキーマです。^{[3] [1]}${\displaystyle \varphi (x)}$

この公理スキーマを理解するには、集合がAのサブセットでなければならないことに注意してください。したがって、公理スキーマが実際に言っているのは、集合と述語 が与えられた場合、を満たすAのメンバーとまったく同じメンバーを持つAのサブセットを見つけることができるということです。外延性公理により、この集合は一意です。通常、この集合は集合構築記法を使用してと表します。したがって、公理の本質は次のとおりです。 ${\displaystyle S}$${\displaystyle A}$${\displaystyle \varphi (x)}$${\displaystyle S}$${\displaystyle \varphi (x)}$${\displaystyle S=\{x\in A|\varphi (x)\}}$

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

前述の分離形式は、1930年にトラルフ・スコーレムによって、以前の非一階形式^[7]のツェルメロ^[8]の改良版として導入されました。仕様指定の公理スキームは、通常の集合論ZFCに関連する公理集合論のシステムの特徴ですが、根本的に異なる代替集合論のシステムでは通常現れません。たとえば、新基礎理論と正値集合論は、素朴集合論の内包公理の異なる制限を使用します。ヴォペンカの代替集合論は、半集合と呼ばれる集合の適切なサブクラスを許可することに特に重点を置きます。ZFCに関連するシステムでも、このスキームは、固有元を持つクリプキ-プラテック集合論のように、有界量指定子を持つ式に制限されることがあります。

仕様公理スキーマは、置換公理スキーマと空集合公理によって暗示される。^{[9] [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}}}$^[9 ]

仕様化の公理スキーマを導くには、を式と集合とし、が真で、が偽である場合には となる関数を定義します。ここで、 は真です。すると、置換の公理スキーマによって保証される集合は、まさに仕様化の公理スキーマで要求される集合になります。 が存在しない場合は、仕様化の公理スキーマには空集合があり、その存在（つまり、空集合の公理）が必要になります。^[9]${\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)}$

このため、仕様公理スキーマは、ZF（ツェルメロ-フランケル）集合論のいくつかの公理化から除外されているが、^[10]一部の著者は、冗長性にもかかわらず、両方を含めている。^[11]いずれにしても、仕様公理スキーマは、フランケルが1922年に置換公理を発明する前の1908年のツェルメロの公理の最初のリストにあったため注目に値する。 ^[10]さらに、ZFC集合論（つまり、選択公理を含むZF）を採用し、置換公理と収集公理を削除し、仕様公理スキーマを保持すると、 ZCと呼ばれるより弱い公理系（つまり、ツェルメロの公理に選択公理を加えたもの）が得られる。^[12]

無制限理解の公理スキーマは次のようになります。

$${\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 , w1 , ..., wb )}と表記されます。

非分類物質集合論では、完全または無制限の理解の公理または規則は、任意の特性Pに対して、 Pを満たすすべてのオブジェクトの集合{ x | P ( x )}が存在することを述べています。 ^[13]

この公理スキームは、厳密な公理化が採用される前の素朴な集合論の初期に暗黙的に使用されていました。しかし、後に、 φ ( x )を¬ ( x  ∈  x ) (つまり、集合xがそれ自身のメンバーではないという性質) と見なすことで、ラッセルのパラドックスに直接つながることが発見されました。したがって、集合論の有用な公理化は無制限の理解を使用することはできません。ラッセルのパラドックスの証明は直観的に有効であるため、古典論理から直観論理に移行しても役に立ちません。

指定の公理スキームのみを受け入れることが、公理的集合論の始まりでした。その後、他のほとんどのツェルメロ-フランケル公理​​（外延公理、正則性公理、選択公理を除く）は、内包公理スキームを指定の公理スキームに変更することで失われたものの一部を補うために必要になりました。これらの公理はそれぞれ、特定の集合が存在することを述べ、そのメンバーが満たすべき述語を与えることでその集合を定義します。つまり、内包公理スキームの特別なケースです。

また、 New Foundationsの層別式のみ(下記参照) や、正値集合論の正値式 (連言、選言、量化、原子式のみの式) のみなど、適用可能な式を制限することで、スキーマの矛盾を防ぐこともできます。ただし、正値式では通常、ほとんどの理論が表現できる特定の事柄を表現できません。たとえば、正値集合論には補集合や相対補集合はありません。

フォン・ノイマン・ベルネイス・ゲーデル集合論では、集合とクラスが区別される。クラス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 クワインが開拓した集合論へのNew Foundationsアプローチでは、与えられた述語に対する内包公理は無制限の形式をとりますが、スキーマで使用できる述語自体は制限されています。述語 ( CはCに含まれない) は禁止されています。これは、同じシンボルC がメンバーシップ シンボルの両側に (したがって、異なる「相対型」で) 出現するためです。したがって、ラッセルのパラドックスは回避されます。ただし、P ( C )を( C = C )とすると(これは許可されています)、すべての集合の集合を形成できます。詳細については、階層化を参照してください。