クリプキ・プラテックの集合論 (Kripke– Platek set theory) \(\textrm{KP}\)集合論とは1階の公理的集合論であって\(\textrm{ZF}\)集合論より弱いものである[1]。\(\textrm{KP}\)集合論は無限個の変項記号と２つの関係記号\(=\)と\(\in\)を含む集合論の言語により記述される。
公理[]
一言に\(\textrm{KP}\)集合論と言っても、それが指すものには２種類の論理体系がある。１つは無限公理を含まないもの（\(\textrm{KP}\)と略される）で、もう１つは無限公理を含むもの（\(\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 などの拡張が知られている。これらは順序数解析の分野で現れ、それらの証明論的順序数は非常に大きい。
脚注[]
- ↑ \(\textrm{KP}\)集合論 （Cantor's Atticの記事：無効なリンク）
- ↑ 集合論においては集合の要素もまた集合であるので、集合 \(x\) は集合族でもある。
- ↑ すなわち性質 \(\phi(x_0,\overrightarrow{p})\) を満たす集合 \(x_0\) であって、いかなる \(x \in x_0\) も \(\phi(x,\overrightarrow{p})\) を満たさないもののことである。
- ↑ ここで \(a\) の要素に限らず「いかなる 集合 \(x\) に対しても」とする流儀もある。得られる論理式は当然異なるものになってしまうが、公理図式としては同値なものが得られる。
- ↑ \(x\) を決めても \(y\) は必ずしも一意に決まらないので、\(x\) ごとに \(y\) を選べるからといって \(a\) 全体で一気に \(x\) から \(y\) を定める写像が存在すること（すなわち選択公理）は保証されない。
- ↑ ただし無限という概念にはいくつもの定式化があり、その１つは無限公理そのものを用いるため、定式化によっては \(x\) が無限個の要素を持つことは単なるトートロジーな主張である。