構成的集合論

With computably undecidable propositions already arising in Robinson arithmetic, even just Predicative separation lets one define elusive subsets easily. In stark contrast to the classical framework, constructive set theories may be closed under the rule that any property that is decidable for all sets is already equivalent to one of the two trivial ones, ${\displaystyle \top }$ or ${\displaystyle \bot }$. Also the real line may be taken to be indecomposable in this sense. Undecidability of disjunctions also affects the claims about total orders such as that of all ordinal numbers, expressed by the provability and rejection of the clauses in the order defining disjunction ${\displaystyle (\alpha \in \beta )\lor (\alpha =\beta )\lor (\beta \in \alpha )}$. This determines whether the relation is trichotomous. A weakened theory of ordinals in turn affects the proof theoretic strength defined in ordinal analysis.

In exchange, constructive set theories can exhibit attractive disjunction and existence properties, as is familiar from the study of constructive arithmetic theories. These are features of a fixed theory which metalogically relate judgements of propositions provable in the theory. Particularly well-studied are those such features that can be expressed in Heyting arithmetic, with quantifiers over numbers and which can often be realized by numbers, as formalized in proof theory. In particular, those are the numerical existence property and the closely related disjunctive property, as well as being closed under Church's rule, witnessing any given function to be computable.^[2]

A set theory does not only express theorems about numbers, and so one may consider a more general so-called strong existence property that is harder to come by, as will be discussed. A theory has this property if the following can be established: For any property ${\displaystyle \phi }$, if the theory proves that a set exist that has that property, i.e. if the theory claims the existence statement, then there is also a property ${\displaystyle \psi }$ that uniquely describes such a set instance. More formally, for any predicate ${\displaystyle \phi }$ there is a predicate ${\displaystyle \psi }$ so that

$\displaystyle {\mathsf {T}}\vdash \exists x.\phi (x)\implies {\mathsf {T}}\vdash \exists !x.\phi (x)\land \psi (x)}$

The role analogous to that of realized numbers in arithmetic is played here by defined sets proven to exist by (or according to) the theory. Questions concerning the axiomatic set theory's strength and its relation to term construction are subtle. While many theories discussed tend have all the various numerical properties, the existence property can easily be spoiled, as will be discussed. Weaker forms of existence properties have been formulated.

存在の古典的な解釈を持ついくつかの理論は、実際には強い存在特性を示すように制約することもできます。すべての集合が順序定義可能であると仮定したツェルメロ・フレンケル集合論では、次のように表される理論があります。${\displaystyle {\mathsf {ZF}}+({\mathrm {V} }={\mathrm {HOD} })}$定義可能性を持たない集合は存在しない。この性質は、構成可能宇宙公準によっても強制される。${\displaystyle {\mathsf {ZF}}+({\mathrm {V} }={\mathrm {L} })}$対照的に、理論を考えてみよう${\displaystyle {\mathsf {ZFC}}}$によって与えられた${\displaystyle {\mathsf {ZF}}}$さらに、選択存在公理の完全な公理：この公理の集合は整列定理を証明し、任意の集合に対して整列が存在することを意味していることを思い出してください。特に、これは関係が$\displaystyle W\subset {\mathbb {R} }\times {\mathbb {R} }}$正式には、整列を確立するものが存在する${\displaystyle {\mathbb {R} }}$（つまり、この理論は、すべての部分集合に対して最小の要素が存在すると主張している。${\displaystyle {\mathbb {R} }}$（これらの関係に関して）このような順序の定義可能性は、${\displaystyle {\mathsf {ZFC}}}$後者は、特定の公式が存在しないことを意味する。${\displaystyle \psi }$理論の言葉で言えば、その理論は対応する集合が実数の整列関係であることを証明しているのだろうか。${\displaystyle {\mathsf {ZFC}}}$部分集合の存在を形式的に証明する$\displaystyle W\subset {\mathbb {R} }\times {\mathbb {R} }}$整列関係という性質を持ちながら、同時に特定の集合を持たない${\displaystyle W}$検証可能なプロパティを定義することができる可能性がある。

前述のように、構成理論${\displaystyle {\mathsf {T}}}$数値存在特性を示す可能性があり、$\displaystyle {\mathsf {T}}\vdash \exists e.\psi (e)\implies {\mathsf {T}}\vdash \psi ({\underline {\mathrm {e} }})}$ある数に対して${\displaystyle {\mathrm {e} }}$そしてどこで${\displaystyle {\underline {\mathrm {e} }}}$は形式理論における対応する数字を表す。ここでは、2 つの命題間の証明可能な含意を注意深く区別する必要がある。${\displaystyle {\mathsf {T}}\vdash P\to Q}$、そして理論の形式の性質${\displaystyle {\mathsf {T}}\vdash P\implies {\mathsf {T}}\vdash Q}$メタ論理的に確立された後者のタイプの図式を証明計算の推論規則として採用し、何も新しいことが証明できない場合、その理論は${\displaystyle {\mathsf {T}}}$その規則に基づき閉鎖される。

代わりに、メタ理論的性質に対応する規則を含意（「${\displaystyle \to }$"） に${\displaystyle {\mathsf {T}}}$公理図式として、または量化形式で表現される。よく研究される状況は、固定された${\displaystyle {\mathsf {T}}}$次のタイプのメタ理論的特性を示す：特定の形式の数式の集合からのインスタンスについては、ここでは次のように捉えられる。${\displaystyle \phi }$そして${\displaystyle \psi }$1つは数の存在を確立した${\displaystyle {\mathrm {e} }}$となることによって$\displaystyle {\mathsf {T}}\vdash \phi \implies {\mathsf {T}}\vdash \psi ({\underline {\mathrm {e} }})}$ここで、次のように仮定することができる。$\displaystyle \phi \to \exists (e\in {\mathbb {N} }).\psi (e)$境界が${\displaystyle e}$は理論の言語では数値変数である。例えば、チャーチの規則は一階ハイティング算術における許容規則である。${\displaystyle {\mathsf {HA}}}$さらに、対応する教会のテーゼ原則${\displaystyle {\mathrm {CT} }_{0}}$は一貫して公理として採用される可能性がある。この原理が追加された新しい理論は反古典的であり、 も採用することがもはや一貫していない可能性がある。${\displaystyle {\mathrm {PEM} }}$同様に、排中律に隣接して${\displaystyle {\mathrm {PEM} }}$ある理論によれば${\displaystyle {\mathsf {T}}}$このように得られた理論は、厳密に古典的な新しい命題を証明する可能性があり、これは、以前に確立されたメタ理論的性質の一部を損なう可能性があります。${\displaystyle {\mathsf {T}}}$そういうわけで、${\displaystyle {\mathrm {CT} }_{0}}$採用されない可能性がある${\displaystyle {\mathsf {HA}}+{\mathrm {PEM} }}$ペアノ算術としても知られる${\displaystyle {\mathsf {PA}}}$。

この小節では、後述するように、完全に形式的な無限列空間、すなわち関数空間上の量化を伴う集合論に焦点を当てる。チャーチの規則を理論自体の言葉で翻訳すると、次のようになる。

$\displaystyle \forall (f\in {\mathbb {N} }^{\mathbb {N} }).\exists (e\in {\mathbb {N} }).{\Big (}\forall (n\in {\mathbb {N} }).\exists (w\in {\mathbb {N} }).T(e,n,w)\land U(w,f(n)){\Big )}}$

クリーネのT述語と結果抽出を組み合わせると、任意の入力数値が${\displaystyle n}$番号にマッピングされる${\displaystyle f(n)}$は、${\displaystyle w}$計算可能なマッピングであることが確認されている。${\displaystyle {\mathbb {N} }}$は標準自然数の集合論モデルを表し、${\displaystyle e}$は、固定されたプログラム列挙に関するインデックスです。この原理を関数に拡張した、より強力なバリアントも使用されています。${\displaystyle f\in {\mathbb {N} }^{X}}$ドメイン上で定義される${\displaystyle X\subset {\mathbb {N} }}$低複雑性。この原理は述語の決定可能性を否定する。${\displaystyle Q(e)}$定義される${\displaystyle \exists (w\in {\mathbb {N} }).T(e,e,w)}$次のように表現する${\displaystyle e}$これは、計算可能な関数のインデックスが自身のインデックスで停止することである。この原理のより弱い、二重否定形式も考慮することができ、すべてのに対して再帰的な実装の存在を必要としない。${\displaystyle f}$しかし、再帰的実現を持たないことが証明されている関数の存在を主張する原理は依然として矛盾している。チャーチのテーゼの原理のいくつかの形式は、古典的な弱いいわゆる2階算術理論とも矛盾しない。${\displaystyle {\mathsf {RCA}}_{0}}$2ソート1階理論のサブシステム${\displaystyle {\mathsf {Z}}_{2}}$。

計算可能な関数の集合は古典的には部分可算であり、これは古典的には可算であることと同じである。しかし、古典的な集合論では一般的に、${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$計算可能な関数以外の関数も保持する。例えば、証明は次のとおりである。${\displaystyle {\mathsf {ZF}}}$チューリングマシンでは捉えられない全関数（集合論的な意味で）が存在する。計算可能な世界を存在論として真剣に捉えると、マルコフ学派に関連する反古典的概念の代表的な例は、さまざまな非可算集合の許容部分可算性である。すべての無限自然数列の集合の部分可算性を採用すると（${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$構成理論において、この集合の「小ささ」（古典的な意味での）は、いくつかの集合論的実現において、すでに理論自体によって捉えられている。構成理論は、古典的公理も反古典的公理も採用せず、どちらの可能性に対しても中立的な立場をとることもできる。

建設的な原則はすでに証明している$\displaystyle \forall (x\in X).\neg \neg {\big (}Q(x)\lor \neg Q(x){\big )}}$いかなる場合でも${\displaystyle Q}$。したがって、任意の要素について${\displaystyle x}$の${\displaystyle X}$、命題に対応する排中文は否定できない。実際、任意の与えられた命題に対して${\displaystyle x}$矛盾しないので、${\displaystyle Q(x)}$そして、その否定を同時に排除すれば、上記のように関連するド・モルガンの法則が適用される。しかし、理論によっては、拒否の主張も許容される場合がある。$\displaystyle \neg \forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )}}$これを採用しても、特定のものを提供する必要はありません${\displaystyle t\in X}$特定の命題に対する排中律の失敗を目撃する${\displaystyle Q(t)}$つまり、矛盾を目撃する${\displaystyle \neg {\big (}Q(t)\lor \neg Q(t){\big )}}$述語${\displaystyle Q(x)}$無限領域上${\displaystyle X}$決定問題に対応する。計算不可能であることが証明されている問題に触発されて、述語の決定可能性を否定しても、存在の主張はしない。${\displaystyle X}$別の例として、このような状況はブロウワーの直観主義分析で強制され、量化子が無限に続く二進数列を範囲とする場合、${\displaystyle Q(x)}$シーケンスは${\displaystyle x}$はどこでもゼロである。この性質、すなわち、永遠に一定の数列として決定的に識別されるという性質に関して、ブロウワーの連続性原理を採用すると、これがすべての数列に対して決定可能であることが厳密に否定される。

したがって、ここで用いられているような、いわゆる非古典論理を用いた構成的な文脈においては、排中律の量化された形式と矛盾する公理を一貫して採用することが可能であり、また、計算可能な意味でも、あるいは先に述べたメタ論理的な存在特性によって測られる意味でも、非構成的な公理を採用することも可能となる。このようにして、構成的な集合論は、例えば滑らかな無限小解析をモデル化した環など、非古典理論を研究するための枠組みを提供することもできる。

構成的集合論で研究されている多くの理論は、ツェルメロ・フレンケル集合論の単なる制限である（${\displaystyle {\mathsf {ZF}}}$）その公理と基礎となる論理に関して。このような理論は、あらゆるモデルで解釈することもできます。${\displaystyle {\mathsf {ZF}}}$。

算術を集合論の言語で理論と比較すると、古典的なペアノ算術は${\displaystyle {\mathsf {PA}}}$は、以下の理論と双方向的に解釈可能である。${\displaystyle {\mathsf {ZF}}}$マイナス無限と無限集合なし、さらにすべての推移閉包の存在。（後者は、後述する集合帰納図式に正則性を昇格させた後にも暗黙のうちに導かれる。）同様に、構成的算術は、で採用されたほとんどの公理に対する弁明としても捉えることができる。${\displaystyle {\mathsf {CZF}}}$:ヘイティング算術${\displaystyle {\mathsf {HA}}}$弱い構成的集合論と双方向的に解釈可能である^{[ 8 ] [ 9 ]。}これは、記事でも説明されている。${\displaystyle {\mathsf {HA}}}$メンバーシップ関係を算術的に特徴づけることができる。${\displaystyle \in }$そして、自然数の集合の存在の代わりに、それを証明する。${\displaystyle \omega }$- その理論におけるすべての集合は、(有限)フォン・ノイマン自然数と一対一である、という原理。${\displaystyle {\mathrm {V} }={\mathrm {Fin} }}$この文脈は、外延性、ペアリング、和集合、二項交差（述語的分離の公理図式に関連する）および集合帰納図式をさらに正当化する。公理として捉えると、前述の原理は、すでに与えられた理論と同一である集合論を構成する。${\displaystyle {\mathsf {CZF}}}$存在を除けば${\displaystyle \omega }$しかしプラス${\displaystyle {\mathrm {V} }={\mathrm {Fin} }}$公理として。これらの公理はすべて以下で詳しく説明します。関連して、${\displaystyle {\mathsf {CZF}}}$また、遺伝的に有限な集合がこれまでのすべての公理を満たすことも証明される。これは、次の段階に進む際にも成り立つ結果である。${\displaystyle {\mathsf {PA}}}$そして${\displaystyle {\mathsf {ZF}}}$マイナス無限大。反対側では、${\displaystyle {\mathsf {CZF}}}$プラス完全分離は、古典的な2階算術よりも強力ではありません。

構成的実現に関しては、関連する実現可能性理論が存在する。関連して、アツェルの構成的ツェルメロ＝フレンケル理論がある。${\displaystyle {\mathsf {CZF}}}$は、マルティン＝レーフ型の理論で解釈されてきた。${\displaystyle {\mathsf {CZF}}}$このように、この集合論およびより弱い集合論で証明可能な定理は、コンピュータによる実現の候補となる。

構成的集合論のプレシーフモデルも導入されている。これらは、1980年代にダナ・スコットによって開発された直観主義的集合論のプレシーフモデルに類似している。 ^{[ 10 ] [ 11 ]}実現可能性モデル${\displaystyle {\mathsf {CZF}}}$有効なトポス内では、例えば、完全な分離、相対化された依存的選択を同時に検証するものが特定されている。${\displaystyle {\mathrm {RDC} }}$前提の独立性${\displaystyle {\mathrm {IP} }}$集合だけでなく、すべての集合の可算性、マルコフの原理${\displaystyle {\mathrm {MP} }}$そしてチャーチの論文${\displaystyle {\mathrm {CT} _{0}}}$すべての述語の定式化において。^{[ 12 ]}

構文式を形成するために使用される命題結合記号は標準的である。集合論の公理は等号を証明する手段を提供する。${\displaystyle =}$「集合の」であり、その記号は表記の濫用によりクラスにも使用されることがある。等号述語が決定可能な集合は離散的とも呼ばれる。否定「${\displaystyle \neg }$「平等の否定」は、平等の否定とも呼ばれ、一般的には次のように書かれます。${\displaystyle \neq }$しかし、例えばシーケンスを扱う場合など、分離関係の文脈では、後者の記号は別の意味で使用されることもあります。

ここでも採用されている一般的な処理では、形式的には基礎となる論理を集合論の1つの原始的な二項述語で拡張するだけです。${\displaystyle \in }$「平等と同様に、要素性の否定」${\displaystyle \in }$「はよく書かれる」${\displaystyle \notin }$「。

ギリシャ語${\displaystyle \phi }$は公理図式における命題または述語変数を表し、${\displaystyle P}$または${\displaystyle Q}$は、特定の述語に使用されます。「述語」という単語は、単項の場合でも、「式」と互換的に使用されることがあります。

量化子は常に集合のみを対象とし、それらは小文字で表されます。一般的なように、構文表現における特定の自由変数を強調するために、引数括弧を使用して述語を表現することができます。例:${\displaystyle Q(z)}$「. 唯一無二の存在${\displaystyle \exists !x.Q(x)}$ここでの意味は${\displaystyle \exists x.\forall y.{\big (}y=x\leftrightarrow Q(y){\big )}}$。

また、よくあることですが、クラスにはセットビルダー記法が用いられます。クラスはほとんどの場合、オブジェクト言語の一部ではありませんが、簡潔な議論のために使用されます。特に、対応するクラスの記法宣言は「${\displaystyle A=\{z\mid Q(z)\}}$、いかなる表現の目的でも${\displaystyle Q(a)}$として${\displaystyle a\in A}$論理的に同等の述語は、同じクラスを導入するために使用できます。また、次のように記述することもできます。${\displaystyle \{z\in B\mid Q(z)\}}$略語として${\displaystyle \{z\mid z\in B\land Q(z)\}}$例えば、${\displaystyle \{z\in B\mid z\notin C\}}$また、これは次のように表記されます。${\displaystyle B\setminus C}$。

略す${\displaystyle \forall z.{\big (}z\in A\to Q(z){\big )}}$による${\displaystyle \forall (z\in A).Q(z)}$そして${\displaystyle \exists z.{\big (}z\in A\land Q(z){\big )}}$による${\displaystyle \exists (z\in A).Q(z)}$この意味での限定量化の構文概念は、以下の公理の議論で見られるように、公理スキーマの定式化において役割を果たすことができる。サブクラスの主張を表現する。${\displaystyle \forall (z\in A).z\in B}$つまり${\displaystyle \forall z.(z\in A\to z\in B)}$、 による${\displaystyle A\subset B}$述語の場合${\displaystyle Q}$ごく当たり前に${\displaystyle \forall z.{\big (}(z\in B\land Q(z))\to z\in B{\big )}}$そして、次のことが続く。${\displaystyle \{z\in B\mid Q(z)\}\subset B}$部分集合で制限された量化子の概念、例えば${\displaystyle \forall (z\subset A).z\in B}$は集合論的な研究にも用いられてきたが、ここではそれ以上詳しく述べることはしない。

クラス内に集合が存在することが証明されている場合、つまり${\displaystyle \exists z.(z\in A)}$すると、そこは居住地と呼ばれる。また、量化は${\displaystyle A}$これを表現するために${\displaystyle \exists (z\in A).(z=z)}$授業${\displaystyle A}$は、後述するように、空集合ではないことが証明されます。古典的には同値ですが、構成的に空でないという概念は、2つの否定を含むより弱い概念であり、「居住されていない」とは言い換えるべきでしょう。残念ながら、より有用な「居住されている」という概念を表す言葉は、古典数学ではほとんど使われていません。

クラスが互いに排他的であることを表現する2つの方法は、直観的に妥当な否定規則の多くを捉えている。${\displaystyle {\big (}\forall (x\in A).x\notin B{\big )}\leftrightarrow \neg \exists (x\in A).x\in B}$上記の表記法を用いると、これは純粋に論理的な同値関係であり、この記事ではさらに、命題は次のように表現できる。${\displaystyle A\cap B=\{\}}$。

サブクラス${\displaystyle A\subset B}$は取り外し可能と呼ばれます${\displaystyle B}$相対化されたメンバーシップ述語が決定可能であれば、つまり${\displaystyle \forall (x\in B).x\in A\lor x\notin A}$成り立つ。また、文脈から上位クラスが明確な場合、決定可能とも呼ばれる。多くの場合、上位クラスは自然数の集合である。

で表す${\displaystyle A\simeq B}$2 つのクラスがまったく同じ要素を持っていることを表す記述、つまり${\displaystyle \forall z.(z\in A\leftrightarrow z\in B)}$または同等に${\displaystyle (A\subset B)\land (B\subset A)}$これは、後述する等価性の概念と混同してはならない。

と${\displaystyle A}$の${\displaystyle \{z\mid Q(z)\}}$、便利な表記関係${\displaystyle x\in A}$そして${\displaystyle Q(x)}$、次の形式の公理${\displaystyle \exists a.\forall z.{\big (}z\in a\leftrightarrow Q(z){\big )}}$すべての集合のクラスを仮定すると、${\displaystyle Q}$は実際に集合を形成する。より非公式には、これは次のように表現できる。${\displaystyle \exists a.a\simeq A}$同様に、命題${\displaystyle \forall a.(a\simeq A)\to P(a)}$伝える「${\displaystyle P(A)}$いつ${\displaystyle A}$は理論の集合の中に含まれています。${\displaystyle P}$は自明に偽の述語であり、命題は前の存在主張の否定と同等であり、 の非存在を表している。${\displaystyle A}$セットとして。

上記のようなクラス内包表記のさらなる拡張は集合論でよく使われ、次のような文に意味を与えます。${\displaystyle \{f(z)\mid Q(z)\}\simeq \{\langle x,y,z\rangle \mid T(x,y,z)\}}$"、 等々。

構文的にはより一般的に、セット${\displaystyle w}$別の2項述語を用いて特徴付けることもできる。${\displaystyle R}$トラフ${\displaystyle \forall x.x\in w\leftrightarrow R(x,w)}$右辺は実際の変数に依存する可能性がある${\displaystyle w}$会員資格についても${\displaystyle w}$自体。

この公理はしばしば採用されるものの、構成主義的な思考においては批判されてきた。なぜなら、それは異なる定義を持つ性質、あるいは少なくともそれらの性質の拡張とみなされる集合を事実上同一視してしまうからである。これはフレーギアン的な概念である。

現代の型理論は、代わりに要求された等価性を定義することを目指しているかもしれない。${\displaystyle \simeq }$関数の観点から言えば、例えば型等価性を参照のこと。関連する関数外延性の概念は、型理論ではしばしば採用されない。

構成的数学の他の枠組みでは、要素に対して等号や分離に関する特定の規則を要求するかもしれない。${\displaystyle z\in x}$各セットのそれぞれ${\displaystyle x}$議論された。しかし、分離性を強調する集合へのアプローチでは、部分集合に関する上記の定義を等価性の概念を特徴付けるために使用できる。${\displaystyle \simeq }$これらの部分集合のうちの。関連して、2 つの部分集合の補集合という大まかな概念${\displaystyle u\subset x}$そして${\displaystyle v\subset x}$2 人のメンバーが${\displaystyle s\in u}$そして${\displaystyle t\in v}$互いに明らかに異なる。補完的なペアの集合${\displaystyle \langle u,v\rangle }$代数的に良好な性質を持つ。

書く${\displaystyle 1}$のために${\displaystyle S0}$これは、${\displaystyle \{\{\}\}}$つまり${\displaystyle \{0\}}$同様に、${\displaystyle 2}$のために${\displaystyle S1}$これは、${\displaystyle \{\{\},\{\{\}\}\}}$つまり${\displaystyle \{0,1\}}$例えば、単純で明らかに誤りである命題は次のようになる。${\displaystyle \{\}\in \{\}}$、対応する${\displaystyle 0<0}$標準算術モデルでは、ここでも次のような記号が使われます。${\displaystyle \{\}}$これらは便利な表記法として扱われ、実際にはどの命題も「」のみを使用した式に変換されます。${\displaystyle \in }$「そして量化子を含む論理記号。新しい理論の能力が実質的に同等であるというメタ数学的分析を伴い、次のような記号による形式的拡張、${\displaystyle 0}$も考慮される可能性がある。

より一般的には、集合に対して${\displaystyle x}$後継セットを定義する${\displaystyle Sx}$として${\displaystyle x\cup \{x\}}$後継操作とメンバーシップ関係の相互作用には、次のような意味で再帰的な節がある。${\displaystyle (y\in Sx)\leftrightarrow (y\in x\lor y=x)}$等号の反射性により、${\displaystyle x\in Sx}$、特に${\displaystyle Sx}$常に人が住んでいる。

基本的な構成的集合論${\displaystyle {\mathsf {BCST}}}$標準的な集合論に含まれるいくつかの公理から構成されるが、いわゆる「完全な」分離公理は弱められている。上記の4つの公理に加えて、述語的分離と置換スキーマも仮定する。

この公理は集合の存在を仮定することに相当する${\displaystyle s}$任意の集合の交差によって得られる${\displaystyle y}$述語的に記述されたクラス${\displaystyle \{x\mid \phi (x)\}}$どのような場合でも${\displaystyle z}$述語が次のように解釈されると、集合であることが証明される。${\displaystyle \phi (x):=x\in z}$集合の二項交差が得られ、次のように記述される。${\displaystyle s=y\cap z}$交差は論理積に対応するが、これは和集合が論理和に対応するのと同様の関係にある。

述語が否定として扱われる場合${\displaystyle \phi (x):=x\notin z}$すると、任意の集合の存在を仮定した差分原理が得られる。${\displaystyle y\setminus z}$.次のようなセットに注意してください${\displaystyle y\setminus y}$または${\displaystyle \{x\in y\mid \neg (x=x)\}}$空集合は常に空である。したがって、前述のように、分離と少なくとも1つの集合（例えば、下記の無限集合）の存在から、空集合の存在が導かれる。${\displaystyle \{\}}$（また表記される）${\displaystyle 0}$この保守的な文脈の中で${\displaystyle {\mathsf {BCST}}}$述語的分離スキーマは、実際には空集合と任意の2つの集合の二項交差の存在と同等である。後者の公理化のバリアントは、式スキーマを使用しない。

述語分離は、証明可能な同値性まで集合定義述語の構文的側面を考慮に入れるスキーマである。許容される式は、で表される。${\displaystyle \Delta _{0}}$集合論的レヴィ階層の最下位レベル。^{[ 13 ]} 集合論における一般述語は、このような構文上の制限を受けることは決してないため、実際には、集合の一般的なサブクラスは依然として数学言語の一部である。証明可能な集合であるサブクラスのスコープは、既に存在する集合に依存するため、さらに集合の存在公理が追加されると、このスコープは拡張される。

要素が最大で1つしかないクラスは、サブシングルトンと呼ばれます。命題の場合${\displaystyle P}$集合論の構成的分析における繰り返し登場する比喩は、述語を${\displaystyle x=0\land P}$サブシングルトンとして${\displaystyle B:=\{x\in 1\mid P\}}$これは第2序数のサブクラスです${\displaystyle 1:=S0=\{0\}}$もしそれが証明できるならば${\displaystyle P}$保持する、または${\displaystyle \neg P}$、 または${\displaystyle \neg \neg P}$、 それから${\displaystyle B}$それぞれ、居住されている、空いている（無人）、または空いていない（無人ではない）です。明らかに、${\displaystyle P}$は、命題と同等である。${\displaystyle 0\in B}$、また${\displaystyle B=1}$。 同じく、${\displaystyle \neg P}$と同等${\displaystyle B=0}$そして同様に、${\displaystyle \neg (0\in B)}$ということで、ここで、${\displaystyle B}$取り外し可能である${\displaystyle 1}$正確には${\displaystyle P\lor \neg P}$自然のモデルでは、${\displaystyle B}$は数字です。${\displaystyle 0\in B}$また、${\displaystyle 0}$より小さい${\displaystyle B}$上記の後継演算定義の一部である共用体は、除外中間文を次のように表現するために使用できます。${\displaystyle 0\in SB}$言葉で言うと、${\displaystyle P}$は、後継者が${\displaystyle B}$最小の序数よりも大きい${\displaystyle 0}$提案 ${\displaystyle P}$どちらにしても、どのように決定するかは${\displaystyle 0}$小さいです:${\displaystyle 0}$すでに小さい${\displaystyle B}$または${\displaystyle 0}$いる${\displaystyle SB}$の直接の前身。 の排中を表す別の方法${\displaystyle P}$居住クラスの最小メンバーの存在${\displaystyle b:=B\cup \{1\}}$。

分離公理が分離を許容する場合${\displaystyle P}$、 それから${\displaystyle B}$は部分集合であり、に関連付けられた真理値と呼ばれることがあります。${\displaystyle P}$2 つの真理値は、集合として、同値性を証明することによって等しいと証明できます。この用語で言えば、証明値の集合は先験的に豊富であると理解できます。当然のことながら、決定可能な命題は、2 つの真理値の集合のいずれかを持ちます。そのための排中論理和は、${\displaystyle P}$グローバルステートメントによっても暗示される${\displaystyle \forall b.(0\in b)\lor (0\notin b)}$。

非公式なクラス用語を使用する場合、任意の集合もクラスとみなされます。同時に、集合として拡張できないいわゆる真のクラスも発生します。理論において証明がある場合、${\displaystyle \neg \exists x.A\subset x}$、 それから${\displaystyle A}$適切でなければならない。（${\displaystyle {\mathsf {ZF}}}$集合論において、完全分離理論では、真クラスは一般的に、集合としては「大きすぎる」ものと考えられています。より厳密に言えば、それらは累積階層のサブクラスであり、あらゆる順序境界を超えて広がっています。

集合のマージに関するセクションの注釈により、集合は、次の形式のクラスのメンバーであることを一貫して排除することはできません。${\displaystyle A\cup \{x\mid x\notin A\}}$そのクラスに属するという構成的証明には情報が含まれています。${\displaystyle A}$セットである場合、クラス${\displaystyle \{x\mid x\notin A\}}$これは証明可能な正当性を持つ。以下は、次の特殊なケースでこれを証明する。${\displaystyle A}$右辺が普遍クラスである場合、空になります。結果が否定的であるため、古典理論と同じように解釈されます。

以下のことは、あらゆる関係に当てはまります。${\displaystyle E}$2 つの項が純粋に論理的な条件を与える。${\displaystyle s}$そして${\displaystyle y}$できない${\displaystyle E}$互いに関連している。

${\displaystyle {\big (}\forall x.xEs\leftrightarrow (xEy\land \neg xEx){\big )}\to \neg (yEs\lor sEs\lor sEy)}$

ここで最も重要なのは、最後の選言子の拒否である。${\displaystyle \neg sEy}$表現${\displaystyle \neg (x\in x)}$これは無制限の量化を伴わないため、分離において許容される。ラッセルの構成は、${\displaystyle \{x\in y\mid x\notin x\}\notin y}$。したがって、任意の集合に対して${\displaystyle y}$述語的分離のみでは、 の要素ではない集合が存在することを意味する。${\displaystyle y}$特に、この理論においては普遍集合は存在し得ない。

規則性の公理をさらに採用した理論では、${\displaystyle {\mathsf {ZF}}}$証明済み${\displaystyle x\in x}$任意の集合に対して偽である${\displaystyle x}$つまり、部分集合は${\displaystyle \{x\in y\mid x\notin x\}}$に等しい${\displaystyle y}$それ自体、そしてクラス${\displaystyle \{x\mid x\in x\}}$は空集合です。

いかなる場合でも${\displaystyle E}$そして${\displaystyle y}$特別なケース${\displaystyle s=y}$上記の式では

${\displaystyle \neg {\big (}\forall x.xEy\leftrightarrow \neg xEx{\big )}}$

これはすでに、どの集合も${\displaystyle y}$サブクラスと等しい${\displaystyle \{x\mid x\notin x\}}$普遍クラスの、つまりそのサブクラスも適切なものである。しかし、${\displaystyle {\mathsf {ZF}}}$規則性がない場合、それぞれが正確に自身を含むシングルトンの適切なクラスが存在することは矛盾しない。

余談だが、直観主義的新基礎論のような階層構造を持つ理論では、構文表現${\displaystyle x\in x}$分離理論では、これは認められない可能性がある。逆に、その理論では、普遍集合の存在を否定する上記の証明は実行できない。

述語分離の公理図式は、${\displaystyle \Delta _{0}}$-分離または有界分離、例えば集合有界量化子のみの分離。（注意：レヴィ階層の命名法は、${\displaystyle \Delta _{0}^{0}}$算術階層においては、比較は微妙な場合があるが、算術分類は構文的にではなく、自然数のサブクラスという観点から表現されることもある。また、算術階層の最下層にはいくつかの共通定義があり、その中には全関数の一部の使用を許容しないものもある。同様の区別は、次のレベルでは関係ない。${\displaystyle \Sigma _{1}^{0}}$またはそれ以上。最後に、${\displaystyle \Delta _{0}}$理論上、式の分類は等価性まで表現できる。

この図式は、マック・レーンがツェルメロ集合論に近いシステムを弱体化させる方法でもある。${\displaystyle {\mathsf {Z}}}$トポス理論に関連する数学的基礎のために用いられる。また、絶対性の研究にも用いられ、クリプキ＝プラテック集合論の定式化の一部となっている。

公理の制約は、非述語的定義のゲートキーピングにもなります。明示的に記述できないオブジェクト、または定義が自身や適切なクラスへの参照を含むオブジェクト（チェック対象の性質が全称量化子を含む場合など）については、存在を主張すべきではありません。したがって、冪集合公理のない構成理論では、${\displaystyle R}$2項述語を表す場合、一般的にはサブクラスを期待すべきではない。${\displaystyle s}$の${\displaystyle y}$定義される場合、集合となる。例えば、

${\displaystyle \{x\in y\mid \forall t.{\big (}(t\subset y)\to R(x,t){\big )}\}}$、

または、集合上の任意の量化を含む同様の定義を介して${\displaystyle t\subset y}$. このサブクラスの場合、${\displaystyle s}$の${\displaystyle y}$が集合であることが証明された場合、この部分集合自体も集合変数の無制限スコープに含まれる。${\displaystyle t}$言い換えれば、サブクラスのプロパティとして${\displaystyle s\subset y}$満たされる、この正確なセット${\displaystyle s}$式を使用して定義されます${\displaystyle R(x,s)}$それは、それ自体の特徴づけにおいて役割を果たすだろう。

述語的分離によって与えられたクラス定義のうち集合となるものは少なくなるが、古典的には等価な多くのクラス定義が、より弱い論理に限定すると等価ではなくなることを強調しておく必要がある。一般述語の潜在的な不確定性のため、部分集合と部分クラスの概念は、構成的集合論では古典的な集合論よりも必然的に複雑になる。このようにして、より広範な理論が得られる。これは、理論のように完全な分離を採用した場合でも変わらない。${\displaystyle {\mathsf {IZF}}}$しかしながら、これは存在特性と標準的な型理論の解釈を損ない、構成的集合のボトムアップ的な見方を損なうことになる。余談だが、サブタイピングは構成的型理論の必須機能ではないため、構成的集合理論はその枠組みとはかなり異なると言える。

次に、

これは、定義域を通じて得られる関数のような述語の範囲を、集合として存在させるものです。上記の定式化では、述語は分離スキーマのように制限されていませんが、この公理は既に前件に存在量化子を含んでいます。もちろん、より弱いスキーマも考慮することができます。

置換により、任意のペアの存在${\displaystyle \{x,y\}}$また、他の特定のペアからも同様の結果が得られます。${\displaystyle \{0,1\}=2=SS0}$しかし、バイナリユニオンは、${\displaystyle S}$すでにペアリング公理を利用しているこのアプローチでは、次の存在を仮定する必要がある。${\displaystyle 2}$のそれよりも${\displaystyle 0}$非述語的冪集合公理を持つ理論では、${\displaystyle 2\subset {\mathcal {P}}{\mathcal {P}}0}$分離を用いて実証することもできる。

置換スキームを用いると、これまで概説した理論は、同値類または添え字付き和が集合であることを証明します。特に、 2つの集合のすべての要素のペアを保持するデカルト積は集合です。さらに、任意の固定数（メタ理論において）に対して、対応する積の式、例えば${\displaystyle x\times x\times x\times x}$は集合として構成できます。言語内で再帰的に定義された集合の公理的要件については、以下でさらに詳しく説明します。集合${\displaystyle x}$離散的である、つまり集合内の要素の等価性${\displaystyle x}$対応する関係が部分集合として決定可能である場合${\displaystyle x\times x}$決定可能である。

置換は関数理解に関連しており、より一般的には理解の一形態と見なすことができます。${\displaystyle {\mathrm {PEM} }}$置換はすでに完全な分離を意味するのでしょうか。${\displaystyle {\mathsf {ZF}}}$置換は主に高ランクの集合の存在を証明するために重要であり、具体的には公理スキーマのインスタンスを介して証明されます。${\displaystyle \phi (x,y)}$比較的小さなセットに関連する${\displaystyle x}$より大きなものへ、${\displaystyle y}$。

構成的集合論では、一般的に置換公理図式が用いられ、時には限定された論理式に限定される。しかし、他の公理が削除されると、この図式は実際には強化されることが多い。ただし、${\displaystyle {\mathsf {ZF}}}$しかし、そうではなく、単に証明可能性の強さを取り戻すためだけにそうしているわけではない。後述するように、理論の強い存在特性を損なわない、より強力な公理も存在する。

もし${\displaystyle i_{X}}$は、関数であることが証明されています。${\displaystyle X}$そしてそれは終域を備えている${\displaystyle Y}$（以下で詳しく説明します）次に、${\displaystyle i_{X}}$は、${\displaystyle Y}$集合概念に対する他のアプローチでは、部分集合の概念は次のように「演算」の観点から定義されます。

遺伝的に有限な集合のクラスの要素のペンダント${\displaystyle H_{\aleph _{0}}}$は、一般的なプログラミング言語であればどれでも実装できます。上記で説明した公理は、集合データ型に対する一般的な操作を抽象化したものです。ペアリングとユニオンは、ネストとフラット化、または連結に関連しています。置換は内包表記に関連しており、分離は、多くの場合より単純なフィルタリングに関連しています。置換と集合帰納法（後述）を組み合わせることで、公理化に十分です。${\displaystyle H_{\aleph _{0}}}$建設的に、そしてその理論は無限性なしでも研究されている。

ペアリングとユニオンの中間のようなもので、後継者により関連付けられやすい公理は随伴公理である。^{[ 14 ] [ 15 ]}このような原理は、個々のノイマン順序数の標準的なモデリングに関連している。ユニオンと置換を1つに組み合わせた公理の定式化も存在する。置換を仮定することは、ハイティング算術と双方向に解釈可能な弱い構成的集合論の設計において必須ではないが、${\displaystyle {\mathsf {HA}}}$何らかの帰納法が用いられている。比較のために、自然数のクラスとその算術を外延性、随伴性、完全分離のみによって解釈する一般集合論と呼ばれる非常に弱い古典理論を考えてみよう。

議論は、異なるが関連する形で依存型理論にも見られる対象の存在を規定する公理、すなわち積と完全集合としての自然数の集合について進む。無限集合は、非有界インデックス領域で定義された数列に適用される演算、例えば生成関数の形式微分や2つのコーシー数列の加算について推論する際に特に便利である。

動機付けが必要な場合、他の帰納的性質に関連して無限の数の集合を仮定することの便利さは、後述する集合論における算術の議論で明らかになります。しかし、古典的な集合論でおなじみのように、無限の弱い形式も定式化できます。たとえば、帰納的集合の存在を仮定するだけで、${\displaystyle \exists y.\mathrm {Ind} _{y}}$- 完全な分離が帰納的部分集合を切り出すのに使用できる場合、そのような存在公準で十分である${\displaystyle w}$自然数の集合、すなわちすべての帰納的クラスの共通部分集合。あるいは、より具体的な存在公理を採用することもできる。いずれにせよ、帰納的集合は以下を満たす。${\displaystyle \Delta _{0}}$フォン・ノイマンモデルの意味での先行存在特性：

${\displaystyle \forall m.(m\in w)\leftrightarrow {\big (}m=0\lor \exists (p\in w).Sp=m{\big )}}$

先に定義した後継記法の表記法を用いずに、後継者への外延的等価性${\displaystyle Sp=m}$捕獲される${\displaystyle \forall n.(n\in m)\leftrightarrow (n=p\lor n\in p)}$これは、すべての要素が${\displaystyle m}$等しいか${\displaystyle 0}$または、それ自体が先行セットを保持している${\displaystyle p\in w}$他のすべてのメンバーを共有する${\displaystyle m}$。

「${\displaystyle \exists (p\in w)}$右側には、特性として${\displaystyle w}$メンバーによって${\displaystyle m}$ここで構文的に再びシンボルが含まれています${\displaystyle w}$それ自体。自然数のボトムアップの性質により、ここではこれは穏やかです。${\displaystyle \Delta _{0}}$-誘導加熱器を上に置く${\displaystyle {\mathsf {ECST}}}$2つの異なる集合はこの性質を持ちません。また、この性質にはより長い定式化もあり、「${\displaystyle \exists (p\in w)}$「無制限の量化子を支持する。」

無限公理を採用すると、述語で使用される集合境界量化は${\displaystyle \Delta _{0}}$-分離により、数値的に無制限の量化子が明示的に許可されます - 「有界」の2つの意味を混同してはいけません。${\displaystyle \omega }$手元にある番号のクラスを呼び出す${\displaystyle I\subset \omega }$以下の存在条件が満たされる場合、有界である。

${\displaystyle \exists (m\in \omega ).\forall (n\in \omega ).(n\in I\to n<m)}$

これは有限性に関する記述であり、同様に次のように定式化される。${\displaystyle m\leq n\to n\notin I}$同様に、以下の関数の議論をより正確に反映するために、上記の条件を次の形式で考えてみましょう。${\displaystyle \exists (m\in \omega ).\forall (n\in I).(n<m)}$決定可能な性質については、これらは${\displaystyle \Sigma _{2}^{0}}$算術の命題だが、無限公理では、2 つの量化子は集合に束縛される。

授業のために${\displaystyle C}$論理的に肯定的な非有界性命題

${\displaystyle \forall (k\in \omega ).\exists (j\in \omega ).(k\leq j\land j\in C)}$

は今や無限の1つでもある。${\displaystyle \Pi _{2}^{0}}$決定可能な算術の場合。集合の無限性を検証するために、この性質は、集合が無限個の要素以外にも他の要素を持つ場合でも機能します。${\displaystyle \omega }$。

以下では、自然数の最初の部分、つまり${\displaystyle \{n\in \omega \mid n<m\}}$いかなる場合でも${\displaystyle m\in \omega }$空集合を含む集合は、で表されます。${\displaystyle \{0,1,\dots ,m-1\}}$このセットは${\displaystyle m}$そしてこの時点で「${\displaystyle m-1}$「」は、その前のもの（つまり、減算関数を含まないもの）の単なる表記です。

集合内包と外延性を持つ理論が、最終的に述語論理を符号化する仕組みを思い出すことは有益である。集合論におけるあらゆるクラスと同様に、集合は集合上の述語に対応するものとして解釈できる。例えば、整数が偶数であるとは、それが偶数の集合の要素である場合であり、自然数が後継数を持つとは、それが後継数を持つ自然数の集合の要素である場合である。より単純な例ではないが、ある集合を固定する。${\displaystyle y}$そして${\displaystyle Q(n)}$有限順序数上の関数空間が であることを示す存在命題を表す。${\displaystyle y}$存在する。述語は次のように表記される。${\displaystyle \exists h.h\simeq y^{\{0,1,\dots ,n-1\}}}$以下に示すように、存在量化子は自然数上の1だけではなく、他の集合によって制限されることもありません。${\displaystyle \forall (n\in \omega ).Q(n)}$そして、よりくだけた言い方をすれば、平等${\displaystyle \omega =\{n\in \omega \mid Q(n)\}}$これらは、同じ望ましい声明を定式化する2つの方法にすぎません。${\displaystyle n}$存在命題の添え字付き連言${\displaystyle n}$すべての自然数の集合を範囲とする。外延的同一視により、2 番目の形式はサブクラス内包表記を使用して主張を表現し、右辺の括弧で囲まれたオブジェクトは集合を構成しない可能性がある。そのサブクラスが証明可能な集合でない場合、それは実際には証明における多くの集合論の原理で使用されず、普遍閉包を確立する。${\displaystyle \forall (n\in \omega ).Q(n)}$定理が成り立たない場合もあるため、集合論は、述語的限定分離とともに使用される集合存在公理を増やすことによって強化できるが、より強い公理を仮定することによっても強化できる。${\displaystyle \forall }$-声明。

無限の強い公理における2番目の全称量化子は、すべての に対して数学的帰納法を表す。${\displaystyle y}$議論の宇宙、つまり集合の場合。これは、この節の帰結が、${\displaystyle \omega \subset y}$すべて${\displaystyle n\in \omega }$関連する述語を満たす。述語的分離を使用してサブセットを定義できる${\displaystyle \omega }$この理論は、すべての述語に対する帰納法を証明する。${\displaystyle \phi (n)}$集合境界量化子のみを含む。集合境界量化子のこの役割は、より多くの集合存在公理がこの帰納原理の強さに影響を与えることを意味し、記事の残りの部分で焦点となる関数空間と集合公理をさらに動機づける。特に、${\displaystyle {\mathsf {ECST}}}$すでに自然数上の量化子を用いた帰納法を検証しており、したがって一階算術理論における帰納法も検証している。${\displaystyle {\mathsf {HA}}}$集合論の言語で表現された任意の述語（つまりクラス）に対するいわゆる完全数学的帰納法の公理は、${\displaystyle {\mathsf {ECST}}}$前述の帰納法原理を直接採用すれば、2階算術により近いものとなる。集合論では、完全（つまり無制限）分離からも導かれる。完全（つまり無制限）分離とは、すべての述語が${\displaystyle \forall }$集合である。数学的帰納法は、（完全な）集合帰納法の公理によっても置き換えられる。