Is the following set stratified (and why not) in New Foundations?

Question

notation:

$Id=\{\langle x,y\rangle : x=y\}$ (identity relation)

$X[y]$ (image of an element y under a relation X)

the set I am asking for is:

$Z=\{\langle x,y\rangle : \neg \exists k\; y \in k \wedge \langle y,k\rangle \in x\}[Id]$

in words:

it is an image of the element (which is a relation) $Id$ under $\{\langle x,y\rangle : \neg \exists k\; y \in k \wedge \langle y,k\rangle \in x\}$

Answer 1

The condition for stratification for a formula $\Phi$ in Quine's New Foundation :

requires that there should be a function $\sigma$ (a “stratification”) from the bound variables in $\Phi$ to an initial segment of the natural numbers such that if ‘$u \in v$’ is a subformula of $\Phi$ then $\sigma(v) = \sigma (u) + 1$ and if ‘$u = v$’ is a subformula of $\Phi$ then $\sigma (v) = \sigma(u)$.

In your proposal, you are using $\langle y, k \rangle$, that is $\{ \{ y \} \{ y, k \} \}$; because of $y \in \{ y \}$ we need $\sigma(y) = n$ and $\sigma(\{ y \}) = n+1$, and also $\sigma(\{ y, k \}) = n+1$.

We have also $y \in k$, so that $\sigma(k) = n+1$.

But $k \in \{ y, k \}$ and this conflicts with the above assignements.

According to the SEP entry :

to fully understand stratification [...] It's harder when one has formulæ no longer in primitive notation, and the reader encounters these difficulties very early on, since the ordered pair is not a set-theoretic notion. How does one determine whether or not a formula is stratified when it contains subformulæ like $ƒ(x) = y$? The answer is that of course one has to fix an implementation of ordered pair and stick to it. Does that mean that — for formulæ involving ordered pairs — whether or not the given formula is stratified depends on how one implements ordered pairs? The answer is ‘yes' but the situation is not as grave as this suggests. There are various standard definitions of ordered pair [see pairing function], and they are all legitimate in $NF$, and all satisfactory in the sense that they are “level” or homogeneous. All of them make the formula $\langle x, y \rangle = z$ stratified and give the variables $x$ and $y$ the same type; $z$ takes a higher type in most cases (never lower). How much higher depends on the version of ordered pair being used, but there are very few formulæ that come out stratified on one version of ordered pair but unstratified on another, and they are all pathological in ways reminiscent of the paradoxes.

Thus, in every case we have problems with the formula $y \in k \land \langle y, k \rangle \in x$.