自分自身を含む集合

$ A\in Aが成立する集合$ Aのこと

正則性公理を採用する公理系では構成できない

方針

$ A\in Aが成り立つ場合、$ \{A\}が正則性公理に違反する

$ A\in A

$ \implies A\cap \{A\}\neq\varnothing

$ \iff \forall A'\in\{A\};A'\cap\{A\}\neq\varnothing

$ \iff \bot

$ \because \forall B\left(B\neq\varnothing\implies\exists x\in B(x\cap B=\varnothing)\right) \implies \exists A'\in \{A\};A'\cap\{A\}=\varnothing

$ \therefore \forall A;A\notin A

自分自身を含む集合#618b43cf1280f00000c93d6eを書いていて気付いたけど、正則性公理から$ \impliesをつなぐだけでも証明できそうだな

$ \{A\}を作る部分は同じ

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

$ \implies \forall A\exists x\in \{A\};x\cap\{A\}=\varnothing

$ B=\{A\}を代入した

$ \iff \forall A;A\cap\{A\}=\varnothing

$ \iff \forall A\forall a(a\in A\land a\in \{A\}\iff \bot)

$ \because外延性公理と$ a\in \varnothing \iff \bot

$ \iff \forall A\forall a(\lnot(a\in A\land a=A))

$ \implies \forall A;A\notin A

$ a=Aを代入した