3
$\begingroup$

I have a couple of questions concerning the reflection schema over PA,

Suppose that we want to consider a deviant reflection schema over PA formalized by $Prov_{Ros-PA}(\varphi)\rightarrow \varphi$, where $Prov_{ROS-PA}$ is a Rosser provability predicate: $\exists x (Prf(x,\varphi)\wedge \forall z<x \neg Prf(z, \neg\varphi))$, where Prf is the standard representation of provability relation.

1) Is this schema provable in PA? 2) If not, how strong is PA + deviant reflection? 3) Is there any link between deviant reflection and the regular reflection? 4) Is it the case that PA+ deviant reflection for $\Pi_1$-formulas proves Con(PA) (where Con is formalized using the standard provability predicate)?

$\endgroup$
1
$\begingroup$

1) No.

2) Its strength is between PA and PA + the ordinary local reflection principle for PA, but the details are subtle. See, e.g., S.V. Goryachev, Arithmetic with a local reflection principle for Rosser provability formulas, Mat. Zametki, 46(3):12-21, 1989. In general, the properties of the deviant reflection principle depends on the choice of "the standard representation" of the provability relation (e.g. Gödel numbering).

3) PA + reflection is deductively equivalent to PA + deviant reflection iff the latter theory proves Con(PA). There are standard provability predicates such that the corresponding deviant reflection principle has this property. These results can be found in the aforementioned paper.

4) That the situation is similar for $\Pi_1$ reflection has been shown by T. Kurahashi, Henkin sentences and local reflection principles for Rosser provability, Annals of Pure and Applied Logic, 167(2):73-94, 2016. Again, there are standard provability predicates such that the corresponding $\Pi_1$ deviant reflection principle is equivalent to ordinary $\Pi_1$ reflection, and these therefore prove Con(PA) (Corollary 6.14).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.