A two-storied universe of transfinite mechanisms (Q1121881)

In an earlier paper [Comment. Math. Univ. St. Pauli 35, 1-38 (1986; Zbl 0633.03053)] the author introduced a very general theory of types, in which the types may contain free variables, for which terms of the language L can be substituted. In the language L it is possible to speak about ordinal diagrams and functions of ordinal diagrams. Terms of those types are called methods resp. hypermethods, the theory is called HP, the theory of the hyper-principle. In the paper under review, an extension of this theory HP is presented. Now it is allowed to substitute free variables in types by terms which contain free variables themselves. Thus a hierarchy of three kinds of objects is created: The function variables constitute the lowest level, the basement. The terms of HP are the first floor, the terms with variables for terms of HP to be substituted in types are the second floor. The formal system on this hierarchy of types and terms with a principle of continuity and an interpretation is called the hyper-principle for the two-storied universe of transfinite mechanisms, TM[2]. Transfinitely often iterated inductive definitions, which are used in well-ordering proofs for ordinal notation systems, can be expressed in this system. There are certainly analogies to other systems of generalized inductive definitions, but they are far from being obvious.