Slow reflection

DOI10.1016/J.APAL.2017.06.003MaRDI QIDQ2407272zbMATH OpenOpenAlexDBLPWikidataFDO

Publication date 29 September 2017

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1601.08214

consistency strength fast growing hierarchy iterated consistency Peano arithmetic slow consistency slow reflection

Models of arithmetic and set theory (03C62) Recursive functions and relations, subrecursive hierarchies (03D20) Relative consistency and interpretations (03F25) First-order arithmetic and fragments (03F30)

Abstract: We describe a "slow" version of the hierarchy of uniform reflection principles over Peano Arithmetic (

m a t h b f P A

). These principles are unprovable in Peano Arithmetic (even when extended by usual reflection principles of lower complexity) and introduce a new provably total function. At the same time the consistency of

m a t h b f P A

plus slow reflection is provable in

m a t h b f P A + o p e r a t o r n a m e C o n (m a t h b f P A)

. We deduce a conjecture of S.-D. Friedman, Rathjen and Weiermann: Transfinite iterations of slow consistency generate a hierarchy of precisely

v a r e p s i l o n_{0}

stages between

m a t h b f P A

and

m a t h b f P A + o p e r a t o r n a m e C o n (m a t h b f P A)

(where

o p e r a t o r n a m e C o n (m a t h b f P A)

refers to the usual consistency statement).

Review text

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})\).

Recommendations

Cites work

Cited in

(6)

This page was built for publication: Slow reflection

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2407272)