タルスキ＝グロタンディーク集合論

タルスキ＝グロタンディーク集合論（TG 、数学者アルフレッド・タルスキとアレクサンダー・グロタンディークにちなんで命名）は公理的集合論である。これはツェルメロ＝フレンケル集合論（ZFC）の非保存的拡張であり、各集合にはそれが属する「タルスキ宇宙」が存在するというタルスキの公理（下記参照）が含まれている点で他の公理的集合論と区別される。タルスキの公理は到達不可能な基数の存在を意味し、ZFCよりも豊かな存在論を提供する。例えば、この公理を追加することで圏論が支持される。

MizarシステムとMetamathは、証明の形式的検証にTarski–Grothendieck集合論を使用しています。

タルスキ＝グロタンディーク集合論は、従来のツェルメロ＝フレンケル集合論を出発点とし、そこに「タルスキの公理」を追加する。ここでは、ミザールの公理、定義、記法を用いて説明する。ミザールの基本的な対象とプロセスは完全に形式的であるが、以下では非形式的に説明する。まず、以下のことを仮定する。

• 任意の集合が与えられた場合${\displaystyle A}$シングルトン${\displaystyle \{A\}}$存在する。
• 任意の2つの集合が与えられた場合、それらの順序付けられていないペアと順序付けられているペアが存在する。
• 任意の集合の集合が与えられた場合、その和集合は必ず存在する。

TGには以下の公理が含まれています。これらはZFCの一部でもあるため、慣習的な公理です。

• 集合公理：量化された変数は集合のみを対象とする。すべては集合である（ ZFCと同じ存在論）。
• 外延性の公理：2つの集合は、同じ要素を持つならば同一である。
• 正則性の公理：いかなる集合もそれ自身を要素とすることはなく、循環的な要素連鎖は不可能である。
• 置換の公理図式：クラス関数のドメインを${\displaystyle F}$セットである${\displaystyle A}$すると、範囲は${\displaystyle F}$（${\displaystyle F(x)}$すべてのメンバー向け${\displaystyle x}$の${\displaystyle A}$も集合です。

TG を他の公理的集合論と区別するのは、タルスキの公理です。タルスキの公理は、無限、選択、^{[ 1 ] [ 2 ] [ 3 ]}および冪集合の公理も含意します。^{[ 4 ] [ 5 ]}また、到達不可能な基数の存在も含意しており、そのおかげでTGの存在論はZFCなどの従来の集合論の存在論よりもはるかに豊かです。

• タルスキの公理（タルスキ 1939 ^{[ 6 ]}より改変）。すべての集合に対して${\displaystyle s}$集合が存在する${\displaystyle u}$（宇宙）

1. ${\displaystyle s\in u}$: 含まれています${\displaystyle s}$
2. ${\displaystyle (\forall x\in u)(\forall y\subseteq x)(y\in u)}$: それはすべてのメンバーのすべての部分集合を含みます
3. ${\displaystyle (\forall x\in u)({\mathcal {P}}(x)\in u)}$: それはすべてのメンバーの冪集合を含んでいます
4. ${\displaystyle (\forall x\subseteq u)(|x|<|u|\to x\in u)}$: より小さい濃度を持つ自身のすべての部分集合を含む

より正式には：

${\displaystyle \forall s\exists u[s\in u\land (\forall x\in u)({\mathcal {P}}(x)\subseteq u\land {\mathcal {P}}(x)\in u)\land (\forall x\subseteq u)(|x|<|u|\to x\in u)]}$

どこ${\displaystyle |\cdot |}$は集合の濃度を表します。簡単に言うと、タルスキの公理は、すべての集合がタルスキ宇宙に属すると述べています。タルスキ宇宙が推移的であれば、それはグロタンディーク宇宙でもあります。^{[ 7 ]}逆に、選択公理を仮定すると、すべてのグロタンディーク宇宙はタルスキ宇宙です（つまり、タルスキの公理を満たします）。^{[ 8 ]}

セット${\displaystyle u}$まるで「ユニバーサルセット」のようだ${\displaystyle s}$—メンバーとして権限セットを持つだけでなく${\displaystyle s}$、およびすべてのサブセット${\displaystyle s}$また、その冪集合の冪集合も持ち、以下同様です。つまり、その要素は冪集合を取る操作や部分集合を取る操作に関して閉じています。これは「普遍集合」のようなものですが、もちろんそれ自体の要素ではなく、すべての集合の集合でもありません。これが保証された宇宙です。${\displaystyle s}$に属する。そして、そのような${\displaystyle u}$それ自体がさらに大きな「ほぼ普遍的な集合」の要素であり、以下同様である。タルスキの公理は、ZFCよりもはるかに多くの集合を保証する公理である。

MizarシステムのTG実装の基盤となり、その論理構文を提供するMizar言語は型付けされており、型は空でないものと想定されています。したがって、理論は暗黙のうちに空でないものとみなされます。存在公理、例えば順序なしペアの存在なども、項コンストラクタの定義によって間接的に実装されています。

このシステムには、等価性、メンバーシップ述語、および以下の標準定義が含まれています。

• シングルトン：要素が1つだけの集合。
• 順序なしペア：2つの異なる要素からなる集合。${\displaystyle \{a,b\}=\{b,a\}}$;
• 順序対：セット${\displaystyle \{\{a,b\},\{a\}\}=(a,b)\neq (b,a)}$;
• 部分集合：すべての要素が別の与えられた集合の要素である集合。
• 集合の和集合${\displaystyle Y}$: 任意のメンバーのすべてのメンバーの集合${\displaystyle Y}$。

Metamathシステムは任意の高階論理をサポートしていますが、通常は「set.mm」で定義された公理と組み合わせて使用​​されます。ax -groth公理はタルスキの公理を追加したもので、Metamathでは次のように定義されています。

⊢ ∃ y ( x ∈ y ∧ ∀ z ∈ y (∀ w ( w ⊆ z → w ∈ y ) ∧ ∃ w ∈ y ∀ v ( v ⊆ z → v ∈ w )) ∧ ∀ z ( z ⊆ y → ( z ≈ y ∨ z ∈ y )))

• サイズの制限に関する公理

• Andreas Blass、IM Dimitriou、Benedikt Löwe (2007)「選択公理なしのアクセス不可能な基数」、Fundamenta Mathematicae 194: 179-89。
• ブルバキ、ニコラス(1972)。「ユニバース」。マイケル・アーティンで;アレクサンドル・グロタンディーク;ジャン＝ルイ・ヴェルディエ（編）。Séminaire de Géométrie Algébrique du Bois Marie – 1963-64 – Théorie des topos et cohomologie étale des schémas – (SGA 4) – vol. 1 (数学の講義ノート269 ) (フランス語)。ベルリン;ニューヨーク: Springer-Verlag。 pp. 185–217 。オリジナルは 2003 年 8 月 26 日にアーカイブされました。 
• パトリック・サップス（1960）『公理的集合論』ヴァン・ノストランド社。ドーバー社再版、1972年。
• アルフレッド、タルスキ(1938)。「Uber unerreichbare Kardinalzahlen」(PDF)。数学の基礎。30 : 68–89 .土井: 10.4064/fm-30-1-68-89。
• Tarski, Alfred (1939). 「任意の集合の整列部分集合について」(PDF) . Fundamenta Mathematicae . 32 : 176– 183. doi : 10.4064/fm-32-1-176-783 .

• Trybulec, Andrzej, 1989, " Tarski–Grothendieck集合論", Journal of Formalized Mathematics .
• Metamath：「証明エクスプローラーのホームページ」。「グロタンディークの公理」までスクロールしてください。
• PlanetMathでのTarski の公理。