Principia mathematica, vol. 1 (of 3)

In the present number, we introduce two new primitive ideas, which may be expressed as " is always[50] true" and " is sometimes[51] true," or, more correctly, as " always" and " sometimes." When we assert " always," we are asserting all values of , where "" means the function itself, as opposed to an ambiguous value of the function (cf. pp. 15, 42); we are not asserting that is true for all values of , because, in accordance with the theory of types, there are values of for which "" is meaningless; for example, the function itself must be such a value. We shall denote " always" by the notation where the "" will be followed by a sufficiently large number of dots to cover the function of which "all values" are concerned. The form in which such propositions most frequently occur is the "formal implication," i.e. such a proposition as i.e. " always implies ." This is the form in which we express the universal affirmative "all objects having the property have the property ."

In a proposition of either of the two forms , (, the is called an apparent variable. A proposition which contains no apparent variables is called "elementary," and a function, all whose values are elementary propositions, is called an elementary function. For reasons explained in Chapter II of the Introduction, it would seem that negation and disjunction and their derivatives must have a different meaning when applied to elementary propositions from that which they have when applied to such propositions as or . If is an elementary function, we will in this number call and "first-order propositions." Then in virtue of the fact that disjunction and negation do not have the same meanings as applied to elementary or to first-order propositions, it follows that, in asserting the primitive propositions of *1, we must either confine them, in their application, to propositions of a single type, or we must regard them as the simultaneous assertion of a number of different primitive propositions, corresponding to the different meanings of "disjunction" and "negation." Likewise in regard to the primitive ideas of disjunction and negation, we must either, in the primitive propositions of *1, confine them to disjunctions and negations of elementary propositions, or we must regard them as really each multiple, so that in regard to each type of propositions we shall need a new primitive idea of negation and a new primitive idea of disjunction.

In the present number, we shall show how, when the primitive ideas of negation and disjunction are restricted to elementary propositions, and the , , of *1—*5 are therefore necessarily elementary propositions, it is possible to obtain definitions of the negation and disjunction of first-order propositions, and proofs of the analogues, for first-order propositions, of the primitive propositions *1·2—·6. (*1·1 and *1·11 have to be assumed afresh for first-order propositions, and the analogues of *1·7·71·72 require a fresh treatment.) It follows that the analogues of the propositions of *2—*5 follow by merely repeating previous proofs. It follows also that the theory of deduction can be extended from first-order propositions to such as contain two apparent variables, by merely repeating the process which extends the theory of deduction from elementary to first-order propositions. Thus by merely repeating the process set forth in the present number, propositions of any order can be reached. Hence negation and disjunction may be treated in practice as if there were no difference in these ideas as applied to different types; that is to say, when "" or "" occurs, it is unnecessary in practice to know what is the type of or , since the properties of negation and disjunction assumed in *1 (which are alone used in proving other properties) can be asserted, without formal change, of propositions of any order or, in the case of , of any two orders.

The limitation, in practice, to the treatment of negation or disjunction as single ideas, the same in all types, would only arise if we ever wished to assume that there is some one function of whose value is always , whatever may be the order of , or that there is some one function of and whose value is always , whatever may be the orders of and . Such an assumption is not involved so long as (and ) remain real variables, since, in that case, there is no need to give the same meaning to negation and disjunction for different values of (and ), when these different values are of different types. But if (or ) is going to be turned into an apparent variable, then, since our two primitive ideas and both demand some definite function , and restrict the apparent variable to possible arguments for , it follows that negation and disjunction must, wherever they occur in the expression in which (or ) is an apparent variable, be restricted to the kind of negation or disjunction appropriate to a given type or pair of types. Thus, to take an instance, if we assert the law of excluded middle in the form there is no need to place any restriction upon : we may give to a value of any order, and then give to the negation and disjunction involved those meanings which are appropriate to that order. But if we assert it is necessary, if our symbol is to be significant, that "" should be the value, for the argument , of a function ; and this is only possible if the negation and disjunction involved have meanings fixed in advance, and if, therefore, is limited to one type.

Thus the assertion of the law of excluded middle in the form involving a real variable is more general than in the form involving an apparent variable. Similar remarks apply generally where the variable is the argument to a typically ambiguous function.

In what follows the single letters p and q will represent elementary propositions, and so will "," "," etc. We shall show how, assuming the primitive ideas and propositions of *1 as applied to elementary propositions, we can define and prove analogous ideas and propositions as applied to propositions of the forms and . By mere repetition of the analogous process, it will then follow that analogous ideas and propositions can be defined and proved for propositions of any order; whence, further, it follows that, in all that concerns disjunction and negation, so long as propositions do not appear as apparent variables, we may wholly ignore the distinction between different types of propositions and between different meanings of negation and disjunction. Since we never have occasion, in practice, to consider propositions as apparent variables, it follows that the hierarchy of propositions (as opposed to the hierarchy of functions) will never be relevant in practice after the present number.

The purpose and interest of the present number are purely philosophical, namely to show how, by means of certain primitive propositions, we can deduce the theory of deduction for propositions containing apparent variables from the theory of deduction for elementary propositions. From the purely technical point of view, the distinction between elementary and other propositions may be ignored, so long as propositions do not appear as apparent variables; we may then regard the primitive propositions of *1 as applying to propositions of any type, and proceed as in *10, where the purely technical development is resumed.

It should be observed that although, in the present number, we prove that the analogues of the primitive propositions of *1, if they hold for propositions containing apparent variables, also hold for such as contain , yet we must not suppose that mathematical induction may be used to infer that the analogues of the primitive propositions of *1 hold for propositions containing any number of apparent variables. Mathematical induction is a method of proof which is not yet applicable, and is (as will appear) incapable of being used freely until the theory of propositions containing apparent variables has been established. What we are enabled to do, by means of the propositions in the present number, is to prove our desired result for any assigned number of apparent variables—say ten—by ten applications of the same proof. Thus we can prove, concerning any assigned proposition, that it obeys the analogues of the primitive propositions of *1, but we can only do this by proceeding step by step, not by any such compendious method as mathematical induction would afford. The fact that higher types can only be reached step by step is essential, since to proceed otherwise we should need an apparent variable which would wander from type to type, which would contradict the principle upon which types are built up.

Definition of Negation. We have first to define the negations of ( and (. We define the negation of as , i.e. "it is not the case that is always true" is to mean "it is the case that is sometimes true." Similarly the negation of ( is to be defined as . Thus we put

In virtue of these definitions, the true scope of an apparent variable is always the whole of the asserted proposition in which it occurs, even when, typographically, its scope appears to be only part of the asserted proposition. Thus when ( or appears as part of an asserted proposition, it does not really occur, since the scope of the apparent variable really extends to the whole asserted proposition. It will be shown, however, that, so far as the theory of deduction is concerned, ( and ( behave like propositions not containing apparent variables.

Of these, the first states that, if is true, then there is a value of which is true; i.e. if we can find an instance of a function which is true, then the function is "sometimes true." (When we speak of a function as "sometimes" true, we do not mean to assert that there is more than one argument for which it is true, but only that there is at least one.) Practically, the above primitive proposition gives the only method of proving "existence-theorems": in order to prove such theorems, it is necessary (and sufficient) to find some instance in which an object possesses the property in question. If we were to assume what may be called "existence-axioms," i.e. axioms stating ( for some particular , these axioms would give other methods of proving existence. Instances of such axioms are the multiplicative axiom (*88) and the axiom of infinity (defined in *120·03). But we have not assumed any such axioms in the present work.

The second of the above primitive propositions is only used once, in proving (, which is the analogue of *1·2 (namely when is replaced by (. The effect of this primitive proposition is to emphasize the ambiguity of the required in order to secure (. We have, of course, in virtue of *9·1, But if we try to infer from these that , we must use the proposition , where is (. Now it will be found, on referring to *4·77 and the propositions used in its proof, that this proposition depends upon *1·2, i.e. . Hence it cannot be used by us to prove (, and thus we are compelled to assume the primitive proposition *9·11.

We have next two propositions concerned with inference to or from propositions containing apparent variables, as opposed to implication. First, we have, for the new meaning of implication resulting from the above definitions of negation and disjunction, the analogue of *1·1, namely

That is to say, given "" and "," we may proceed to "," even when the propositions and are not elementary. Also, as in *1·11, we may proceed from "" and "" to "" where is a real variable, and and are not necessarily elementary functions. It is in this latter form that the axiom is usually needed. It is to be assumed for functions of several variables as well as for functions of one variable.

We have next the primitive proposition which permits the passage from a real to an apparent variable, namely "when may be asserted, where may be any possible argument, then ( may be asserted." In other words, when is true however may be chosen among possible arguments, then ( is true, i.e. all values of are true. That is to say, if we can assert a wholly ambiguous value , that must be because all values are true. We may express this primitive proposition by the words: "What is true in any case, however the case may be selected, is true in all cases." We cannot symbolise this proposition, because if we put that means: "However may be chosen, implies (," which is in general false. What we mean is: "If is true however may be chosen, then ( is true." But we have not supplied a symbol for the mere hypothesis of what is asserted in "," where is a real variable, and it is not worth while to supply such a symbol, because it would be very rarely required. If, for the moment, we use the symbol to express this hypothesis, then our primitive proposition is In practice, this primitive proposition is only used for inference, not for implication; that is to say, when we actually have an assertion containing a real variable, it enables us to turn this real variable into an apparent variable by placing it in brackets immediately after the assertion-sign, followed by enough dots to reach to the end of the assertion. This process will be called "turning a real variable into an apparent variable." Thus we may assert our primitive proposition, for technical use, in the form:

*9·131.Definition of "being of the same type." The following is a step-by-step definition, the definition for higher types presupposing that for lower types. We say that and "are of the same type" if (1) both are individuals, (2) both are elementary functions taking arguments of the same type, (3) is a function and is its negation, (4) is or and is , where and are elementary functions, (5) is and is (, where , are of the same type, (6) both are elementary propositions, (7) is a proposition and is , or (8) is ( and is (, where and are of the same type.