A cut-elimination proof in intuitionistic predicate logic (Q1304543)

\textit{G. Gentzen} proved in ``Untersuchungen über das logische Schließen. I, II'' [Math. Z. 39, 176-210, 405-431 (1934; Zbl 0010.14501, Zbl 0010.14601)] the cut elimination theorem using the mix rule instead of the cut rule, because the proof for the system with cut rule fails in the presence of the contraction rule. Later on \textit{M. E. Szabo} [Algebra of proofs (North Holland, Amsterdam) (1978; Zbl 0532.03030)] gave a direct proof of the cut elimination theorem, since in the setting of the categorical approach to his logical system he could not formulate the mix rule. Besides the parameters rank and degree he introduced a third one, the weighted rank of a derivation. The author shows in Section 3 by an example that the reduction tree of a derivation is not necessarily founded when using weighted rank and degree only. In comparing sequent calculi and systems of natural deduction, \textit{J. Zucker} [Ann. Math. Logic 7, 1-112, 113-115, 156 (1974; Zbl 0298.02023)] associated so-called indices as weights to the occurrences of formulae, not to the complete derivation. The author performs this idea and succeeds in giving a proof of the cut elimination theorem for a sequent calculus with cut rule and contraction rule. The paper is a contribution to linear logic in so far as it deals with the presence and absence, respectively, of certain structural rules. In the investigations of proof search in computer science, the weight of occurences of the cut rule is also used, for instance in the work of R. Dyckhoff and L. Pinto.