 The resolution of this in the system of PM is to adopt an axiom which guarantees that any class defined in terms of another class will be of the same type. Thus impredicative definitions of classes are allowed, and do not introduce a class of a higher type. This is accomplished by adopting the Axiom of Reducibility, in ∗12, which guarantees that for any function \(\phi\), there will be a co-extensive predicative function. More precisely, the Axiom of Reducibility asserts that for any function of any number of arguments of an arbitrary level, there is an equivalent function of level 1, ie. one true of the same entities: