-functions the first type of
-functions;
-functions involving reference to the totality of the first type we call the second type; and so on. No variable
-function can run through all these different types: it must stop short at some definite one.
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