Induktive Definitionen und Dilatoren

Summary In this paper we give a new and comparatively simple proof of the following theorem by Girard 1]:If x y (x,y) (where the relation is arithmetic and positive in Kleene's ), then there exists a recursive DilatorD such that x ^<y ⁾ (x, y).The essential feature of our proof is its very direct definition of the dilatorD. Within a certain infinitary cutfree system of inductive logic (which in fact is a modification of Girard's system in 1]) we construct in a uniform way for each ordinal a derivation T of the formula x ^<y (x, y), and then defineD immediately from the family (T)_On. Especially we set D():=Kleene-Brouwer length of (T).