¿Esperamos que los ordinales computables suficientemente grandes resuelvan todas las cuestiones de aritmética?

Question

Me encontré con un Correo electrónico: de Ron Maimon en physics.SE que hace lo que me parece una conjetura muy interesante que nunca he visto antes sobre lo que se necesitaría para resolver todas las cuestiones de aritmética. Primero intentaré ser más preciso: a cuestión de aritmética es un enunciado de primer orden en la aritmética de Peano, por ejemplo, un enunciado sobre si alguna máquina de Turing se detiene. Creo que estos son exactamente los enunciados matemáticos que, por ejemplo, Scott Aaronson considera que tienen valores de verdad definidos e independientes de nuestra capacidad de demostrar o refutar a partir de cualquier sistema particular de axiomas, a diferencia, por ejemplo, de la hipótesis del continuo.

Si he entendido bien a Ron, parece creer lo siguiente:

Conjetura: Toda cuestión de aritmética se resuelve con la afirmación de que algún ordinal computable suficientemente grande $\alpha$ está bien fundado.

Por ejemplo, Gentzen demostró que el fundamento de $\alpha = \epsilon_0$ puede demostrar la consistencia de la AP.

Pregunta: ¿Se ha planteado esto como una conjetura en algún lugar de la literatura? ¿Se espera que sea cierto?

Una versión posiblemente más específica de esta pregunta: ¿existe para cada número entero positivo $n$ un ordinal computable $\alpha_n$ cuyo fundamento determina el valor del número de Busy Beaver $BB(n)$ ?

Answer 1

La cuestión de si un orden lineal computable está bien fundado es $\Pi^1_1$ -completo, por lo que esto es cierto en cierto sentido:

Existe una función computable $F$ tal que, para cada frase $\varphi$ en el lenguaje de la aritmética con el número de Godel $\ulcorner\varphi\urcorner$ , $F(\ulcorner\varphi\urcorner)$ es un índice para un ordenamiento computable si $\varphi$ es cierto.

(Para ser precisos, esto es demostrable en - digamos - $\mathsf{ZF}$ o incluso mucho menos). Esta es una forma de visualizar $F$ :

Existe un árbol computable $\mathcal{T}\subseteq\mathbb{N}^{<\mathbb{N}}$ con una ruta única $p$ que codifica el conjunto de sentencias aritméticas verdaderas. Esencialmente, un nodo de altura $k$ en $\mathcal{T}$ consiste en una asignación de verdad a la primera $k$ -muchas frases en el lenguaje de la aritmética et datos adicionales de Skolemización parcial" que hasta ahora parecen coherentes (los detalles son un poco tediosos). Dada una frase $\varphi$ , dejemos que $\mathcal{T}_\varphi$ sea el subárbol de $\mathcal{T}$ formado por todos los nodos de $\mathcal{T}$ que (cuando se "leen" de forma adecuada) no declaran $\varphi$ sea verdadera; se trata de un subárbol computable de $\mathcal{T}$ , de manera uniforme en $\varphi$ y está bien fundado si $\varphi$ es cierto. A continuación, establecemos $F(\ulcorner\varphi\urcorner)$ para ser el Ordenación de Kleene-Brouwer de $\mathcal{T}_\varphi$ .

Por supuesto, todo esto es bastante artificial. Para que quede claro, el mapa $F$ mismo es perfectamente natural/interesante/importante, pero el resultado $F(\ulcorner\varphi\urcorner)$ no es particularmente interesante para mí. Contrasta con la construcción anterior, donde la conexión entre $\varphi$ y $F(\ulcorner\varphi\urcorner)$ es aburridamente tautológico, con el teorema de Gentzen de que la fundamentación de (la notación habitual para) $\epsilon_0$ implica $Con(PA)$ . Incluso si uno no compra esto como hacer $Con(PA)$ más creíble - y no lo hago - es ciertamente un hecho profundo e interesante. La versión interesante de la conjetura, para mí, sería: "Por cada frase de aritmética $\varphi$ existe un orden lineal computable $\alpha$ tal que $(i)$ $WF(\alpha)\leftrightarrow\varphi$ y $(ii)$ sabiendo que esto de alguna manera arroja luz sobre $\varphi$ (a menos que $\varphi$ ya era tan simple como para ser aburrido)". Y nada de lo que he descrito puede hacer eso, obviamente.