In this paper we treat the ramified type theory of Russell [6], afterwards adopted by Whitehead and Russell in Principia mathematica [12], so that we may compare Russell's resolution of the semantical antinomies by ramified type theory with the now widely accepted resolution of them by the method of Tarski in [7], [8], [9].

To avoid impredicativity the essential restriction is that quantification over any domain (type) must not be allowed to add new members to the domain, as it is held that adding new members changes the meaning of quantification over the domain in such a way that a vicious circle results. As Whitehead and Russell point out, there is no one particular form of the doctrine of types that is indispensable to accomplishing this restriction, and they have themselves offered two different versions of the ramified hierarchy in the first edition of Principia (see Preface, p. vii). The version in §§58–59 of the writer's [1], which will be followed in this paper, is still slightly different.

To distinguish Russellian types or types in the sense of the ramified hierarchy from types in the sense of the simple theory of types, let us call the former r-types.

There is an r-type i to which the individual variables belong. If β1, β2, …, βm are any given r-types, m ≧ 0, there is an r-type (β1, β2, …, βm)/n to which there belong m-ary functional variables of level n, n ≧ 1. The r-type (α1, α2, …, αm)/k is said to be directly lower than the r-type (β1, β2, …, βm)/n if α1 = β1, α2 = β2, …, αm = βm, k < n.