[dkbrk]

> In contrast, the Quine definition of ordered pairs, defined in definition df-op, is type level. That is, <. x , y >. has the same type as x and y

How is that not a problem? The type of a set needs to be higher than its elements to prevent the construction of a set containing itself. If a tuple is the same type as an elements, then can't you construct a tuple that contains itself as its first element, i.e. "x.0 = x" is a stratified formula so x exists.

[randallholmes]

The Quine pair works in ordinary set theory (Zermelo or ZFC); it has a mildly baroque definition but there is no problem with it. Look at the machinery and you will see why a pair (as opposed to a general set) doesnt strictly speaking need to be of higher type than its components.

[LudwigNagasena]

How is that a problem that a set contains itself? It's allowed in NF.