Two measures for proving Gentzen's Hauptsatz without mix (Q1407599)

The paper under review continues the investigations of two earlier papers which are concerned with the proof of Gentzen's Hauptsatz without using the mix rule, as Gentzen did, but only the cut rule. While in Ann. Pure Appl. Logic 99, 105-136 (1999; Zbl 0933.03074) the author considered intuitionistic predicate logic, the author, \textit{K. Došen} and \textit{Z. Petrić} introduced in Math. Struct. Comput. Sci. 10, 99-136 (2000; Zbl 0949.03054) besides the degree of a derivation a new definition of the rank of a derivation and treated intuitionistic propositional logic by nested recursion on degree and rank. In the present paper, this method is applied to classical and intuitionistic predicate logic and compared with the procedure of \textit{J. von Plato} [Arch. Math. Logic 40, 9-18 (2001; Zbl 0968.03065)], who defines the concept of height instead of rank.