By Russel's paradox, we know that the concept of the set of all sets is inconsistent. Similarly, if classes have only sets as members, the concept of the class of all classes is inconsistent because some classes are proper and should be members of this class. But suppose that we consider sets as superclasses of level 0, proper classes as superclasses of level 1 (where superclasses of level 1 also contain superclasses of level 0), superclasses of level 2 as collections whose members are superclasses of level 1, and so on. And let a collection be defined as every superclass with a finite level. Does there exist a formal theory, consistent with say ZFC, such that a concept like the collection of all collections is possible ? Gérard Lang

I think that the least misleading thing to say about the Russell class and the universe in this context is that it is a theorem of firstorder logic (even the constructive fragment thereof) that there is no set containing precisely those sets that are not members of themselves (and the ``Double Russell class'' similarly). You don't need any set theoretic axioms at all, not even extensionality! The nonexistence of the universal set requires set theoretic axioms. The set theoretic axioms that you need may be very appealing to you, but that isn't really the point. The nonexistence of the Russell class is a theorem of pure logic; the nonexistence of the universal set is not, and the difference matters. 


Church’s “Set Theory with a Universal Set” (see, e.g., Thomas Forster’s article) has a set of all sets, and Church provides a model (actually an interpretation in ZFGC) for it. He never published the actual consistency proof, though, and after looking in the Church archives at Princeton, I suspect that he abandoned it, as well as a couple of more complicated theories in which he was attempting to converge with New Foundations. I provide a full consistency proof in an article I’ve submitted to Logique et Analyse, for a variant in which the singleton function is a set (which is impossible in New Foundations), though the natural generalization leads to a variant of the Russell Paradox, the set of all nonselfmembered sets equinumerous to the universe. Arnold Oberschelp also has a set theory with a universal set and the singleton function, though his consistency proof is difficult to verify, as a key part is merely a reference to an earlier article which uses a significantly different formalism. 


I presented a system for reasoning about arbitrary concepts, including the concept "is a concept". It's located at arXiv:1112.6129. The system has full comprehension; there is no restriction on "subconcept" formation. The paper includes a consistency proof. The key idea of my paper is that we do not have a global notion of an object falling under a concept, in exactly the same way that we do not have a global notion of an assertion being true. The best we can do is talk about provably falling under, referring (as constructivists do) to the general semantic notion of provability, not to provability within some formal system. My system deals with concepts like "is a concept that does not provably fall under itself" by restricting the axioms relating to provability. One of the basic axioms that you expect to hold for provability turns out not to have a clear justification. Maybe no one can read this paper because you'd have to be familiar with both Fregean concepts and intuitionistic logic, as well as comfortable with substantial technical content. 


Quine's system New Foundations is now suspected to be consistent with ZFC, and the modified systen NFU has been known to be consistent for decades. These systems certainly allows for a set of all sets, hence do not require any introduction of classes. On the other hand, (sub)set formation is severly restricted. It's perhaps a matter of personal values: do you prefer to have the set $\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;${$x: x=x$} or the functions $\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;X\ni x\mapsto$ {$x$} $\in\mathcal{P}X$? 

