  The hard part is to fully understand stratification. There is an easy rule of thumb with formulæ that are in primitive notation, for one can just ask oneself whether the formula could become a wff of type theory by adding type indices. 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 \(f(x) = y\)? The technical/notational difficulty here lands on top of – as so often – a conceptual difficulty. 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, 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.