We may now return to the apparent definability of any, some, and a, in terms of formal implication. Let a and b be class-concepts, and consider the proposition any a is a b. This is to be interpreted as meaning x is an a implies x is a b. It is plain that, to begin with, the two propositions do not mean the same thing: for any a is a concept denoting only a's, whereas in the formal implication x need not be an a. But we might, in Mathematics, dispense altogether with any a is a b, and content ourselves with the formal implication: this is, in fact, symbolically the best course. The question to be examined, therefore, is: How far, if at all, do any and some and a enter into the formal implication? (The fact that the indefinite article appears in x is an a and x is a b is irrelevant, for these are merely taken as typical propositional functions.) We have, to begin with, a class of true propositions, each asserting of some constant term that if it is an a it is a b. We then consider the restricted variable, any proposition of this class. We assert the truth of any term included among the values of this restricted variable. But in order to obtain the suggested formula, it is necessary to transfer the variability from the proposition as a whole to its variable term. In this way we obtain x is an a implies x is a b. But the genesis remains essential, for we are not here expressing a relation of two propositional functions x is an a and x is a b. If this were expressed, we should not require the same x both times. Only one propositional function is involved, namely the whole formula. Each proposition of the class expresses a relation of one term of the propositional function x is an a to one of x is a b; and we say, if we choose, that the whole formula expresses a relation of any term of x is an a to some term of x is a b. We do not so much have an implication containing a variable as a variable implication. Or again, we may say that the first x is any term, but the second is some term, namely the first x. We have a class of implications not containing variables, and we consider any member of this class. If any member is true, the fact is indicated by introducing a typical implication containing a variable. This typical implication is what is called a formal implication: it is any member of a class of material implications. Thus it would seem that any is presupposed in mathematical formalism, but that some and a may be legitimately replaced by their equivalents in terms of formal implications.(§ 89 ¶ 1)