El mayor número definible

Question

Si $a_n$ se define como el mayor número entero definible mediante $n$ caracteres en alguna teoría estándar como PA o $Z_2$ .

¿Podemos probar o refutar que hay algún número entero finito $k$ , tal que para todo $i>k$ , $a_i$ es una potencia perfecta ( $m^n$ , para $n>1$ )? (o muy cercano a uno de la forma a^b, con $b\gg a$ )?

Answer 1

Probablemente no. Su función $a_n$ no es computable, y es bastante sensible a pequeños detalles de cómo contamos los símbolos y cuáles son exactamente las operaciones primitivas, que normalmente no son lo suficientemente importantes como para ser especificadas con mucha precisión en los textos.

En cuanto a su pregunta de seguimiento: La función no puede ser significativamente mucho más pequeño que la función Busy Beaver, porque podemos definir la ejecución de una máquina de Turing con una fórmula PA/Z2 que es lineal en el tamaño de la descripción de la máquina. Por otro lado, no puede ser significativamente mucho más grande que el Castor Ocupado, porque a para cualquier fórmula podemos especificar una máquina de Turing que busque una prueba de que a esta fórmula define un número único.

Así que, aparte de algún posible estiramiento o encogimiento horizontal, el crecimiento de su fórmula es equivalente al del Castor Ocupado.

Answer 2

La secuencia $(a_n)$ crece mucho más rápido que los números de Busy Beaver. Por ejemplo, no sólo la secuencia de Busy Beaver $BB(n)$ pero también expresiones como $BB(BB(n))$ y $\underbrace{BB(\cdots(BB(}_{n\text{ times}}n)))$ son definibles en PA con fórmulas de longitud no muy superior a la de la fórmula más pequeña que define $n$ (en particular, con una longitud sublineal en $n$ ). Esto se debe a que las funciones $n\mapsto BB(n)$ etc. son definibles en PA, por lo que para definir un valor de la función en un número entero específico sólo hay que combinar la definición de la función (que tiene longitud constante) con la definición del número entero.

Por cierto, hay dos razones por las que la máquina de Turing sugerida por Henning Makholm no funcionaría: en primer lugar, podría no encontrar una prueba de que la fórmula en cuestión define un número entero (ya que aunque el hecho de que la fórmula defina un número entero es cierto, puede no ser demostrable), y en segundo lugar, incluso si encontrara una prueba de que la fórmula define un número entero, no tendría forma de convertir esa prueba en información sobre cuál es el valor de ese número entero.