Esquema de reflexión sobre PA para el predicado de demostrabilidad de Rosser

Question

Tengo un par de preguntas sobre el esquema de reflexión en AP,

Supongamos que queremos considerar un esquema de reflexión desviado sobre PA formalizado por $Prov_{Ros-PA}(\varphi)\rightarrow \varphi$ donde $Prov_{ROS-PA}$ es un predicado de demostrabilidad de Rosser: $\exists x (Prf(x,\varphi)\wedge \forall z<x \neg Prf(z, \neg\varphi))$ donde Prf es la representación estándar de la relación de demostrabilidad.

1) ¿Es este esquema demostrable en PA? 2) Si no es así, ¿qué fuerza tiene PA + reflexión desviada? 3) ¿Existe algún vínculo entre la reflexión desviada y la reflexión regular? 4) ¿Se da el caso de que PA+ reflexión desviada para $\Pi_1$ -fórmulas demuestra Con(PA) (donde Con se formaliza utilizando el predicado de demostrabilidad estándar)?

Answer 1

1) No.

2) Su fuerza está entre PA y PA + el principio de reflexión local ordinario para PA, pero los detalles son sutiles. Véase, por ejemplo, S.V. Goryachev, Aritmética con un principio de reflexión local para fórmulas de demostrabilidad de Rosser Mat. Zametki, 46(3):12-21, 1989. En general, las propiedades del principio de reflexión desviada dependen de la elección de "la representación estándar" de la relación de demostrabilidad (por ejemplo, la numeración de Gödel).

3) PA + reflexión es deductivamente equivalente a PA + reflexión desviada si esta última teoría prueba Con(PA). Existen predicados de demostrabilidad estándar tales que el correspondiente principio de reflexión desviada tiene esta propiedad. Estos resultados se pueden encontrar en el artículo antes mencionado.

4) Que la situación es similar para $\Pi_1$ La reflexión ha sido demostrada por T. Kurahashi, Sentencias de Henkin y principios de reflexión local para la demostrabilidad de Rosser Annals of Pure and Applied Logic, 167(2):73-94, 2016. De nuevo, existen predicados de demostrabilidad estándar tales que el correspondiente $\Pi_1$ principio de reflexión desviada es equivalente al ordinario $\Pi_1$ y, por tanto, demuestran Con(PA) (Corolario 6.14).