The following question is about the possibility of having a world of sets obeying new foundations "NF" with their well founded sets obeying rules of ZF. It uses the revised version of Quines $``ML"$ (Mathematical Logic (chapter 4)) system, in order to define well foundedness in a faithful manner, and then adds axioms of size and infinity over the well founded sector.
FORMAL EXPOSITION:
Language: First order logic with equality and membership with extra-logical axioms of:
Extensionality: $\forall z (z \in x \leftrightarrow z \in y) \to x=y$
Classes: if $\phi$ is a formula in which $x$ doesn't occur free, then $(\exists x \forall y (y \in x \leftrightarrow set(y) \land \phi))$
Where: $set(y) \iff \exists z(y \in z)$
Define: $x=V \iff \forall y \ (set(y) \to y \in x)$
Define: $x=\{y \in V| \phi\} \iff \forall y (y \in x \leftrightarrow y \in V \land \phi)$
Stratification: if $\phi(y,x_1,..,x_n)$ is a stratified formula in which all quantifiers are bounded by $V$, and all free variables of it are among symbols $``y,x_1,..,x_n"$, then:$$\forall x_1 \in V,...,\forall x_n \in V (\{y\in V| \phi\} \in V)$$
Size: $x,y\text{ are well founded} \land |x|=|y| \land x \in V \to y \in V$
Where: $\text{well founded} (x) \iff \\\not \exists d (x \cap d \neq \emptyset \land \forall m \in d \exists n \in d (n \in m))$
Infinity: $\omega \in V$
Where $\omega$ is the set of all finite Von Neumann ordinals.
Question 1: Is this theory consistent relative to consistency of $NF$ and $ZF$?
Question 2: if we weaken Extensionality to weak Extensionality of $NFU$, as to allow Ur-elements. Would that be consistent relative to $NFU$ and $ZFU$?
