Reflection schema over PA for Rosser provability predicate

167 Views Asked by At

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)?