  Crabbé [1982a] proved the consistency of two predicative fragments of NF: NFP and NFI. Both are extensionality plus existence of \(\{y : \phi(y, x_1 ,\ldots ,x_n)\}\) where \(\phi\) is stratified and there are extra restrictions on the variables in \(\phi\). All variables (bound or free) are restricted to type no higher than that of the set being defined; bound variable are not to be of any type exceeding the type of \(y\) (NFP) or (type of \(y) + 1\) (NFI). NFP + Axiom of sumset = NF. They are distinguished from the other subsystems of NF known to be consistent by the circumstance that they allow a proof of the axiom of infinity which makes essential use of Specker’s proof of the axiom of infinity. In NFP we argue: either the axiom of sumset holds, in which case we have NF and can run Specker’s proof of the Axiom of infinity, or (ii) it doesn’t, in which case – since finite sets have sumsets – not every set is finite.