¿Cuál es el estatus lógico de la frase que combina las ideas de Löb y Rosser, "esta frase es demostrable antes de cualquier prueba de su negación"?

Question

Los lógicos están familiarizados con la variedad de oraciones autorreferenciales expresables en el lenguaje de la aritmética:

• El Gödel frase, "esta frase no es demostrable", que de hecho no es demostrable en cualquier teoría base que se haya utilizado al formularla y, por tanto, es verdadera pero no demostrable.

• El Rosser La frase "para cualquier prueba de esta frase hay una prueba menor de su negación", que también es verdadera e indemostrable. Esta sentencia ofrece una mejora técnica con respecto a la sentencia de Gödel en el sentido de que la independencia de la sentencia de Rosser puede demostrarse asumiendo únicamente la consistencia de la teoría base, mientras que Gödel ha utilizado $\omega$ -Consistencia.

• El Löb La frase "esta frase es demostrable" es efectivamente demostrable, notablemente, por Teorema de Löb .

Mi pregunta es sobre la frase que podríamos formar combinando las ideas de Rosser y Löb. A saber, por los métodos habituales de punto fijo, podemos formar una sentencia $\zeta$ que PA afirma de forma demostrable:

$\qquad$ " $\zeta$ es demostrable en PA mediante una prueba que es más pequeña que cualquier prueba de $\neg\zeta$ ."

Aquí nos referimos a "menor", al igual que con la sentencia Rosser, en el sentido de los códigos Gödel de la prueba.

Pregunta. ¿Cuál es el estado lógico de la sentencia combinada Rosser-Löb $\zeta$ ? ¿Es demostrable, independiente o qué?

Los argumentos habituales a favor de las sentencias Rosser y Löb no parecen tener ningún peso en la sentencia combinada.

Esta pregunta surgió del debate sobre Twitter sobre la reciente pregunta de Henry Yuen en MathOverflow, ¿Encontrará esta máquina de Turing una prueba de su detención? y varios comentarios sobre mi respuesta .

A saber, se puede formular una versión de la pregunta anterior en el contexto de la computabilidad (y Akiva Weinberger lo hizo en el hilo de Twitter), considerando el programa de la máquina de Turing $z$ que busca pruebas de que $z$ se detiene o no se detiene, y si encuentra una prueba de detención antes de encontrar cualquier prueba de no detención, entonces se detiene. En $z$ ¿Detener?

Answer 1

Como Akiva Weinberger conjeturó Esto depende de la aplicación.

Sí, es cierto, $0=0$ es una frase de este tipo, es decir $0=0$ es equivalente a la afirmación de que existe una prueba de $0=0$ que es más corto que todas las pruebas de su negación, ya que podemos demostrarlo y comprobar, por enumeración, que la prueba es más corta que todas las pruebas de su negación, y dos tautologías son equivalentes.

De la misma manera, $0=1$ es equivalente a la afirmación de que existe una prueba de $0=1$ que es más corto que todas las pruebas de su negación, ya que podemos refutar esto y comprobar, por enumeración, que no hay ninguna prueba más corta, y dos contradicciones son equivalentes.

Coincido con la conjetura de Akiva de que también existen sentencias indecidibles de este tipo.

Incluso para las sentencias de Rosser, aunque todas son indecidibles, no sé si hay razones para creer que todas son equivalentes entre sí (como lo son las sentencias de Gödel y Löb). No creo que las operaciones de tipo Rosser tengan puntos fijos únicos.

Answer 2

Como ya han señalado Akiva Weinberger y Will Sawin, la respuesta depende de los detalles de la formalización de la noción de prueba.

Arreglemos la terminología: Dado un predicado de prueba $\mathrm{Prf}_\tau(x,y)$ , el correspondiente predicado de comprobabilidad $\mathrm{Pr}_\tau(x)$ se define como $\exists y \mathrm{Prf}_\tau(x,y)$ y el correspondiente Predicado de demostrabilidad de Rosser como $\exists y (\mathrm{Prf}_\tau(x,y) \land \forall z \leq y \lnot \mathrm{Prf}_\tau(\lnot x,z))$ . Un predicado de demostrabilidad es estándar si concuerda, de forma demostrable en PA, con el predicado de demostrabilidad "ordinario". Un punto fijo de un predicado de demostrabilidad $\mathrm{Pr}(x)$ a menudo se denomina Sentencia Henkin .

Ahora, Kurahashi ( Sentencias de Henkin y principios de reflexión local para la demostrabilidad de Rosser , APAL 167(2):73-94, 2016) muestra que hay predicados de prueba estándar tales que sus correspondientes predicados de demostrabilidad de Rosser tienen sentencias de Henkin demostrables y refutables únicamente (Teorema 4.2), y que hay otros predicados de prueba estándar tales que sus predicados de demostrabilidad de Rosser tienen sentencias de Henkin independientes (Corolario 4.1).

Véase también la pregunta 7.2 de Halbach & Visser ( Autorreferencia en aritmética II RSL 7(4):692-712, 2014) y la discusión posterior, que parece implicar que el punto fijo de un predicado de demostrabilidad de Rosser, obtenido por la diagonalización canónica de Gödel, no puede ser independiente.