Epsilon substitution method for \([\Pi^0_1,\Pi^0_1]\)-FIX (Q2576640)

In this article, the epsilon substitution method is applied to the theory \([\Pi^0_1,\Pi^0_1]\)-FIX. A \([\Pi^0_1,\Pi^0_1]\)-operator is an operator of the form \(\Gamma[X,n]:\equiv \Gamma_0[X,n] \lor (\Gamma_0[X] \subseteq X \land \Gamma_1[X,n])\), where \(\Gamma_i[X,n]\) are \(\Pi^0_1\)-formulas. \([\Pi^0_1,\Pi^0_1]\)-FIX has two sorts: the sort of natural numbers and a sort of ordinals. \([\Pi^0_1,\Pi^0_1]\)-FIX is the theory claiming the existence of a fixed point for a (possibly nonmonotonic) \([\Pi^0_1,\Pi^0_1]\)-operator, which is obtained by iterating this operator along the sort of ordinals. The proof-theoretic strength of this theory is KPM, i.e. Kripke-Platek set theory plus the existence of one recursively Mahlo ordinal. The method used is an extension of that used in [\textit{T. Arai}, ``Epsilon substitution method for \(\roman{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)'', Ann. Pure Appl. Logic 121, No. 2--3, 163--208 (2003; Zbl 1022.03040), and ``Ideas in the epsilon substitution method for \(\Pi_{1}^{0}\)-FIX'', Ann. Pure Appl. Logic 136, No. 1--2, 3--21 (2005; Zbl 1116.03051), reviewed below]. In this article, after introducing this theory and the ordinal notation system used, the theory is translated into a quantifier-free theory in the epsilon-substitution calculus. Then the H-process is adapted to this theory. There are now three different steps. One corresponds to the steps taken by \textit{W. Ackermann} [``Zur Widerspruchsfreiheit der Zahlentheorie'', Math. Ann. 117, 162--194 (1940; Zbl 0022.29202)] in his analysis of Peano arithmetic using the epsilon-substitution method. One is the closure of the nonmonotone inductive definition under \(\Gamma_0\), which corresponds to the \(\Pi\)-step in [loc. cit. (2005)]. And the last one is the closure under \(\Gamma_1\), provided the iteration of the operator is already closed under \(\Gamma_0\). Finally, termination is shown using a similar (but technically much more complicated) approach as in the previous articles mentioned. The article is well written and all details are worked out.