These considerations are relevant to our definition of the derived extensional function. We there spoke of "a function formally equivalent to ." It is necessary to decide upon the type of our function. Any decision will do, but some decision is unavoidable. Let us call the supposed formally equivalent function . Then appears as a variable, and must be of some determinate type. All that we know necessarily about the type of is that it takes arguments of a given type—that it is (say) an -function. But this, as we have just seen, does not determine its type. If we are to be able (as our fifth requisite demands) to deal with all classes whose members are of the same type as , we must be able to define all such classes by means of functions of some one type; that is to say, there must be some type of -function, say the , such that any -function is formally [Pg 190] equivalent to some -function of the type. If this is the case, then any extensional function which holds of all -functions of the type will hold of any -function whatever. It is chiefly as a technical means of embodying an assumption leading to this result that classes are useful. The assumption is called the "axiom of reducibility," and may be stated as follows:— "There is a type ( say) of -functions such that, given any -function, it is formally equivalent to some function of the type in question." If this axiom is assumed, we use functions of this type in defining our associated extensional function. Statements about all -classes (i.e. all classes defined by -functions) can be reduced to statements about all -functions of the type . So long as only extensional functions of functions are involved, this gives us in practice results which would otherwise have required the impossible notion of "all -functions." One particular region where this is vital is mathematical induction. The axiom of reducibility involves all that is really essential in the theory of classes. It is therefore worth while to ask whether there is any reason to suppose it true.