> Is this theory consistent? Language: first order language of set theory, Extra-logical axioms: **1. Extensionality:** as in $\sf NF$. **2. Stratified Comprehension:** as in $\sf NF$. ***Define:*** a set is said to be well founded if it is not an element of a descending membership set. Formally: $$\operatorname {well-founded}(s) \iff \neg \exists x: s \in x \land \forall y \in x \exists z: z \in y \cap x $$ **3. Replacement:** if $A$ is a well founded set, and $\phi(x,y)$ is a formula standing for a many-to-one relation from well founded sets to well founded sets, that doesn't mention "$B$", then there is a set $B=\{y \mid \exists x \in A : \phi(x,y)\}$. **4. Infinity:** There is a well-founded set having the empty set among its elements, that is closed under singletons. **5. Choice:** For every nonempty set of pairwise disjoint well-founded nonempty sets, there is a set that has singleton intersections with each of its elements. So, this theory has a universe obeying the rules of $\sf NF $, and has its well founded realm obeying the rules of $\sf ZFC$. It is known that there is a consistent similar theory that extends $\sf NFU$. A corollary of Randall Holmes theory that speaks about the [$\sf BEST$][1] model of $\sf NFU$. But, is this the case with $\sf NF$? I've asked a [similar][2] question before but in terms of $\sf ML$, this question is in terms of $\sf NF$. [1]: https://randall-holmes.github.io/Papers/nfumcorrected.pdf [2]: https://mathoverflow.net/q/353428/95347