Is this a set in New Foundations theory of sets: A={x∈X: x∉f(x)} when X=universal set and f(x)=x? Does the formula A={x∈X: x∉f(x)} define a set in New Foundations theory of sets (NF) when X=universal set and f(x)=x? If not: WHY?
It can be seen that many elements of universal set (X) satisfy the condition of the formula:


*

*If x=∅(it is possible since ∅ is an element of  universal set(∅∈X)):
Then: f(∅)=∅ and ∅∉∅.
So, in this case x∈X and x∉f(x), thus ∅∈A. We already have one element of A!

*If x≠∅:
This case is also possible, since there is an infinite number of elements of X, for which f(x)=x, but x∉f(x), for example f(x)=x={1,2,3}. But {1,2,3}∉{1,2,3}.
Thus infinite number of elements of A exits, that satisfy condition: x∈X: x∉f(x).
Nonetheless I have to believe, the formula A={x∈X: x∉f(x)} does not define a set in NF, because if it did, the Cantor’s theorem would be valid in NF. But Cantor's theorem is not valid in NF.
Does this set violate some of the axioms of NF?
 A: I actually left a comment on this on your other thread. $\{x\in X: x\notin f(x)\}$ does not define a set. The reason is that the defining formula is unstratified: $x$ and $f(x)$ must have the same type to be stratified, but in $x\notin y$, $y$ must be one type higher than $x$. So our axioms don't guarantee such a set and Cantor's paradox disproves such a set.
However, let $\iota``X := \{\{x\}: x\in X\}$ and assume that you have a function $f:\iota``X\to\mathscr{P}(X)$. Then the set $\{x: \neg(\{x\}\subseteq f(\{x\}))\}$ is stratified and does exist for every set, even $V$. If $f$ were a surjection, we could get Cantor's paradox again, so we show that there is no surjection $\iota``X\to\mathscr{P}(X)$. Since there is a surjection $V\to\mathscr{P}(V)$, what this shows is that in NF $\iota``V < V$, which is an odd result central to much of NF's interesting mathematics. It's a lot like if you could divide a tank of goldfish by putting each in their own bowl, but you could do it by using fewer bowls than fish.
A: This set cannot be defined because the formula $x \notin x$ appearing in the putative set definition $\{x \in X : x \notin x\}$ cannot be stratified.  The restriction of the separation axiom schema to stratified formulas is how New Foundations manages to avoid Russell's paradox even though it allows a universal set.
To be more precise, I should say that the notation $\{x \in X : x \notin x\}$ cannot be said to define a set solely on the basis of the separation axiom schema of NF.  For certain $X$ the notation $\{x \in X : x \notin x\}$ may happen to define a set; for example if $X$ is the empty set it is safe to say that the notation $\{x \in X : x \notin x\}$ defines a set (also the empty set.)  But if $X$ is the universal set then the notation $\{x \in X : x \notin x\}$ cannot define a set, or the argument of Russell's paradox would lead to a contradiction.
