Level restrictions

[104] observed that it is not possible to regard the collection of all types as a type itself. Let Type be this collection of all types. So Type is not an element of Type. Russell suggested schemes for layering or stratifyingstratification these ``inexhaustible concepts'' like Type or Proposition or Set. The idea is to introduce notions of types of various levels. In our theory these levels are indicated by level indexes such as Type_i. They will be defined later.