 Grišin 1981 proved that the system based upon the paradoxical principle par excellence—the uniform naïve comprehension schema—and (some form of) non-contractive logic enjoys cut elimination, and hence is consistent. On the other hand, the consistency of the system is ruined by extensionality and this could be counted as an additional paradox! Of course ‘uniform’ here means that a variable-binding abstraction operator {x | φ(x,a)} for naming the set defined by φ, depending on a list of given parameters a, is available. Interestingly, it has been shown that closely related systems have unexpected applications to the characterization of complexity classes (Girard 1998, Terui 2004); on the other hand, the system is computationally complete (it can interpret combinatory logic, Cantini 2003).