Reduction of higher type levels by means of an ordinal analysis of finite terms (Q759749)

The main contribution of this paper is a new method to obtain assignments of ordinals to all finite terms (in extensions of Gödel's T by transfinite recursion) with the property that successors of a term (in the style of Sanchis) always get smaller ordinals. Although the author states on p. 2 that his work has been strongly inspired by Howard's approach [\textit{W. A. Howard}, J. Symb. Logic 45, 493-504 (1980; Zbl 0444.03029)], in my opinion he really has achieved something new, which is technically highly non-trivial. The usefulness of the result is documented by just one application (elimination of higher type levels) but it seems likely that further applications of his method can be found. The only criticism I have is that the author's approach is rather formal when compared with Howard's. Howard has succeeded to combine the intuitive clarity of Tait's analysis using infinite terms, where the associated ordinal is just the length of the term, with the simplicity of a system of finite terms. In Howard's paper the fact that reducing the degree of a term by one corresponds to raising its ordinal \(\alpha\) to \(\omega^{\alpha}\) is clearly explained by an analysis, where finite sequences of certain subterms come up naturally. In the paper under review I could not find an equally convincing explanation of this phenomenon. Technically, the paper is written very carefully and all proofs I have checked are given with just the right amount of detail.