>>804
＞そもそもループが必要であれば、その考え自体ZFCの基礎の公理に反します

間違っているよ

ZFCの基礎の公理が禁止しているのは、単に∈を使ったループ、つまり ”ｘ∈ｘ”だよ（これを認めると、無限降下列 ・・ｘ∈ｘ∈ｘ∈ｘ ができるから）
一方、包含記号 ⊆ なら、”ｘ⊆ｘ”で、無限降下列 ・・ｘ⊆ｘ⊆ｘ⊆ｘ ができるが、これは無問題
（つまり、ZFCの基礎の公理は、記号∈は等号を含まない 例えば不等号 ”＜”のような性格の記号にしているってことです）

基礎の公理が、全てのループを禁止しているわけではないぞ
（極論すれば、等号＝ならば、ｘ＝ｘで、無限降下列 ・・ｘ＝ｘ＝ｘ＝ｘ ができる）

なお、基礎の公理は、∈-inductionと関連しているという（下記ご参照）

https://en.wikipedia.org/wiki/Epsilon-induction
Epsilon-induction
In mathematics, ∈-induction (epsilon-induction or set-induction) is a variant of transfinite induction.
Considered as a set theory axiom schema, it is called the Axiom schema of set induction.
It can be used in set theory to prove that all sets satisfy a given property. This is a special case of well-founded induction.

Independence
In the context of the constructive set theory CZF, adopting the Axiom of regularity would imply the law of excluded middle and also set-induction.
But then the resulting theory would be standard ZF.
However, conversely, the set-induction implies neither of the two.
In other words, with a constructive logic framework, set-induction as stated above is strictly weaker than regularity.