Epsilon substitution for transfinite induction (Q1778059)

The systems \(\text{PA}+\text{TI}(\prec)\) of first-order arithmetic extended by a scheme of transfinite induction on a recursive well-ordering \(\prec\) (of the order type \(\alpha\)) are often used in proof theory. \textit{T. Arai} [``Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)'', Ann. Pure Appl. Logic 121, 163--208 (2003; Zbl 1022.03040)] outlined a schema of an \(\varepsilon\)-substitution method for such systems and of a termination proof using ordinary assignment by a method of W. Ackermann. The author provides a cross-check via a termination proof using cut elimination following \textit{G. Mints} [``Gentzen-type systems and Hilbert's epsilon substitution method. I'', in: D. Prawitz et al. (eds.), Logic, methodology and philosophy of science IX. Proceedings of the ninth international congress of logic, methodology and philosophy of science, Uppsala, Sweden, August 7--14, 1991. Amsterdam: North-Holland. Stud. Logic Found. Math. 134, 91--122 (1994; Zbl 0835.03023)]. The main new feature of the formulation by T. Arai is a possibility to assign an arbitrary value \(n\) satisfying \(\varphi[n]\) to an \(\varepsilon\)-term \(\varepsilon x\varphi[x]\), not necessarily the \(\prec\)-least \(n\), since the latter is non-computable in general. A correction step corresponding to a critical formula \(\varphi[m]\to\varphi[\varepsilon x\varphi[x]]\) may change such a value \(n\) to \(m\prec n\). The main new feature compared to the termination proof of Mints [loc. cit.] is the treatment of cuts corresponding to the alternative: either \((\varepsilon x\varphi[x],?)\) (that is, \(\forall x\neg \varphi[x]\) and \(\varepsilon x\varphi[x]\) has a default value 0) or (non-default) \(\varepsilon x\varphi[x]=n\) for some \(n\). Redexes corresponding to this cut are situated over an \((\varepsilon x\varphi[x],?)\)-premise and called \(H\)-axioms. An \(H\)-axiom \(A\times H_{\varepsilon x\varphi[x],n}\) corresponds to \(\varepsilon x\varphi[x]=n\). In the reviewer's paper [loc. cit.] a reduction of such a redex used only the premise of the cut corresponding to \(\varepsilon x \varphi[x]=n\). In the present treatment cut elimination in premises for many \(m\preceq n\) is used in a way corresponding to the quantifier \((\forall m\prec x)\) in the progressivity condition \(\forall x(\forall y\prec x\,\, Px\to Py)\). Otherwise the schema of a proof is the same as in the reviewer's paper [loc. cit.]. For a given finite system \(E\) of critical \(\varepsilon\)-formulas, an \(\omega\)-derivation is constructed, cut-elimination theorem is proved, and it is noted that a cut-free derivation is finite and encodes a terminating \(\varepsilon\)-substitution process.