構成的集合論

公理的構成的集合論は、公理的集合論のプログラムに従う数学的構成主義へのアプローチです。通常、古典的集合論の「 」と「 」と同じ一階述語言語が使用されるため、構成的型アプローチと混同しないでください。一方、一部の構成的理論は、型 理論における解釈可能性によって動機付けられています${\displaystyle =}$ ${\displaystyle \in}$

排中律（ ）を否定することに加え、構成的集合論では、公理中の一部の論理量化子が有界集合であることを要求することが多い。後者は、予測不可能性と結びついた結果に基づく。 ${\displaystyle {\mathrm {PEM} }}$

はじめに

建設的な見通し

直観主義論理の使用に関する予備的考察

ここで説明する集合論の論理は、排中律、つまりすべての命題 に対して選言が自動的に成り立つという原理を拒否するという点で構成的です。 これは、それが前提とされている文脈では、排中律 ( ) とも呼ばれます。構成的には、原則として、命題 の排中律を証明する、つまり特定の選言 を証明するには、または を明示的に証明する必要があります。 どちらかの証明が確立されている場合、その命題は決定可能であるとされ、これは論理的に選言が成り立つことを意味します。 同様に、より一般的には、ドメイン内の の述語は、より複雑なステートメントが証明可能であるときに決定可能であると言われます。 非構成的公理は、選言のどちらの側の真偽も示さずに （それぞれ上記の量指定子を使用したステートメント） の排中律を証明するという意味で、そのような（および/または）の決定可能性を正式に主張する証明を可能にする場合があります。 これは古典論理ではよくあることです。対照的に、構成的であるとみなされる公理理論は、計算上決定不可能であることが証明されている特性を含むステートメントの多くの古典的な証明を許可しない傾向があります。 ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle \phi \lor \neg \phi }$ ${\displaystyle \phi}$ ${\displaystyle {\mathrm {LEM} }}$ ${\displaystyle P}$ ${\displaystyle P\lor \neg P}$ ${\displaystyle P}$ ${\displaystyle \neg P}$ ${\displaystyle Q(x)}$ ${\displaystyle x}$ ${\displaystyle X}$ ${\displaystyle \forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )}}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$

矛盾律は、前者の命題形式 の特殊なケースである。 前者を任意の否定ステートメント と共に使用すると、より保守的な最小限の論理において、有効なド・モルガンの法則が 1 つ存在することになる。 言葉で言えば、直観主義論理は依然として次のことを主張する。 命題を除外すると同時にその否定 も除外することは不可能であり、したがって、個々の命題について具体例を挙げた排中律のステートメントを拒絶することは矛盾している。 ここで、二重否定は、仮定された公理から選言が証明できない場合でも (たとえば、選言の 1 つを実証して を決定することによって)、選言ステートメントが除外または拒絶されることは決してないことが証明されている。 ${\displaystyle \neg P}$ ${\displaystyle \neg \neg (P\lor \neg P)}$ ${\displaystyle P}$

より一般的には、構成的数学理論は、古典的定理の古典的に同値な再定式化を証明する傾向がある。例えば、構成的解析においては、中間値定理を教科書的な定式のまま証明することはできないが、二重否定消去とその帰結が正当であると仮定すれば、アルゴリズム的な内容を持つ定理は、古典的命題と直ちに同値となることを証明することができる。違いは、構成的証明の方が見つけにくいということである。

ここで論じる集合論の根底にある直観主義論理は、最小論理とは異なり、排中律が成立する個々の命題に対しては依然として二重否定の消去を許容する。その結果、有限対象に関する定理の定式化は、古典的な定理と変わらない傾向がある。すべての自然数のモデルが与えられた場合、述語に対する同等の定理、すなわちマルコフ原理は自動的には成立しないが、追加の原理として考えることができる。 ${\displaystyle P}$

居住領域で爆発 を使用すると、この選言は存在主張 を意味し、それは を意味します。古典的には、これらの含意は常に可逆です。前者のいずれかが古典的に有効である場合、後者の形式でそれを確立してみる価値はあります。が拒否される特殊なケースでは、反例の存在主張 を扱います。これは一般に、拒否主張よりも構成的に強力です。が矛盾するようなを例示することは、もちろん、すべての可能な に当てはまるではないことを意味します。しかし、特定の反例の助けを借りずに、さらには反例を作成できない場合でも、すべて に当てはまると論理的に矛盾が生じることを示すこともできます。後者の場合、構成的には、ここでは存在主張を規定しません。 ${\displaystyle P\lor \exists (x\in X).\neg Q(x)}$ ${\displaystyle \exists (x\in X).(Q(x)\to P)}$ ${\displaystyle {\big (}\forall (x\in X).Q(x){\big )}\to P}$ ${\displaystyle P}$ ${\displaystyle \exists (x\in X).\neg Q(x)}$ ${\displaystyle \neg \forall (x\in X).Q(x)}$ ${\displaystyle t}$ ${\displaystyle Q(t)}$ ${\displaystyle Q}$ ${\displaystyle x}$ ${\displaystyle Q}$ ${\displaystyle x}$

集合論に課せられた制約

古典的な対応物と比較すると、実現できない関係の存在を証明する可能性は一般に低くなります。存在のアプリオリな構成的読み取りへの制限は、無制限のコレクションを含むセットのどの特徴付けが（数学的な、したがって常に完全な）関数を構成するかに関して、より厳しい要件につながります。これは多くの場合、ケースごとの定義になるはずの述語が決定可能でない可能性があるためです。外延性を介して集合の等価性の標準的な定義を採用すると、完全な選択公理は、ディアコネスクの定理によって、採用した分離スキーマで許可されている式に対してが成り立つような非構成的な原理です。以下に示すように、同様の結果は正則性公理の存在主張にも当てはまります。後者には、古典的に同等な帰納的代替があります。そのため、集合論の真に直観主義的な展開には、いくつかの標準的な公理を古典的に同等なものに言い換えることが必要です。計算可能性の要求や予測不可能性の留保とは別に、^{[ 1 ]}どの非論理的公理が理論の基礎となる論理を効果的に拡張するかという技術的な問題も、それ自体が研究課題である。 ${\displaystyle f\subset X\times Y}$ ${\displaystyle {\mathrm {PEM} }}$

メタロジック

ロビンソン算術ではすでに計算可能決定不可能な命題が生じているため、述語分離だけでも、とらえどころのない部分集合を簡単に定義できます。古典的なフレームワークとはまったく対照的に、構成的集合論は、すべての集合に対して決定可能な任意のプロパティが、2 つの自明なプロパティのいずれかとすでに同等であるという規則の下で閉じている可能性があります。また、実数直線はこの意味で分解不可能であると見なすことができます。選言の決定不可能性は、すべての順序数などの全順序に関する主張にも影響を及ぼし、順序を定義する選言の節の証明可能性と棄却によって表現されます。これにより、関係が三分関係であるかどうかが決まります。順序数の弱められた理論は、今度は順序解析で定義されている証明理論的強度に影響します。 ${\displaystyle \top }$ ${\displaystyle \bot }$ ${\displaystyle (\alpha \in \beta )\lor (\alpha =\beta )\lor (\beta \in \alpha )}$

その代わりに、構成的集合論は、構成的算術理論の研究でおなじみの、魅力的な選言特性と存在特性を示すことができる。これらは、理論で証明可能な命題の判断をメタ論理的に関連付ける、固定理論の特徴である。特によく研究されているのは、ハイティング算術で数に対する量化子を用いて表現でき、証明理論で形式化されているように、数によって実現できることが多い特徴である。特に、それらは数値的存在特性と密接に関連する選言特性であり、チャーチの規則の下で閉じているため、任意の関数が計算可能であることを証明する。^{[ 2 ]}

集合論は数に関する定理を表現するだけではない。そのため、後述するように、より一般的な、より見つけにくい、いわゆる「強い存在性」を考慮することができる。理論がこの性質を持つとは、以下のことが証明できる場合である。任意の性質について、その性質を持つ集合が存在することを理論が証明する場合、すなわち、理論が存在命題を主張する場合、そのような集合のインスタンスを一意に記述する性質も存在する。より正式には、任意の述語に対して、述語が存在し、 ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle \phi }$ ${\displaystyle \psi }$

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

算術における実現数に相当する役割を、ここでは理論によって（あるいは理論に従って）存在が証明された定義済み集合が担う。公理的集合論の強さと項構成との関係に関する疑問は微妙である。議論されている多くの理論は様々な数値的性質をすべて備えている傾向があるが、存在性は後述するように容易に損なわれる可能性がある。より弱い存在性の形も定式化されている。

存在の古典的な解釈を伴う理論の中には、強い存在特性を示すように制約されるものもあります。集合がすべて順序数定義可能とされるツェルメロ-フランケル集合論 (と表記される理論)では、そのような定義可能性を持たない集合は存在しません。この特性は、における構成可能宇宙公理によっても強制されます。対照的に、によって与えられる理論と完全な選択公理である存在公理を考えてみましょう。この公理の集合は整列定理を証明し、任意の集合に対して整列が存在することを意味することを思い出してください。特に、これはの整列を確立する関係が正式に存在することを意味します(つまり、理論はそれらの関係に関して のすべての部分集合に対する最小元の存在を主張します)。これは、そのような順序付けの定義可能性が と独立であることが知られているという事実にもかかわらずです。後者は、理論の言語の特定の式に対して、対応する集合が実数の整列関係であることを理論が証明しないことを意味します。したがって、整列関係であるという特性を持つサブセットの存在は正式に証明されますが、同時に、その特性を検証できる特定のセットを定義することはできません。 ${\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}$

反古典的原理

前述のように、構成理論はある数とに対して数値的存在性を示すことがあります。ここで、は形式理論における対応する数値を表します。ここでは、2つの命題の間の証明可能な含意と、形式 の理論の性質を注意深く区別する必要があります。後者のタイプのメタ論理的に確立された図式を証明計算の推論規則として採用し、何も新しいことが証明できない場合、その規則の下で 理論は閉じていると言われます${\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} }}}$ ${\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 }$ ${\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 )}}$

Kleene の T 述語は、結果の抽出とともに、数値 にマッピングされる任意の入力数がを通じて計算可能なマッピングであることが証明されることを表します。ここで、 は標準の自然数の集合論モデルを表し、は固定されたプログラム列挙に関するインデックスです。この原理を低複雑度の領域で定義された関数に拡張する、より強い変種が使用されています。この原理は、として定義される述語の決定可能性を否定し、 が自身のインデックスで停止する計算可能関数のインデックスであることを表します。この原理のより弱い二重否定形式も考えられます。これは、すべての の再帰実装の存在を要求しませんが、それでも、再帰実現がないことが証明されている関数の存在を主張する原理とは矛盾します。原理としての Church のテーゼのいくつかの形式は、 2 ソートされた一階述語理論のサブシステムである、古典的な弱いいわゆる二階述語算術理論とさえ一致します。 ${\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}$ ${\displaystyle {\mathsf {RCA}}_{0}}$ ${\displaystyle {\mathsf {Z}}_{2}}$

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

構成原理は既に任意の に対してを証明しています。したがって の任意の要素に対して、命題 に対応する排中律のステートメントを否定することはできません。実際、任意の に対して、無矛盾性により、その否定を同時に排除することは不可能であり、関連するド・モルガンの規則が上記のように適用されます。しかし、理論は場合によっては の拒絶主張 も許容する場合があります。これを採用することは、特定の命題 に対する排中律の失敗を証明する特定の を提供すること、つまり矛盾する を証明することを必要としません。無限領域上の述語は、決定問題に対応します。証明済みの計算可能決定不可能な問題に動機付けられて、 における存在主張を行わずに、述語の決定可能性の可能性を拒絶することができます。別の例として、そのような状況は、量指定子が無限に多くの終わりのない2進シーケンスに及ぶ場合や、シーケンスがどこでもゼロであると述べる場合に、 Brouwerian直観主義解析で強制されます。永遠に一定であるシーケンスとして決定的に識別されるというこの特性に関しては、ブラウワーの連続性原理を採用すると、これがすべてのシーケンスに対して決定可能であることが証明される可能性が厳密に排除されます。 ${\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}$

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

歴史と概要

歴史的に、構成的集合論（しばしば「 」とも呼ばれる）の主題は、ジョン・マイヒルの および とも呼ばれる理論に関する研究から始まった。^{[ 3 ] [ 4 ] [ 5 ]} 1973 年に、彼は前者を直観主義論理に基づく一階集合論として提案し、最も一般的な基礎を取り、選択公理と排中律を捨てて、当初は他のすべてをそのまま残した。しかし、古典的な設定では同値である公理のいくつかの異なる形式は構成的な設定では同値ではなく、いくつかの形式は を意味する（後で実証する）。そのような場合、結果として直観主義的に弱い定式化が採用された。はるかに保守的なシステムも一階理論であるが、いくつかの種類と有界量化を持ち、エレット・ビショップの構成的数学のプログラムに正式な基礎を提供することを目指している。 ${\displaystyle {\mathsf {CST}}}$ ${\displaystyle {\mathsf {IZF}}}$ ${\displaystyle {\mathsf {CST}}}$ ${\displaystyle {\mathsf {ZFC}}}$ ${\displaystyle {\mathsf {ZFC}}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {CST}}}$

主な議論では、 と同じ言語で、ピーター・アツェルのよく研究されたに至る一連の理論を提示し、^{[ 6 ]}以降も続いています。多くの現代的な結果は、ラスジェンと彼の学生に遡ります。 はまた、マイヒルの理論にも存在する 2 つの特徴によって特徴付けられます。一方では、完全な無制限の分離スキーマの代わりに述語的分離を使用しています。有界性は構文プロパティとして扱うことができ、あるいは、代わりに、理論は、より高い有界性述語とその公理を用いて保守的に拡張することができます。第 2 に、非述語的羃集合公理は破棄され、一般に、関連しているがより弱い公理が採用されています。強い形式は、古典的な一般位相で非常に気軽に使用されています。よりもさらに弱い理論に追加すると、以下に詳述するように、が回復されます。^{[ 7 ]} 直観主義ツェルメロ–フランケル集合論 ( ) として知られるようになったこのシステムは、 のない強い集合論です。これは に似ていますが、 ほど保守的でも述語的でもありません。ここで示される理論は の構成的バージョンであり、冪集合の形式を持たず、コレクション公理さえも有界である 古典的なクリプキ・プラテック集合論です。${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathsf {IZF}}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {IKP}}}$ ${\displaystyle {\mathsf {KP}}}$

モデル

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

ペアノ算術は 、マイナス無限大で与えられた理論と無限集合なし、さらにすべての推移的閉包の存在とで双方向に解釈可能である。（後者は、後述する集合帰納法スキーマに正則性を昇格させた後にも暗示される。）同様に、構成的算術は、で採用されているほとんどの公理の言い訳として取ることもできる。ハイティング算術は、 ^{[ 8 ] [ 9 ]}の記事でも説明されているように、弱い構成的集合論と双方向に解釈可能である。帰属関係「」を算術的に特徴付け、それを用いて、自然数の集合の存在の代わりに、その理論のすべての集合が（有限の）フォン・ノイマン自然と一対一であることを証明することができる。この原理は で表される。この文脈は、外延性、ペアリング、和集合、二項交差（述語的分離 の公理スキーマに関連）および集合帰納法スキーマの妥当性をさらに検証する。公理として捉えると、前述の原理は集合論を構成し、これはの存在をマイナスにし、 を公理としてプラスにすることで与えられる理論と既に同一である。これらの公理はすべて以下で詳細に議論される。関連して、 は遺伝的に有限な集合が前述のすべての公理を満たすことも証明する。これは、 およびをマイナス無限大 に渡しても成立する結果である。${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\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}}}$ ${\displaystyle {\mathsf {CZF}}}$

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

表記

公理的集合論では、集合は特性を示す実体である。しかし、集合の概念と論理の間にはより複雑な関係がある。例えば、 100 より小さい自然数という特性は、その特性を持つ数の集合のメンバーであると再定式化できる。集合論の公理は集合の存在を支配し、したがって、どの述語が、この意味で、それ自体として実体化できるかを支配している。仕様指定も、後述するように、公理によって直接支配されている。実際的な考察として、例えば、全体として裏よりも表が多く出る一連のコイン投げの結果であるという特性を考えてみよう。この特性は、コイン投げの有限シーケンスの任意の集合の対応するサブセットを分離するために使用できる。関連して、確率的イベントの測度論的形式化は、集合に基づいて明示的に行われ、より多くの例を提供している。

このセクションでは、この具体化を形式化するために使用されるオブジェクト言語と補助概念を紹介します。

言語

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

ここでも採用されている一般的な扱いは、集合論の基本的な二項述語「」を形式的に拡張するだけです。等号の場合と同様に、要素の否定「」はしばしば「 」と表記されます。 ${\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}$

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

クラスが互いに素であることを表現する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}$

外延的同値性

2つのクラスが全く同じ要素、すなわち、または同値であるを持つことを表す文によって表されます。これは、以下でも使用される 等数性の概念と混同しないでください${\displaystyle A\simeq B}$ ${\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)\}}$

構文的にもっと一般的に言えば、集合は別の 2 項述語troughを使用して特徴付けることもできます。この場合、右側の項は実際の変数 に依存し、場合によってはそれ自体のメンバーシップに依存することもあります。 ${\displaystyle w}$ ${\displaystyle R}$ ${\displaystyle \forall x.x\in w\leftrightarrow R(x,w)}$ ${\displaystyle w}$ ${\displaystyle w}$

ZFの部分理論

ソート理論

構成的集合論

マイヒルの体系は、彼が提示したように、構成的一階述語論理と、集合以外の2つの種、すなわち自然数と関数を用いた理論である。その公理は以下のとおりである ${\displaystyle {\mathsf {CST}}}$

• 集合に対する通常の外延公理、関数に対する通常の外延公理、および和集合公理。
• 制限された、または述語的な分離の公理は、古典的な集合論の分離公理の弱められた形式で、説明したように、任意の量化が別の集合に制限されることを要求します。
• 無限公理の一種で、自然数の集合（定数を導入）は実際には集合であると主張する。${\displaystyle \omega }$
• べき乗公理は、任意の2つの集合に対して、定義域が最初の集合であり、値域が2番目の集合である関数のすべて（そして唯一）を含む第3の集合が存在することを主張する。これは古典集合論におけるべき乗集合公理の大幅に弱められた形であり、マイヒルをはじめとする人々は、その予測不可能性を理由に異議を唱えた。

さらに：

• 自然数に関する通常のペアノ公理
• 関数の定義域と値域が両方とも集合であることを主張する公理。さらに、非選択公理は、選択が既に行われている場合に選択関数が存在することを主張する。これらは、古典集合論における通常の置換公理のように作用する。

前のセクションと比較すると、 この理論の強さを の構築的なサブ理論によって大まかに特定することができます。${\displaystyle {\mathsf {ZF}}}$

そして最終的にこの理論は

• 従属選択公理。これは通常の選択公理よりもはるかに弱いです。

ビショップ流集合論

エレット・ビショップの構成主義派の集合論はマイヒルの集合論と類似しているが、集合がその離散性を支配する関係性を備えているという考え方に基づいている。一般的には従属選択が採用される。

この文脈では、 多くの分析とモジュール理論が開発されてきました。

圏理論

集合に関するすべての形式論理理論が、二項帰属述語「」を直接公理化する必要はありません。集合の圏の初等理論（）のような理論、例えばオブジェクト間の構成可能な写像のペアを捉える理論も、構成的背景論理で表現できます。圏理論は、矢印とオブジェクトの理論として構築できますが、第一階の公理化は矢印についてのみ可能です ${\displaystyle \in }$ ${\displaystyle {\mathsf {ETCS}}}$

それに加えて、トポイには、それ自体が直観主義的であり、集合の概念を捉えることができる内部言語もあります。

圏論における構成的集合論の良いモデルは、指数関数のセクションで述べた前置詞である。優れた集合論によっては、これには十分な射影公理（集合の射影的「表現」に関する公理）が必要となり、可算かつ従属選択となる。

参照

• 述語分離の公理図
• 構成的数学
• 構成的分析
• 構成的チャーチのテーゼ規則と原理
• 計算可能集合
• ディアコネスクの定理
• 選言と存在性
• イプシロン帰納法
• 遺伝的有限集合
• ハイティング算術
• 非述語性
• 直観主義型理論
• 排中律
• 順序分析
• 集合論
• 部分可算性

参考文献

1. フェファーマン、ソロモン（1998年）、In the Light of Logic、ニューヨーク：オックスフォード大学出版局、pp.  280– 283, 293– 294、ISBN 0-195-08030-0
2. Troelstra, AS, van Dalen D.,数学における構成主義：入門1 ; 論理学と数学の基礎研究; Springer, 1988;
3. Bridges D., Ishihara H., Rathjen M., Schwichtenberg H. (編)構成的数学ハンドブック; 論理学と数学の基礎研究; (2023) pp. 20-56
4. マイヒル、ジョン (1973). 「直観主義ツェルメロ＝フランケル集合論のいくつかの性質」(PDF) .ケンブリッジ数理論理学サマースクール. 数学講義ノート. 第337巻. pp.  206– 231. doi : 10.1007/BFb0066775 . ISBN 978-3-540-05569-3。
5. クロシラ、ローラ著『集合論：構成主義的および直観主義的ZF』スタンフォード哲学百科事典、2009年
6. Peter AczelとMichael Rathjen、「構成的集合論に関するノート」、Mittag-Leffler研究所報告書、数理論理学 - 2000/2001、第40号
7. ジョン・L・ベル『直観主義集合論』2018年
8. ジョン・ハヌル（2022）「構成的アッカーマン解釈」、純粋応用論理学会誌、173（5）103086、arXiv：2010.04270、doi：10.1016/j.apal.2021.103086、S2CID 222271938 
9. Shapiro, S., McCarty, C. & Rathjen, M.,直観主義的集合と数：小集合論とHeyting算術, https://doi.org/10.1007/s00153-024-00935-4 , Arch. Math. Logic (2024)
10. Gambino, N. (2005). 「構成的集合論のための前層モデル」(PDF) . Laura Crosilla, Peter Schuster (編). 『集合と型から位相と解析へ』 (PDF) . pp.  62– 96. doi : 10.1093/acprof:oso/9780198566519.003.0004 . ISBN 9780198566519。
11. スコット、DS (1985). 直観主義集合論のための圏論的モデル。カーネギーメロン大学での講演の原稿スライド
12. ベンノ・ファン・デン・ベルグ、「述語的トポス理論と構成的集合論のモデル」、オランダ大学、博士論文、2006年

さらに詳しい参考文献

• トロルストラ、アン、ヴァン・ダーレン、ダーク（ 1988年）。数学における構成主義、第2巻。論理学と数学の基礎研究。619 ページ。ISBN 978-0-444-70358-3。
• Aczel, P. および Rathjen, M. (2001).構成的集合論に関するノート. 技術報告書 40, 2000/2001. ミッタク・レフラー研究所, スウェーデン

外部リンク

• クロシラ、ローラ（2019年2月13日）「集合論：構成的ZFと直観主義的ZF」。ザルタ、エドワード・N.（編）『スタンフォード哲学百科事典』。ISSN 1095-5054。OCLC 429049174。  
• ヴァン・デン・バーグ、ベンノ（2012年9月7日）。「構成的集合理論 – 概要」(PDF)。アムステルダムの Heyting dag からのスライド