Proof-theoretic analysis of termination proofs (Q1899143): Difference between revisions

\textit{E. A. Cichoń} [in: Proof theory, Int. Summer School and Conf., Leeds, UK, 1990, 173-193 (1992; Zbl 0793.03057)] raised the question whether there is a relation between the order type of a termination ordering \(\prec\) and the lengths of reduction sequences in a rewrite system reducing under \(\prec\). \textit{D. Hofbauer} [Theor. Comput. Sci. 105, No. 1, 129-140 (1992; Zbl 0759.68045)] gave an answer to this question in case that \(\prec\) is a multiset path ordering, \textit{A. Weiermann} [ibid. 139, 355-362 (1995)] settled the problem for \(\prec\) being a lexicographic path ordering. In both papers, the procedure is rather tedious. In the paper under review, the author gives an elegant solution for both kinds of termination orderings using proof-theoretical means. He first proves the well-foundedness of the lexicographic path ordering \(\langle T, \prec\rangle\) considering the accessible part \(W\) of \(\langle T, \prec\rangle\) and showing that \(W= T\). The crucial observation of the author is the following: For proving termination of a single finite rewrite system using lexicographical path ordering one does not need the full relation \(\prec\) but only a suitable subset \(\prec_k\) of it, for some \(k\in \mathbb{N}\) (Lemma 7). He defines for every \(k\) such a relation \(\prec_k \subset \prec\) and proves that it is well-founded following the lines of the proof for \(\langle T, \prec\rangle\). In this proof, the accessible part of \(T\) w.r.t. \(\prec_k\) is already defined by a \(\Sigma_1^0\)-formula. Thus the proof of well-foundedness of \(\prec_k\) can be carried through in \(\Pi_2^0\)-IA, i.e. \(\Pi_2^0\)-IA \(\lvdash\forall t\) \(t\in W_k\) holds, and therefore, by a result \textit{Ch. Parsons} communicated in Notices AMS 13 (1966), there is some \(\alpha\prec \omega^\omega\) such that the length of every \(\prec_k\)-decreasing sequence of elements of \(W_k\) starting with \(t\) is bounded by \(F_\alpha(t)\), \(F_\alpha\) being a function of the fast-growing hierarchy. In the last section, the author indicates how the proof for lexicographic path orderings can be modified to a proof of the corresponding result for recursive path orderings. The paper is a highly sophisticated application of proof theoretic means in the sense of analyzing the structure of proofs.