 In order to be able to formulate Gentzen’s results from the end of section 3.3, we have to “arithmetize” the treatment of ordinals. Let us first state some precise definitions and a Cantorian theorem.