A proof of strongly uniform termination for Gödel's \(T\) by methods from local predicativity (Q1374676): Difference between revisions

After reviewing the historical development of the subject, the author reconsiders the Howard-Schütte assignment of finite sequences of ordinals to terms in Gödel's \(T\). In its original form, this method yields decreasing ordinals only when the conversion \(I(t+1)ab \mapsto a(Itab)\) is restricted to numerals \(t\). This restriction is overcome by using an `essentially less than' relation \(\ll\) and a collapsing function \({\mathcal D}\) (as in the paper of \textit{W. Buchholz, A. Cichon} and \textit{A. Weiermann} [``A uniform approach to fundamental sequences and hierarchies'', Math. Log. Q. 40, 273-286 (1994; Zbl 0812.03023)]) such that \(a\) reduces to \(b\) implies that \([b]_0 \ll [a]_0\) and hence \({\mathcal D}(b) < {\mathcal D}(a)\). The collapse can be thought of as providing time to wait until the numerical argument \(t\) of the iterator \(Itab\) is reduced to a numeral. For simplicity of presentation the author has chosen a form of \(T\) with combinators and iterators. A treatment allowing for arbitrary typed \(\lambda\)-terms and the recursor is promised for a subsequent paper. The paper also sketches -- as the author puts it -- an `affirmative contribution' to a problem of Girard, who had assigned an ordinal \(|t|\) less than the Bachmann-Howard ordinal to every term \(t\) of \(T\) and asked `what is the relation of the ordinals \(|t|\) to the structure of computation of \(t\)?' Moreover, the author conjectures that the method of the present paper can be applied to general investigations on proving termination for higher order rewrite systems by using ordinal notations, referring to a paper of \textit{J. van de Pol} and \textit{H. Schwichtenberg} [``Strict functionals for termination proofs'', in: M. Dezani-Ciancaglini and G. Plotkin (editors), Typed Lambda Calculi and Applications, Lect. Notes Comput. Sci. 902, 350-364 (1995)] for related work.