On provably recursive functions and ordinal recursive functions*
Akiko Kino · Journal of the Mathematical Society of Japan · 1968
precise definition, cf.$[8a]$ and \S 2.)In [11], Takeuti defined $GLC$, a Gentzen-style simple type theory contain- ing t-variables of the first order and $f$ -variables with finitely many argument- places and stated his fundamental conjecture (FC) about $GLC$ ; (that Gentzen's Hauptsatz for $LK$, that is the cut elimination theorem, holds in $GLC$ as well.)Takeuti proved that FC holds for many subsystems of $GLC$ by using transfinite