It appears from the above discussion that the variable is a very complicated logical entity, by no means easy to analyze correctly. The following appears to be as nearly correct as any analysis I can make. Given any proposition (not a propositional function), let `a` be one of its terms, and let us call the proposition `ϕ`(`a`). Then in virtue of the primitive idea of a propositional function, if `x` be any term, we can consider the proposition `ϕ`(`x`), which arises from the substitution of `x` in place of `a`. We thus arrive at the class of all propositions `ϕ`(`x`). If all are true, `ϕ`(`x`) is asserted simply: `ϕ`(`x`) may then be called a *formal* truth. In a formal implication, `ϕ`(`x`), *for every value of *`x`, states an implication, and the assertion of `ϕ`(`x`) is the assertion of a *class* of implications, not of a single implication. If `ϕ`(`x`) is sometimes true, the values of `x` which make it true form a class, which is the class defined by `ϕ`(`x`): the class is said to *exist* in this case. If `ϕ`(`x`) is false for all values of `x`, the class defined by `ϕ`(`x`) is said not to exist, and as a matter of fact, as we saw in Chapter VI, there is no such class, if classes are taken in extension. Thus `x` is, in some sense, the object denoted by *any term*; yet this can hardly be strictly maintained, for different variables may occur in a proposition, yet the object denoted by *any term*, one would suppose, is unique. This, however, elicits a new point in the theory of denoting, namely that *any term* does not denote, properly speaking, an assemblage of terms, but denotes one term, only not one particular definite term. Thus *any term* may denote different terms in different places. We may say: any term has some relation to any term; and this is quite a different proposition from: any term has some relation to itself. Thus variables have a kind of individuality. This arises, as I have tried to show, from propositional functions. When a propositional function has two variables, it must be regarded as obtained by successive steps. If the propositional function `ϕ`(`x`, `y`) is to be asserted for all values of `x` and `y`, we must consider the assertion, for all values of `y`, of the propositional function `ϕ`(`a`, `y`), where `a` is a constant. This does not involve `y`, and may be represented by `ψ`(`a`). We, then, vary `a`, and assert `ψ`(`x`) for all values of `x`. The process is analogous to double integration; and it is necessary to prove formally that the order in which the variations are made makes no difference to the result. The individuality of variables appears to be thus explained. A variable is not *any term* simply, but any term as entering into a propositional function. We may say, if `ϕ``x` be a propositional function, that `x` is *the* term in *any* proposition of the class of propositions whose type is `ϕ``x`. It thus appears that, as regards propositional functions, the notions of class, of denoting, and of *any*, are fundamental, being presupposed in the symbolism employed. With this conclusion, the analysis of formal implication, which has been one of the principal problems of Part I, is carried as far as I am able to carry it. May some reader succeed in rendering it more complete, and in answering the many questions which I have had to leave unanswered.(§ 93 ¶ 1)