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

タルスキ＝グロタンディーク集合論（タルスキ＝グロタンディークしゅうごうろん、、略称 TG）は、数学者アルフレト・タルスキとアレクサンドル・グロタンディークにちなんで名付けられた公理的集合論の体系である。ツェルメロ＝フレンケル集合論（ZFC）の非保存的拡大であり、「各集合に対しそれが属する『タルスキ宇宙』が存在する」と述べるタルスキの公理を含む点で、他の公理的集合論と区別される（後述）。タルスキの公理は到達不能基数の存在を含意し、ZFC より豊かな存在論を与える。例えば、この公理を追加することで圏論を支えることができる。

Mizar システムおよび Metamath は、にタルスキ＝グロタンディーク集合論を用いる。

公理

タルスキ＝グロタンディーク集合論は、通常のツェルメロ＝フレンケル集合論を出発点とし、そこへ「タルスキの公理」を加えるものである。ここでは Mizar の公理、定義、記法を用いて記述する。Mizar の基本対象と操作は完全に形式的であるが、以下では非公式に説明する。まず次を仮定する。

任意の集合が与えられたとき、単元集合が存在する。任意の2つの集合が与えられたとき、それらの非順序対と順序対が存在する。集合からなる任意の集合が与えられたとき、その和が存在する。

TG は以下の公理を含む。これらは ZFC の一部でもあるため伝統的なものである。集合公理: 変数の量化は集合のみをわたり、すべては集合である（ZFC と同じ存在論）。外延性の公理: 同じ要素を持つ2つの集合は同一である。正則性公理: どの集合も自分自身の要素ではなく、所属関係の循環鎖は不可能である。置換公理（公理図式）: クラス関数の定義域が集合であるとき、の値域（のすべての要素に対するの値の全体）もまた集合である。

TG を他の公理的集合論と区別するのがタルスキの公理である。タルスキの公理はさらに、無限公理、選択公理Tarski (1938)Tarski (1939), p. 181、そして冪集合公理を含意する, Re: AC and strongly inaccessible cardinals.Metamath grothpw.。また到達不能基数の存在を含意し、そのおかげで TG の存在論は ZFC のような通常の集合論よりはるかに豊かである。

タルスキの公理（Tarski 1939Tarski (1939) による）。すべての集合に対し、次を満たす集合（「宇宙」）が存在する。 : を含む : すべての要素のすべての部分集合を含む : すべての要素の冪集合を含む : 自分自身のうちより小さい濃度を持つすべての部分集合を含む

より形式的には:

ここでは集合の濃度を表す。要するに、タルスキの公理は「すべての集合があるタルスキ宇宙に属する」ことを述べている。タルスキ宇宙が推移的集合であれば、それはまたグロタンディーク宇宙でもある。逆に選択公理を仮定すれば、すべてのグロタンディーク宇宙はタルスキ宇宙である（すなわちタルスキの公理を満たす）。

集合はにとっての「普遍集合」のように見える。の冪集合やのすべての部分集合を要素として持つだけでなく、その冪集合の冪集合なども持ち、その要素は冪集合を取る操作や部分集合を取る操作で閉じている。ただしもちろん自分自身の要素ではなく、すべての集合の集合でもない。それが保証された宇宙であり、はこれに属する。さらに、そのようなは自らも一層大きな「ほぼ普遍的な集合」の要素であり、以下同様に続く。タルスキの公理は ZFC よりはるかに多くの集合の存在を保証する公理なのである。

Mizar システムでの実装

Mizar 言語は TG の Mizar システム実装の基盤となり、その論理的構文を提供している。Mizar 言語は型付きであり、型は空でないと仮定される。したがって、この理論は暗黙に非空とみなされる。非順序対の存在などの存在公理も、項構成子の定義を通じて間接的に実装される。

このシステムは等号、所属述語、および以下の標準的な定義を含む: 単集合: 要素をひとつだけ持つ集合; : 相異なる2つの要素を持つ集合。; 順序対: となる集合; 部分集合: そのすべての要素が別の与えられた集合の要素でもあるような集合; 集合からなる集合の和集合: のいずれかの要素のすべての要素からなる集合。

Metamath での実装

Metamath システムは任意の高階論理をサポートするが、通常は公理の "set.mm" 定義とともに使われる。ax-groth 公理はタルスキの公理を加えるものであり、Metamath では次のように定義される:

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

Źródło i licencja