Slow reflection (Q2407272)

Slow reflection is based on the notion of a slow \(\mathrm{PA}\)-proof. The function \(F_{\alpha}(x)\) for \(\alpha\leq\varepsilon_0\) is defined as follows: \(F_0(x)=x+1\), \(F_{\alpha+1}(x)=F_{\alpha}^{x+1}(x)\), \(F_{\lambda}(x)=F_{\{\lambda\}(x)}(x)\) for a limit \(\lambda\). A slow \(\mathrm{PA}\)-proof of a formula \(\varphi\) is a pair \(\langle q,F_{\varepsilon_0}(n)\rangle\) such that \(q\) is a usual proof of \(\varphi\) in the fragment \(\mathrm{I}\Sigma_{n+1}\) of Peano arithmetic. The predicate ``\(p\) is a slow proof of \(\varphi\)'' is defined by a \(\Delta_1\)-formula \(\text{Proof}^{\diamond}_{\mathrm{PA}}(p,\varphi)\) in \(\mathrm{I}\Sigma_1\). Then, \(\text{Pr}^{\diamond}_{\mathrm{PA}}(\varphi)\) is \(\exists p\,\text{Proof}^{\diamond}_{\mathrm{PA}}(p,\varphi)\). The slow reflection principle \(\text{RFN}^{\diamond}_{\mathrm{PA}}(\varphi)\) is the formula \(\forall x_1,\ldots,x_k\,(\text{Pr}^{\diamond}_{\mathrm{PA}}(\varphi(\dot x_1,\ldots,\dot x_k))\to\varphi(x_1,\ldots,x_k))\). Then, \(\text{RFN}^{\diamond}_{\mathrm{PA}}\) is defined as the set of the formulas \(\text{RFN}^{\diamond}_{\mathrm{PA}}(\varphi)\) for all first-order arithmetical formulas \(\varphi\). The connection between slow reflection and transfinite induction is studied. The central result of the paper (Theorem 2.18) states that the consistency of \(\mathrm{PA}+\text{RFN}^{\diamond}_{\mathbf{PA}}\) is provable in \(\mathrm{PA}+\text{Con}(\mathrm{PA})\). Slow consistency \(\text{Con}^{\diamond}(\mathrm{PA}+\varphi)\) for finite extensions of \(\mathrm{PA}\) introduced in [\textit{S.-D. Friedman} et al., Ann. Pure Appl. Logic 164, No. 3, 382--393 (2013; Zbl 1263.03055)] is defined as \(\forall x\,(F_{\varepsilon_0}(x)\downarrow\to\text{Con}(\mathrm{I}\Sigma_{x+1}+\varphi))\). Iterated slow consistency is a \(\Pi_1\)-formula \(\text{Con}^{\diamond}_{\alpha}(\mathrm{PA})\) with a parameter \(\alpha\) obtained with the help of the fixed point theorem and such that \(\mathrm{I}\Sigma_1\vdash\text{Con}^{\diamond}_{\alpha}(\mathrm{PA})\leftrightarrow(\forall\beta<\alpha)\,\text{Con}^{\diamond}(\mathrm{PA}+ \text{Con}^{\diamond}_{\dot\beta}(\mathrm{PA}))\). It is proved (Theorem 3.4) that \(\mathrm{PA}+\text{Con}(\mathrm{PA})\vdash(\forall\alpha<\varepsilon_0)\,\text{Con}(\mathrm{PA}+\text{Con}^{\diamond}_{\alpha}(\mathrm{PA}))\). This implies \(\mathrm{PA}+\text{Con}(\mathrm{PA})\vdash\text{Con}^{\diamond}_{\varepsilon_0}(\mathrm{PA})\). The proof uses slow reflection for \(\Sigma_1\)-formulas. The results of the paper show the conjecture of Friedmann et al. [loc. cit.] that transfinite iterations of slow consistency generate a hierarchy of precisely \(\varepsilon_0\) stages between \(\mathrm{PA}\) and \(\mathrm{PA}+\text{Con}(\mathrm{PA})\).