Mathematical Logic as based on the Theory of TypesBY BERTRAND RUSSELL Published in: American Journal of Mathematics, vol.30(1908), pp. 222-262 Transcribed into hypertext by Burtzev B.I., Jul., 07, 2003 e-mail: bbi-math@narod.ru, site: http://bbi-math.narod.ru/ The Hierarchy of Types.CB.A type is defined as the range of significance of a propositional function, i.e., as the collection of arguments for which the said function has values. Whenever an apparent variable occurs in a proposition, the range of values of the apparent variable is a type, the type being fixed by the function of which Уall valuesФ are concerned. The division of objects into types is necessitated by the reflexive fallacies which otherwise arise. These fallacies, as we saw, are to be avoided by what may be called the Уvicious-circle principle;Ф i.e., Уno totality can contain members defined in terms of itself.Ф This principle, in our technical language, becomes: УWhatever contains an apparent variable must not be a possible value of that variable.Ф Thus whatever contains an apparent variable must be of a different type from the possible values of that variable;
we will say that it is of a higher type. Thus the apparent variables contained in an expression are what determines its type. This is the guiding principle in what follows.
CC.Propositions which contain apparent variables are generated from such as do not contain these apparent variables by processes of which one is always the process of generalization, i.e., the substitution of a variable for one of the terms of a proposition, and the assertion of the resulting function for all possible values of the variable. Hence a proposition is called a generalized proposition when it contains an apparent variable. A proposition containing no apparent variable we will call an elementary proposition. It is plain that a proposition containing an apparent variable presupposes others from which it can be obtained by generalization; hence all generalized propositions presuppose elementary propositions. In an elementary proposition we can distinguish one or more terms from one or more concepts; the terms are whatever can be regarded as the subject of the proposition, while the concepts are the predicates or relations asserted of these ^{18})individuals; these form the first or lowest type.CD.It is unnecessary, in practice, to know what objects belong to the lowest type, or even whether the lowest type of variable occurring in a given context is that of individuals or some other. For in practice only the relative types of variables are relevant; thus the lowest type occurring in a given context may be called that of individuals, so far as that context is concerned. It follows that the above account of individuals is not essential to the truth of what follows; all that is essential is the way in which other types are generated from individuals, however the type of individuals may be constituted.CE.By applying the process of generalization to individuals occurring in elementary propositions, we obtain new propositions. The legitimacy of this process requires only that no individuals should be propositions. That this is so, is to be secured by the meaning we give to the word individual. We may define an individual as something destitute of complexity ; it is then obviously not a proposition, since propositions are essentially complex. Hence in applying the process of generalization to individuals we run no risk of incurring reflexive fallacies.CF.Elementary propositions together with such as contain only individuals as apparent variables we will call first-order propositions. These form the second logical type.CG.We have thus a new totality, that of first-order propositions. We can thus form new propositions in which first-order propositions occur as apparent variables. These we will call second-order propositions; these form the third logical type. Thus, e.g., if Epimenides asserts Уall first-order propositions affirmed by me are false,Ф he asserts a second-order proposition; he may assert this truly, without asserting truly any first-order proposition, and thus no contradiction arises.CH.The above process can be continued indefinitely. The n + 1thn, which will be such as contain propositions of order n Ч 1,CI.In practice, a hierarchy of functions is more convenient than one of propositions. Functions of various orders may be obtained from propositions of various orders by the method of substitution. If p is a proposition, and a a constituent of p, let Уp/a^{;}xФ denote the proposition which results from substituting x for a wherever a occurs in p. Then p/a, which we will call a matrix, may take the place of a function; its value for the argument x is p/a^{;}x, and its value for the argument a is p. Similarly, if p/(a, b)^{;}(x, y)Фx for a and then substituting y for b, we may use the double matrix p/(a, b) to represent a double function. In this way we can avoid apparent variables other than individuals and propositions of various orders. The order of a matrix will be defined as being the order of the proposition in which the substitution is effected, which proposition we will call the prototype. The order of a matrix does not determine its type: in the first place because it does not determine the number of arguments for which others are to be substituted (i.e., whether the matrix is of the form p/a or p/(a,b) or p/(a,b,c) etc.); in the second place because, if the prototype is of more than the first order, the arguments may be either propositions or individuals. But it is plain that the type of a matrix is definable always by means of the hierarchy of propositions.CJ.Although it is possible to replace functions by matrices, and although this procedure introduces a certain simplicity into the explanation of types, it is technically inconvenient. Technically, it is convenient to replace the prototype p by φa, and to replace p/a^{;}x by φx; thus where, if matrices were being employed, p and a would appear as apparent variables, we now have φ as our apparent variable. In order that φ may be legitimate as an apparent variable, it is necessary that its values should be confined to propositions of some one type. Hence we proceed as follows.CK.A function whose argument is an individual and whose value is always a first-order proposition will be called a first-order function. A function involving a first-order function or proposition as apparent variable will be called a second-order function, and so on. A function of one variable which is of the order next above that of its argument will be called a predicative function; the same name will be given to a function of several variables if there is one among these variables in respect of which the function becomes predicative when values are assigned to all the other variables. Then the type of a function is determined by the type of its values and the number and type of its arguments.CL.The hierarchy of functions may be further explained as follows. A first-order function of an individual x will be denoted by φ!xψ, χ, θ, f, g, F, G will also be used for functions). No first-order function contains a function as apparent variable; hence such functions form a well-defined totality, and the φ in φ!xφ appears as apparent variable, and there is no apparent variable of higher type than φ, is a second-order proposition. If such a proposition contains an individual x, it is not a predicative function of x, but if it contains a first-order function φ, it is a predicative function of φ, and will be written f !( ψ ! z )^{^}f is a second-order predicative function; the possible values of f again form a well-defined totality, and we can turn f into an apparent variable. We can thus define third-order predicative functions, which will be such as have third-order propositions for their values and second-order predicative functions for their arguments. And in this way we can proceed indefinitely. A precisely similar development applies to functions of several variables.CM.We will adopt the following conventions. Variables of the lowest type occurring in any context will be denoted by small Latin letters (excluding f and g, which are reserved for functions); a predicative function of an argument x (where x may be of any type) will be denoted by φ!xψ, χ, θ, f, g, F or G may replace φ); similarly a predicative function of two arguments x and y will be denoted by φ!(x, y)x will be denoted by φx, and a general function of x and y by φ(x, y). In φx, φ can not be made into an apparent variable, since its type is indeterminate; but in φ!xφ is a predicative function whose argument is of some given type, φ can be made into an apparent variable.CN.It is important to observe that since there are various types of propositions and functions, and since generalization can only be applied within some one type, all phrases containing the words Уall propositionsФ or Уall functionsФ are prima facie meaningless, though in certain cases they are capable of an unobjectionable interpretation. The contradictions arise from the use of such phrases in cases where no innocent meaning can be found.CO.If we now revert to the contradictions, we see at once that some of them are solved by the theory of types. Wherever Уall propositionsФ are mentioned, we must substitute Уall propositions of order n,Ф where it is indifferent what value we give to n, but it is essential that n should have some value. Thus when a man says УI am lying,Ф we must interpret him as meaning: УThere is a proposition of order n, which I affirm, and which is false.Ф This is a proposition of order n + 1; hence the man is not affirming any proposition of order n; hence his statement is false, and yet its falsehood does not imply, as that of УI am lyingФ appeared to do, that he is making a true statement. This solves the liar.
CP.Consider next Уthe least integer not nameable in fewer than nineteen syllables.Ф It is to be observed, in the first place, that nameable must mean Уnameable by means of such-and-such assigned names,Ф and that the number of assigned names must be finite. For if it is not finite, there is no reason why there should be any integer not nameable in fewer than nineteen syllables, and the paradox collapses. We may next suppose that Уnameable in terms of names of the class NФ means Уbeing the only term satisfying some function composed wholly of names of the class N.Ф The solution of this paradox lies, I think in the simple observation that Уnameable in terms of names of the class NФ is never itself nameable in terms of names of that class. If we enlarge N by adding the name Уnameable in terms of names of the class NФ our fundamental apparatus of names is enlarged; calling the new apparatus N′N′ ФN′N till it embraces all names, УnameableФ becomes (by what was said above) Уbeing the only term satisfying some function composed wholly of names.Ф But here there is a function as apparent variable;
hence we are confined to predicative functions of some one type (for non-predicative functions can not be apparent variables). Hence we have only to observe that nameability in terms of such functions is non-predicative in order to escape the paradox.
CQ.The case of Уthe least indefinable ordinalФ is closely analogous to the case we have just discussed. Here, as before, УdefinableФ must be relative to some given apparatus of fundamental ideas; and there is reason to suppose that Уdefinable in terms of ideas of the class NФ is not definable in terms of ideas of the class N. It will be true that there is some definite segment of the series of ordinals consisting wholly of definable ordinals, and having the least indefinable ordinal as its limit. This least indefinable ordinal will be definable by a slight enlargement of our fundamental apparatus; but there will then be a new ordinal which will be the least that is indefinable with the new apparatus. If we enlarge our apparatus so as to include all possible ideas, there is no longer any reason to believe that there is any indefinable ordinal. The apparent force of the paradox lies largely, I think, in the supposition that if all the ordinals of a certain class are definable, the class must be definable, in which case its successor is of course also definable; but there is no reason for accepting this supposition.CR.The other contradictions, that of Burali-Forti in particular, require some further developments for their solution. |

Notes |