 Even after the logics developed by Russell, Zermelo and Tarski had created the theoretical means to get rid of difficulties involved in the notions of class, set, truth, definability, the paradoxes have remained alive. This probably is due to a persistent interest in alternative formal paradigms, to the controversial features and axioms of Principia Mathematica, and to the problematic place that self-reference occupies in mathematical logic. In this context, it is worth mentioning Quine’s paper of 1937 on the system NF (see the entry  Quine’s New Foundations),  which takes inspiration from the Russellian notion of typical ambiguity, that is, from the systematic device of suppressing the order indices of propositional functions and their arguments, leaving them to be restored at will, when needed, according to the discipline of type theory (see 3.2 above). The idea is to restrict naive comprehension to those instances that are stratified, where in general a formula \(\phi\) is stratified iff it is possible to assign a natural number (type in short) to each term occurrence in such a way that the resulting formula is well-formed in the sense of type theory, e.g., if \(t \in\) s is a subformula of \(\phi\), the type of \(s\) is one greater than the type of \(t\), etc.. Clearly, stratification blocks set formation when formulas of the form \(x\in x, \neg x\in x\) are present. Moreover, in NF the universal set exists. The consistency problem for NF is still open (though partial results are known concerning fragments with bounds on stratification or restriction to extensionality). Remarkably, NF refutes the axiom of choice by a classical theorem of Specker. Again, a classical result of Specker establishes the existence of a model of NF in a suitable version of simple type theory with a formal counterpart of typical ambiguity. Paradoxes are not that far from NF. In 1942 Rosser (and independently Lyndon) published a form of Burali-Forti’s antinomy in a seemingly natural extension (named ML) of the system NF, obtained by adding “ultimate classes”. ML was defined to avoid certain weaknesses of NF (e.g., with respect to number theoretic induction). Once more, the Lyndon-Rosser result brought about the unexpected presence of a paradox in set theory and the foundations of mathematical logic.