 NF3+Infinity has the same strength as second-order arithmetic. So does NFI (which has just enough impredicativity to define the natural numbers, and not enough for the Least Upper Bound Axiom). NFP is equivalent to a weaker fragment of arithmetic, but does (unlike NFU) prove Infinity: this is the only application of the Specker proof of the negation of the Axiom of Choice to a provably consistent theory. Either Union is true (in which case we readily get all of NF and Specker’s proof of Infinity goes through) or Union is not true, in which case we note that all finite sets have unions, so there must be an infinite set. NF3 has considerable interest for a surprising reason: it turns out that all infinite models of TST3 (simple type theory with three types) satisfy the ambiguity schema \(\phi \equiv \phi^+\) (of course this only makes sense for formulas with one or two types) and this turns out to be enough to show that for any infinite model of TST3 there is a model of NF3 with the same theory. NF4 is the same theory as NF (Grishin 1969), and we have no idea how to get a model of TST4 to satisfy ambiguity.