A termination proof for epsilon substitution using partial derivations (Q1401363): Difference between revisions

The epsilon substitution method that was carried out by \textit{W. Ackermann} [Math. Ann. 117, 162-194 (1940; Zbl 0022.29202)] has two components: (1) the description of the \(H\)-process, and (2) a proof that shows the process terminates in a finite number of steps, in success (i.e. all \(\varepsilon\)-terms in question are evaluated correctly). The author (and others) has been addressing (2) for the past ten years or so. He sets up an infinitary system, INF, that formulates the \(H\)-process, and a finitary, FIN, whose derivations are ``notations'' of those in INF. \{`INF' and `FIN' are particular to this review. They are labelled `\(\varepsilon\)PA' and `PA\(\varepsilon^*\)' in the paper.\} The successive stages of the \(H\)-process are reflected in the cut-elimination procedure of INF, and that is, in turn, reflected in FIN. The author assigns ordinal numbers to FIN derivations, and shows that they decrease by the procedure in INF. And, thus, the \(H\)-process terminates in a finite number of steps. In this paper, the author uses a new device: for an \(\varepsilon\)-term \(e\), \((e,+)\) indicates that the value of \(e\) is defined but unknown. So derivations are only partial. Despite the new device, quite a few definitions and notations are involved, due to the nature of the subject. Although the author considers first-order arithmetic in this paper, his aim in this formalized approach is its potential application to other systems. Indeed, he and others worked out second-order arithmetic with arithmetical comprehensions, a few years ago [\textit{G. Mints}, \textit{S. Tupailo} and \textit{W. Buchholz}, Arch. Math. Logic 35, 103-130 (1996; Zbl 0848.03032)].