  Kaye [1991] generalised Specker’s method to show how any typed theory of sets, garnished with the axioms of typical ambiguity, turns out to be equiconsistent with a one-sorted theory. Various weak fragments of NF can be shown consistent by this kind of analysis. Oswald ([1976], [1981] and [1982]) introduced a notation according to which \(NF_n\) is the system axiomatised by the \(n\)-stratified axioms of NF, and \(N_n F\) is extensionality plus the existence of \(\{x : \phi(x)\}\) where \(\phi\) is \(n\)-stratified (parameters are allowed). Oswald showed that