En esta pregunta, que se refiere sólo con enteros positivos $\mathbb N$ y otros finitary objetos que pueden ser codificados con números enteros. Un término de la función significa un total computable en función de $\mathbb N^n\to\mathbb N$ con uno o varios argumentos. Cartas de $m,n,k$$\mathbb N$. Cartas de $f,g$ rango de las funciones.
Un término de la secuencia de funciones de $f_m(n)$ es sólo un nombre diferente para dos argumentos total computable en función de $f(m,n)$. Un elemento de una secuencia es un argumento de la función obtenida mediante la fijación del primer argumento, por ejemplo,$f_2(n)=f(2,n)$.
Decimos que un argumento de la función es un polinomio de la torre de iff puede ser construido en un número finito de pasos mediante los siguientes 3 reglas:
- La función constante $f(n)=1$ es un polinomio de la torre.
- Si $f(n)$ es un polinomio de la torre, a continuación, $n^{f(n)}$ es un polinomio de la torre.
- Si $f(n)$ $g(n)$ son polinomio torres, a continuación, $f(n)+g(n)$ es un polinomio de la torre.
Obviamente, todo polinomio torres es el total de funciones computables. Algunos ejemplos son los $5,n^3+7n+2, n^{n^{n^5+10n}+n^3+1}+2n^{n^2+5}+5n^7+2n+3$.
Una función de $f(n)$ está dominado por una función de $g(n)$ fib $f(n)<g(n)$ para todos lo suficientemente grande $n$; formalmente $\exists k\,\forall n\ge k,f(n)<g(n)$.
Una secuencia de funciones de $f_m(n)$ es no creciente iff ninguno de sus elementos es dominado por el elemento siguiente.
Una secuencia de funciones de $f_m(n)$ estabiliza iff todos sus elementos son los mismos para todos lo suficientemente grande $m$; formalmente $\exists k\,\forall m\ge k\,\forall n,f_m(n)=f_k(n)$.
La proposición. Todos los no-aumento de la secuencia del polinomio torres estabiliza.
Al parecer, la proposición puede ser formalizado como una puramente aritméticos declaración. Estoy interesado en una prueba de esta proposición, que no iba a apelar a conjuntos infinitos de alguna manera. Por ejemplo, no debería utilizar arbitraria secuencias infinitas o los números reales, excepto computable, que puede ser representado por un algoritmo correspondiente, y no debe de pedir prestado los resultados de análisis, a excepción de aquellos que pueden ser probadas en el análisis constructivo. Podríamos utilizar una teoría de la hereditario finito de conjuntos de números naturales, funciones computables, o cualquier otro finitary objetos como urelements (que puede ser codificado como hereditaria finito de conjuntos de todos modos).
Un relativamente fácil infinitary prueba pueden ser esquematizadas de la siguiente manera. Observar, que una forma de un polinomio de la torre escrito como una expresión similar a la forma normal de Cantor de algunos ordinal por debajo de $\varepsilon_0$. De hecho, hay un bijection entre ellos (que se obtiene mediante la sustitución de $n$ $\omega$ o viceversa), y no es difícil ver que este bijection conserva el orden (donde polinomio torres están ordenados por la dominación, y de los ordinales ordenado, como de costumbre, por $\in$). Así, el conjunto de polinomio torres es isomorfo a $\varepsilon_0$. Ahora, debido a que cada ordinal es bien ordenado, vemos que el conjunto de polinomio torres también es bien ordenado, en otras palabras, no es infinito disminución de la secuencia de ellos. Así, todos los infinitos sin aumento de la secuencia debe estabilizarse.
Por supuesto, esta prueba utiliza muchos términos y lemas que generalmente se introdujo y comprobados en términos de conjuntos infinitos. E. g. necesitamos definir $\omega$$\varepsilon_0$, definir bien el orden, bijection y isomorfismo, probar que cada ordinal por debajo de $\varepsilon_0$ tiene una única no-recursiva Cantor forma normal -- todo lo que normalmente se hace con conjuntos infinitos. Yo no soy un finitist de alguna manera, pero se siente que todo lo que podría evitarse durante los fines de probar esta relativamente simple aritmética declaración (por supuesto, no es tan simple si desea escribir en completamente formalizada-pero nosotros no queremos eso). A veces incluso parece obvio, si yo pienso en ella el tiempo suficiente :)
Cada paso disminuye un número de pasos restantes (si ya por debajo de $n$), o que lo obliga a tomar una decison acerca de cómo muchos de los pasos restantes (cuando pasa de $n$ para algunas constantes a continuación), o requiere que usted tome una decisión acerca de cómo muchas veces más que usted puede tomar una decisión que usted será capaz de revisar más tarde (cuando pasa de $n^2$ a continuación), o sobre el número de decisiones sobre el número de decisiones sobre el número de decisiones ..., o sobre el número de cláusulas en los anteriores puntos suspensivos, y así sucesivamente hacia un final inevitable.
Pero espero encontrar una finitary prueba puede rigurosamente captura la idea de que el párrafo anterior, tal vez mediante la construcción de una cadena de las aplicaciones del principio de la inducción y, a continuación, el uso de algunos meta-razonamiento por inducción que esta cadena puede hacerse arbitrariamente largas. He oído (pero nunca he visto a una prueba de ello) que la proposición de mi pregunta no puede ser demostrado a partir de los axiomas de la aritmética de Peano solo, así que somos libres para invocar de nuevo meta-axiomas como "todo es demostrable a partir de axiomas de Peano es cierto", o "todo es demostrable a partir de axiomas de Peano más el anterior axioma es verdadero", y así sucesivamente. Considero esto como una válida finitary razonamiento.
