述語分離の公理図式

公理的集合論において、述語的分離、制限分離、またはΔ ₀分離の公理図式は、ツェルメロ＝フレンケル集合論における通常の分離公理図式を制限した公理図式である。このΔ _{0という名称は、}算術階層との類推から、レヴィ階層に由来する。

この公理は、集合の全体を参照せずに定義できる部分集合が存在する場合にのみ、その部分集合の存在を主張する。この形式的な記述は完全分離スキーマと同じだが、使用できる式に制限がある。任意の式φに対して、

${\displaystyle \forall x\;\exists y\;\forall z\;(z\in y\leftrightarrow z\in x\wedge \varphi (z))}$

ただし、φには有界量化子のみが含まれており、通常どおり、変数yは自由量化子ではないものとします。したがって、 φに含まれる量化子はすべて、次の形式で現れなければなりません。

${\displaystyle \exists u\in v\;\psi (u)}$

${\displaystyle \forall u\in v\;\psi (u)}$

ある部分式ψと、もちろん定義については${\displaystyle v}$それら規則にも拘束される。

この公理は、構成的集合論（CST）および構成的集合論（CZF）の体系、ならびにクリプキ・プラテック集合論の体系に現れる。

• 構成的集合論
• 分離の公理図式

• テナント、ニール（2021）。「選択は本当に排中律を意味するのか？パートII：グッドマン-マイヒル結果†に関する歴史的、哲学的、基礎的考察」。Philosophia Mathematica。29 ： 28-63。doi ： 10.1093 / philmat /nkaa010。