Ideas in the epsilon substitution method for \(\Pi_{1}^{0}\)-FIX (Q2566062)

In this article, the author first revisits the epsilon substitution, which is an alternative approach to the use of cut elimination in ordinal analysis. It was originally proposed by Hilbert, and a termination proof for Peano arithmetic was given by \textit{W. Ackermann} [``Zur Widerspruchsfreiheit der Zahlentheorie'', Math. Ann. 117, 162--194 (1940; Zbl 0022.29202)]. That proof made use of transfinite induction up to \(\epsilon_0\). The author carries out this proof using a modern formalisation with some improvements, including a reformulation of the theory which avoids the need for linearity of the ordering of the data types used.\ Then the author extends this approach to the theory of \(\Pi^0_1\)-FIX of nonmonotonic \(\Pi^0_1\)-inductive definitions, using transfinite induction up to the Bachmann-Howard ordinal. First this theory is formalised in a quantifier-free way using the \(\epsilon\)-operator. Then the operations from Ackermann's proof are extended to this setting. There are now two different steps when generating substitutions in the H-process of the \(\epsilon\)-substitution method: one is the same as before and the other is the \(\Pi\)-step. The \(\Pi\)-step corresponds to the application of collapsing when analysing corresponding theories using cut elimination. The termination proof follows a similar approach as the one taken by Ackermann in assigning ordinals to sequences of substitutions. The complication is that in a sequence one starts with a rank \(< \Omega\) but has in between substitutions of rank \(\geq \Omega\), which need to be collapsed down to ordinals \(< \Omega\). The author makes in this article an attempt to not only carry out the formal details but to explain the ideas of his approach. The explanations include two diagrams which are very helpful in order to understand the argument.