NORMALIZATION FOR ARITHMETICAL COMPREHENSION WITH RESTRICTED OCCURRENCES OF HILBERT’S EPSILON-SYMBOL
Sergei Tupailo · Proceedings of the Estonian Academy of Sciences Physics Mathematics · 1993
We present a normalization proof for the second order arithmetic with arithmetical comprehension and Hilbert's epsilon-axiom F[T]-F[eXFX] which repre- sents a kind of choice principle.The proof is carried out by transfinite induction ир 10 .