クリプキ・プラテックの集合論 (Kripke– Platek set theory) \(\textrm{KP}\)集合論とは1階の公理的集合論であって\(\textrm{ZF}\)集合論より弱いものである[1]。\(\textrm{KP}\)集合論は無限個の変項記号と2つの関係記号\(=\)と\(\in\)を含む集合論の言語により記述される。


公理

一言に\(\textrm{KP}\)集合論と言っても、それが指すものには2種類の論理体系がある。1つは無限公理を含まないもの(\(\textrm{KP}\)と略される)で、もう1つは無限公理を含むもの(\(\textrm{KP} \omega\)と略されるが、流儀によっては\(\textrm{KP}\)と略される)である。


外延性公理

\[\forall x\forall y(\forall z(z\in x\leftrightarrow z\in y)\rightarrow x=y)\]

集合 \(x\) と \(y\) が全く同じ要素しか持たないならば、それらは等しい。


空集合公理

\[\exists x\forall y(y\notin x)\]

要素を持たない集合が存在する。


対公理

\[\forall x\forall y\exists z\forall w(w\in z\leftrightarrow(w=x\lor w=y))\]

集合 \(x\) と \(y\) に対し、それらのみを要素に持つ集合 \(z=\{x,y\}\) が存在する。


和集合公理

\[\forall x\exists y\forall z(z\in y\leftrightarrow\exists w(z\in w\land w\in x))\]

集合 \(x\) に対し、\(x\) の要素の要素[2]全体からなる集合 \(y=\bigcup x\) (または \(y=\bigcup_{z\in x}z\) とも書かれる)が存在する。


基礎の公理図式

各論理式 \(\phi(x,p_1,\cdots,p_n)\) (または \(\phi(x,\overrightarrow{p})\) と略す)ごとに、以下の論理式を公理として導入する:

\[\forall\overrightarrow{p}(\exists x\phi(x,\overrightarrow{p})\rightarrow\exists x(\phi(x,\overrightarrow{p})\land\neg\exists y(y\in x\land\phi(y,\overrightarrow{p}))))\]

性質 \(\phi(x,\overrightarrow{p})\) を満たす集合 \(x\) が存在するならば、性質 \(\phi(x,\overrightarrow{p})\) を満たす集合 \(x\) の全体の中で \(\in\) に関して極小であるような集合[3]が存在する。


\(\Sigma_0\) 分離公理図式

\(\Sigma_0\) 式とは、全ての量化子が有界である論理式のことである。すなわち\(z \in w\) のように量化子を含まない論理式や、他の \(\Sigma_0\) 式 \(\phi\) を用いて \(\forall x\in y\phi\)(つまり \(\forall x(x\in y\rightarrow\phi)\))や\(\exists x\in y\phi\)(つまり \(\exists x(x\in y\land\phi)\))と表されるもののことである。

各 \(\Sigma_0\) 式 \(\phi(x,\overrightarrow{p})\) ごとに、以下の論理式を公理として導入する:

\[\forall\overrightarrow{p}\forall x\exists y\forall z(z\in y\leftrightarrow(z\in x\land\phi(z,\overrightarrow{p})))\]

集合 \(x\) に対し、\(\phi(z,\overrightarrow{p})\) を満たす \(z \in x\) 全体のなす部分集合 \(y=\{z\in x|\phi(z,\overrightarrow{p})\}\) が存在する。


\(\Sigma_0\)-Collectionの公理図式

各 \(\Sigma_0\) 式 \(\phi(x,y,\overrightarrow{p})\) ごとに、以下の論理式を公理として導入する:

\[\forall\overrightarrow{p}\forall a(\forall x\in a\exists y\phi(x,y,\overrightarrow{p})\rightarrow\exists b\forall x\in a\exists y\in b\phi(x,y,\overrightarrow{p}))\]

集合 \(a\) に対し、「\((x,y)\) が性質 \(\phi(x,y,\overrightarrow{p})\) を満たす」という条件を満たす集合 \(y\) が いかなる \(x \in a\) に対しても[4]存在するならば、\(x \in a\) に依存しないある集合 \(b\) の要素としてそのような \(y\) を選ぶことができる[5]


無限公理

\[\exists x(\varnothing\in x\land\forall y\in x(y\cup\{y\}\in x))\]

ただし \(\varnothing\in x\) という文字列は \(\exists y\in x\forall z(\neg z\in y)\) という論理式の略記であり、\(y\cup\{y\}\in x\) という文字列は \(\exists z\in x\forall w(w\in z\leftrightarrow(w\in y\lor w=y))\) という論理式の略記である。集合論の言語には \(\varnothing\) や \(\cup\) という文字が含まれないため、このように略記を導入する(より正確には定義による拡大を行う)ことがしばしばある。

空集合公理で言及される性質を満たす集合(すなわち空集合)を要素に持ち、また要素の後続もまた要素であるような集合 \(x\) が存在する。基礎の公理図式と合わせると、この \(x\) は無限個の要素を持つことが分かる[6]

またこの公理から空集合公理が従うので、無限公理を課す場合に空集合公理は課しても課さなくてもよい。


拡張

KPi や KPM などの拡張が知られている。これらは順序数解析の分野で現れ、それらの証明論的順序数は非常に大きい。


脚注

  1. \(\textrm{KP}\)集合論 (Cantor's Atticの記事:無効なリンク)
  2. 集合論においては集合の要素もまた集合であるので、集合 \(x\) は集合族でもある。
  3. すなわち性質 \(\phi(x_0,\overrightarrow{p})\) を満たす集合 \(x_0\) であって、いかなる \(x \in x_0\) も \(\phi(x,\overrightarrow{p})\) を満たさないもののことである。
  4. ここで \(a\) の要素に限らず「いかなる 集合 \(x\) に対しても」とする流儀もある。得られる論理式は当然異なるものになってしまうが、公理図式としては同値なものが得られる。
  5. \(x\) を決めても \(y\) は必ずしも一意に決まらないので、\(x\) ごとに \(y\) を選べるからといって \(a\) 全体で一気に \(x\) から \(y\) を定める写像が存在すること(すなわち選択公理)は保証されない。
  6. ただし無限という概念にはいくつもの定式化があり、その1つは無限公理そのものを用いるため、定式化によっては \(x\) が無限個の要素を持つことは単なるトートロジーな主張である。
特に記載のない限り、コミュニティのコンテンツはCC-BY-SAライセンスの下で利用可能です。