With a rigorous foundation, these paradoxes instead suggest proofs that certain classes are proper (i.e., that they are not sets). For example, Russell's paradox suggests a proof that the class of all sets which do not contain themselves is proper, and the Burali-Forti paradox suggests that the class of all ordinal numbers is proper. The paradoxes do not arise with classes because there is no notion of classes containing classes. Otherwise, one could, for example, define a class of all classes that do not contain themselves, which would lead to a Russell paradox for classes. A conglomerate, on the other hand, can have proper classes as members, although the "theory" of conglomerates is not yet well-established. ZF set theory does not formalize the notion of classes, so each formula with classes must be reduced syntactically to a formula without classes. For example, one can reduce the formula formula_1 to formula_2. Semantically, in a metalanguage, the classes can be described as equivalence classes of logical formulas: If formula_3 is a structure interpreting ZF, then the object language "class-builder expression" formula_4 is interpreted in formula_3 by the collection of all the elements from the domain of formula_3 on which formula_7 holds; thus, the class can be described as the set of all predicates equivalent to formula_8 (which includes formula_8 itself). In particular, one can identify the "class of all sets" with the set of all predicates equivalent to formula_10  Because classes do not have any formal status in the theory of ZF, the axioms of ZF do not immediately apply to classes. However, if an inaccessible cardinal formula_11 is assumed, then the sets of smaller rank form a model of ZF (a Grothendieck universe), and its subsets can be thought of as "classes". In ZF, the concept of a function can also be generalised to classes. A class function is not a function in the usual sense, since it is not a set; it is rather a formula formula_12 with the property that for any set formula_13 there is no more than one set formula_14 such that the pair formula_15 satisfies formula_16 For example, the class function mapping each set to its successor may be expressed as the formula formula_17 The fact that the ordered pair formula_15 satisfies formula_19 may be expressed with the shorthand notation formula_20  Another approach is taken by the von Neumann–Bernays–Gödel axioms (NBG); classes are the basic objects in this theory, and a set is then defined to be a class that is an element of some other class.