>>411
つづき

（参考）
https://ja.wikipedia.org/wiki/%E6%AD%A3%E5%89%87%E6%80%A7%E5%85%AC%E7%90%86
正則性公理
ZF公理系を構成する公理の一つで、1925年にジョン・フォン・ノイマンによって導入された。

定義
以下の4つの主張はいずれも同値であり、どれを正則性の公理として採用しても差し支えない。

・∀xについて、∈がx上well-founded
・∀xについて、無限下降列である x∋x1∋x2∋... は存在しない。
・ V=WF
ここで、Vはフォン・ノイマン宇宙を指し、WFは0に冪集合の演算を有限回、あるいは超限回繰り返して得られる集合全体のクラスを指す。
ZF公理系の他の公理系から得られる種々の集合演算(対集合、和集合、冪集合) の結果としての集合は常にWF内に含まれるため、V=WFの仮定は全ての集合を0に通常の集合演算を施すことによって得られるものだけに制限することを主張している。
したがって、例えばx={xのような集合やx∈yかつy∈xなる集合は正則性の公理の下では集合にはなり得ない。
WFは通常の集合演算に関して閉じているため、WF公理系から得られる全ての真なる命題がZF公理系においても真となることが分かる。
このため、WF公理系内で通常の数学を展開できることが知られている。

つづく