types in which Amb holds. In 1983, Marcel Crabbé proved consistent a system he called NFI, whose axioms are unrestricted extensionality and those instances of Comprehension in which no variable is assigned a type higher than that of the set asserted to exist. This is a predicativity restriction, though NFI is not a predicative theory: it admits enough impredicativity to define the set of natural numbers (defined as the intersection of all inductive sets; note that the inductive sets quantified over are of the same type as the set of natural numbers being defined). Crabbé also discussed a subtheory of NFI, in which only parameters (free variables) are allowed to have the type of the set asserted to exist by an instance of Comprehension. He called the result "predicative NF" (NFP); it is, of course, doubtful whether any theory with a self-membered universe is truly predicative. Holmes has shown that NFP has the same consistency strength as the predicative theory of types of Principia Mathematica without the Axiom of reducibility. Since 2015, several candidate proofs by Randall Holmes of the consistency of NF relative to ZF have been available both on arXiv and on the logician's home page. Holmes demonstrates the equiconsistency of a 'weird' variant of TST, namely TTTλ - 'tangled type theory with λ-types' - with NF. Holmes next shows that TTTλ is consistent relative to ZFA, that is, ZF with atoms but without choice. Holmes demonstrates this by constructing in ZFA+C, that is, ZF with atoms and choice, a class model of ZFA which includes 'tangled webs of cardinals'. The candidate proofs are all rather long, but no irrecoverable faults have been identified by the NF community as yet. How NF(U) avoids the set-theoretic paradoxes NF steers clear of the three well-known paradoxes of set theory. That NFU, a consistent (relative to Peano arithmetic) theory, also avoids the paradoxes may increase one's confidence in this fact. Russell's paradox: is not a stratified formula, so the existence of is not asserted by any instance of Comprehension. Quine said that he constructed NF with this paradox uppermost in mind. Cantor's paradox of the largest cardinal number exploits the application of Cantor's theorem to the universal set. Cantor's theorem says (given ZFC) that the power set of any set is larger than (there can be no injection (one-to-one map) from into ). Now of course there is an injection from