正則性公理

$ \forall A\left(A\neq\varnothing\implies\exists x\in A\forall a\in A(a\notin x)\right)

空でない集合は、自分自身と交わらない要素を必ず一つ持つ

この意味は同値変形した以下の論理式からのほうが読み取りやすい

$ \forall A\left(A\neq\varnothing\implies\exists x\in A(x\cap A=\varnothing)\right)

この公理の目的

性質

$ \lnot\exist A(A\in A)

$ \because\exist A(A\in A)

$ \iff\exist A(A\in A\land A\neq\varnothing)

$ \implies\exist A(A\in A\land\exists x\in A(x\cap A=\varnothing)

$ \iff\exist A\exist x\in A(x\cap A=\varnothing\land A\in A)

$ \iff\exist A\exist x\in A(x\cap A=\varnothing\land \{x\}\subseteq A\in A)

$ \implies\exist A\exist x\in A(x\cap A=\varnothing\land \{x\}\cap A=\{x\})

$ \implies\bot

別名

References