*9. EXTENSION OF THE THEORY OF DEDUCTION FROM LOWER TO HIGHER TYPES OF PROPOSITIONS.
Project Gutenberg EPUB3 edition
Whitehead, Alfred North and Russell, Bertrand
*9·401.
*9·41.
*9·411.
*9·42.
*9·421.
*9·5.
Dem.
*9·501.
*9·51.
Dem.
*9·511.
*9·52.
Dem.
*9·521.
*9·6.
*9·61. If and are elementary functions of the same type, there is a function .
Dem.
By *9·14·15, there is an for which "," and therefore "," are significant, and therefore so is "," by the primitive idea of disjunction. Hence the result by *9·15.
The same proof holds for functions of any number of variables.
*9·62. If and are elementary functions, and the -argument to is of the same type as the argument to , there are functions
Dem.
By *9·15, there are propositions and , where by hypothesis and are of the same type. Hence by *9·14 there is a proposition , and therefore, by the primitive idea of disjunction, there is a proposition , and therefore, by *9·15 and *9·03, there is a proposition (. Similarly there is a proposition (. Hence the result, by *9·15.
*9·63. If , are elementary functions of the same type, there are functions (, etc. [Proof as above]
We have now completed the proof that, in the primitive propositions of *1, any one of the propositions that occur may be replaced by ( or (. It follows that, by merely repeating the proofs, we can show that any other of the propositions that occur in these propositions can be simultaneously replaced by ( or (. Thus all the primitive propositions of *1, and therefore all the propositions of *2—*5, hold equally when some or all of the propositions concerned are of one of the forms (, (, which was to be proved.
It follows, by mere repetition of the proofs, that the propositions of *1—*5 hold when , , are replaced by propositions containing any number of apparent variables.