Tras una discusión con Russell Miller, tengo una respuesta a la pregunta. De hecho, hay un real abordable que no es abordable de forma demostrable.
Adoptaremos PA como teoría base, aunque la construcción puede adaptarse fácilmente a otras teorías. Describiré una máquina de Turing $M$ que produce una secuencia convergente de números racionales, pero cualquier máquina de Turing $M'$ que PA demuestra que produce una secuencia convergente de números racionales converge a un número diferente de $M$ lo hace.
La idea es diagonalizar contra cualquier prueba de este tipo que se pueda descubrir. Fijar una enumeración de las máquinas de Turing $M_n$ . Consideremos la siguiente máquina de Turing $M$ . Nuestra máquina en la etapa $k$ producir un número racional $r_k$ dando un número finito de dígitos trinarios, pero utilizando sólo los dígitos 0 y 1 y no el 2, para evitar problemas de legibilidad no únicos. A medida que avanza la construcción, enumeramos sistemáticamente todas las pruebas posibles de la teoría. Es posible que en algún momento encontremos $k$ que existe una prueba de que la máquina de Turing $M_n$ produce una secuencia convergente de números racionales. En este caso, ejecutamos $M_n$ para $k$ pasos, obteniendo el racional actual $q_{n,k}$ aproximación al real al que $M_n$ está convergiendo. En este caso, si $r_k$ es diferente de $q_{n,k}$ por dígito $n$ , entonces utilizamos $r_{k+1}=r_k$ ; de lo contrario, producimos $r_{k+1}$ al dar la vuelta a la $n$ -dígito de $r_k$ de $0$ a $1$ o viceversa para garantizar que $r_{k+1}$ es diferente de $q_{n,k}$ . (Nota, estamos invirtiendo el $n$ -dígito, no el $k$ -dígito, por lo que cada máquina $M_n$ está vinculado al $n$ -enésimo dígito de nuestro límite real). Y simplemente proceder con este plan, teniendo en cuenta las nuevas pruebas como aparecen.
Tenga en cuenta que cada máquina $M_n$ que produzca de forma demostrable una secuencia convergente se considerará infinitas veces, para tamaños cada vez más grandes $k$ ya que hay muchas pruebas de que lo hace. Así que lo relevante $k$ para $M_n$ será arbitrariamente grande. Dado que $M_n$ se ha demostrado que produce una secuencia convergente, se deduce que los valores de $q_{n,k}$ realmente convergen y, por tanto, acaban estabilizándose en su primera $n$ bits (si esos bits son todos $0$ s y $1$ s). Por lo tanto, vamos a dar la vuelta a la $n$ -en nuestra parte racional $r_k$ como máximo un número finito de veces. Se deduce que nuestra secuencia $r_k$ es una secuencia convergente de números racionales.
Pero además, se deduce que siempre que haya una prueba de que alguna máquina $M_n$ produce una secuencia convergente de números racionales, entonces el límite de nuestro real diferirá del límite de esa máquina en un dígito $n$ .
Por lo tanto, tenemos un real abordable que no es demostrablemente abordable, como se desea.
Permítanme comentar el confuso punto sutil aquí sobre en qué teoría hemos probado que nuestra máquina produce una secuencia convergente de racionales. La respuesta es que lo hemos hecho en cualquier teoría que sepa que cualquier afirmación que sea demostrable en la teoría base es de hecho verdadera, ya que necesitábamos saber que cuando encontráramos una prueba de que $M_n$ produce una secuencia convergente de racionales, que esos racionales realmente convergen. Por ejemplo, ZFC tiene esta relación con PA, ya que ZFC demuestra que si $\varphi$ es demostrable en PA, entonces $\varphi$ es cierto. Pero más generalmente, para cualquier $\omega$ -Teoría coherente $T$ podemos extender a una teoría más fuerte $T^+$ que conoce esta implicación.
