*12. THE HIERARCHY OF TYPES AND THE AXIOM OF REDUCIBILITY.
Project Gutenberg EPUB3 edition
Whitehead, Alfred North and Russell, Bertrand
*12·11.
We call two functions , formally equivalent when , and similarly we call and formally equivalent when Thus the above axioms state that any function of one or two variables is formally equivalent to some predicative function of one or two variables, as the case may be.
Of the above two axioms, the first is chiefly needed in the theory of classes (*20), and the second in the theory of relations (*21). But the first is also essential to the theory of identity, if identity is to be defined (as we have done, in *13·01); its use in the theory of identity is embodied in the proof of *13·101, below.
We may sum up what has been said in the present number as follows:
(1) A function of the first order is one which involves no variables except individuals, whether as apparent variables or as arguments.
(2) A function of the (th order is one which has at least one argument or apparent variable of order , and contains no argument or apparent variable which is not either an individual or a first-order function or a second-order function or ... or a function of order .
(3) A predicative function is one which contains no apparent variables, i.e. is a matrix. It is possible, without loss of generality, to use no variables except matrices and individuals, so long as variable propositions are not required.
(4) Any function of one argument or of two is formally equivalent to a predicative function of the same argument or arguments.