 All this led Russell to develop the simple and the ramified theory of types, in which syntactical restrictions were built in that make impredicative definitions ill-formed. In simple type theory, the free variables in defining formulas range over entities to which the collection to be defined do not belong. In ramified type theory, it is required in addition that the range of the bound variables in defining formulas do not include the collection to be defined. It was pointed out in  section 2.1  that Russell’s type theory cannot be seen as a reduction of mathematics to logic. But even aside from that, it was observed early on that especially in ramified type theory it is too cumbersome to formalize ordinary mathematical arguments.