En 1936 Gödel anunció un teorema según el cual las pruebas de ciertos teoremas $T_1,T_2,\ldots$ se acortan drásticamente cuando se pasa de un sistema formal, como la aritmética de Peano PA, a uno más fuerte, como un sistema en el que Con(PA) es demostrable. Más concretamente, dada cualquier función computable $f$ podemos encontrar una secuencia $T_1,T_2,\ldots$ de teoremas tales que $T_k$ tiene una prueba de longitud de orden $k$ en el sistema más fuerte, mientras que cualquier prueba de $T_k$ en PA tiene una longitud de al menos $f(k)$ .
Se han demostrado varias versiones de este teorema, dependiendo del refuerzo de PA elegido, y de la definición de longitud. Véase, en particular, este documento . Sin embargo, no he encontrado una versión con natural secuencia de teoremas $T_k$ . Por ejemplo, parece plausible que se pueda utilizar Teorema de Goodstein , al tomar
$T_k$ = El proceso Goodstein, a partir de la entrada $k$ finalmente se detiene.
¿Se conoce algún ejemplo "natural" de aceleración de Gödel?
Actualización y aclaración. El teorema de aceleración de Gödel da, para cualquier función computable $f$ , una secuencia de teoremas $T_1,T_2,\ldots$ de PA de tal manera que cada $T_k$ tiene una prueba de longitud $O(k)$ en algún fortalecimiento de la AP, mientras que la prueba más corta de $T_k$ en PA tiene una longitud $\ge f(k)$ . En este teorema, la secuencia $T_1, T_2,\ldots$ depende de $f$ .
Si queremos una secuencia "natural" $T_1,T_2,\ldots$ (en particular, si $T_k=\varphi(k)$ para alguna fórmula fija $\varphi$ ) entonces ya no podemos exigir que $f$ sea una función computable arbitraria, o incluso de tasa computable arbitraria de crecimiento. Esto se debe a que (suponiendo que la secuencia $T_1,T_2,\ldots$ es c.e.) la función
$g(k)$ = longitud de la prueba más corta de $T_k$ en PA
es computable, por lo que no podemos preguntar $f$ para crecer más rápido que $g$ .
Entonces, como quiero la secuencia $T_1,T_2,\ldots$ para arreglar, tengo que estar satisfecho si $T_k$ tiene la prueba más corta en PA con una longitud de $O(f(k))$ algunos de crecimiento razonablemente rápido $f$ . Parece que Harvey Friedman tiene ejemplos que se ajustan a la como ha señalado Richard Borcherds. Sin embargo, antes de aceptar la respuesta de Richard, me gustaría conocer una referencia. He estudiado detenidamente La investigación de Harvey Friedman sobre los fundamentos de las matemáticas (North-Holland 1985),
y algunos otros trabajos, sin encontrar una declaración clara de aceleración en el sentido anterior.
