An intuitionistic fixed point theory (Q1386672)

In the paper under review the author shows that the theory \(\widehat{ID} ^i_1\) is conservative over Heyting Arithmetic, \(HA\), w.r.t. almost negative formulas. \(\widehat{ID}^i_1\) is the extension of \(HA\) obtained by adding new predicate constants \(P_\Phi\) for every strongly positive formula \(\Phi (X,x)\) containing just free the individual variable \(x\) and the unary predicate variable \(X\), and the new axioms \((FP_\Phi)\) \(\forall x(\Phi(P_\Phi, x) \leftrightarrow P_\Phi x).\) Almost negative formulas (of the language \({\mathcal L}_0\) of number theory with function symbols for all recursive functions) do not contain \(\vee\) and contain \(\exists\) only for equations between terms [cf. \textit{A. S. Troelstra}, Metamathematical investigation of intuitionistic arithmetic and analysis (Lect. Notes Math. 344) (1973; Zbl 0275.02025), 3.2.9]. Strongly positive formulas are built up by atomic formulas of \({\mathcal L}_0\) and the unary predicate symbol \(P\) using the logical symbols \(\wedge, \vee, \exists, \forall.\) In \S 1, Theorem 1 is proved, namely that in \(HA + CT_0\) \((FP_\Phi)\) is provable, \(CT_0\) being Church's thesis (cf. Troelstra (loc. cit.)). As was shown in the introduction, Theorem 1 and material from Troelstra (loc. cit.) give Theorem 2, the above conservativity result. But this is not the whole story. The author assures that Theorem 2 can be generalized to: Theorem \(2'\). If \(\prec\) is a primitive recursive binary relation and \(TI (\prec \upharpoonright)\) the schema of transfinite induction over all proper initial segments of \(\prec\), then \(\widehat{ID}^i_1+TI(\prec \upharpoonright)\) is conservative over \(HA + TI(\prec \upharpoonright)\) w.r.t. almost negative formulas. This has interesting consequences for proof theory. Cut elimination and thus ordinal analysis of a semi-formal theory \(Th\) (also classical) can be formalized in \(\widehat{ID}^i_1+TI(\prec \upharpoonright).\) The definition of a derivability predicate \(\vdash ^\alpha_\varrho F\) can be considered a fixpoint axiom in this theory. This amounts to \[ \widehat{ID}^i_1 +TI (\prec \upharpoonright)\vdash P_\omega \langle \underline{\alpha},\ulcorner A \urcorner \rangle \] for any arithmetical sentence \(A\) with Gödel number \(\ulcorner A \urcorner\) derivable in \(Th\), \(P_\omega\) denoting the fixpoint constant of \(\widehat{ID}^i_1\) related to cut-free derivation, and \(\underline{\alpha}\) a notation of the element \(\alpha\) of \(Fd (\prec)\) for which \(\vdash ^\alpha_0 A\) holds. In \S 2 the author shows that for every arithmetical sentence \(A\) and every \[ \alpha\in Fd (\prec) \widehat{ID}^i_1 + TI (\prec \upharpoonright) \vdash P_\omega \langle \underline{\alpha}, \ulcorner A \urcorner \rangle \Rightarrow A^g, \] \(A^g\) being the Gödel translation of \(A\). It comes into play by introducing a truth-predicate \(\mathbf T_n(z)\), for which \(HA \vdash A^g \leftrightarrow {\mathbf T}_n (\ulcorner A \urcorner)\), if \(rk(A) \leq n.\) (1) and (2) implies \(\widehat{ID}^i_1 + TI (\prec \upharpoonright) \vdash A^g.\) Since \(A^g\) is almost negative, this implies \(PA + TI(\prec \upharpoonright) \vdash A.\) T. Arai showed that Theorem 2 can be proved for arbitrary index \(n\) instead of index 1. The paper contains everything necessary for understanding the procedure in the proofs.