Sucesión de Specker

En teoría de la computabilidad, una sucesión de Specker es una sucesión monótonamente creciente computable y acotada de números racionales cuyo supremo no es un número real computable. El primer ejemplo de tal secuencia fue construido por Ernst Specker (1949).

La existencia de sucesiones de Specker tiene consecuencias para el análisis computable. El hecho de que tales sucesiones existan significa que la colección de todos los números reales computables no satisface el principio del límite inferior superior del análisis real, incluso aunque se sólo consideren sucesiones de números computables.

Una forma común de resolver esta dificultad es considerar únicamente sucesiones que van acompañadas de un módulo de convergencia; ninguna sucesión de Specker tiene un módulo de convergencia computable.

Más en general, una sucesión de Specker se denomina "contraejemplo recursivo" al principio de límite inferior superior, es decir, es una construcción que muestra que este teorema es falso cuando se restringe a reales computables.

El principio del límite inferior superior también se ha analizado en el programa de la matemática inversa, donde se ha determinado la fuerza exacta de este principio. En la terminología de ese programa, el principio del límite inferior superior es equivalente a ACA₀ sobre RCA₀. De hecho, la demostración de la implicación hacia adelante, es decir, que el principio del límite inferior superior implica ACA₀, se obtiene fácilmente de la demostración de libro de texto (véase Simpson, 1999) de la no computabilidad del principio supremo en el límite inferior superior.

Construcción

La siguiente construcción se describe en Kushner (1984). Sea A cualquier conjunto recursivamente enumerable de números naturales que no sea decidible, y sea (a_i) una enumeración computable de A sin repetición. Se define una sucesión (q_n) de números racionales mediante la siguiente regla:

q_{n}=\sum _{i=0}^{n}2^{-a_{i}-1}.

Está claro que cada q_n es no-negativa y racional, y que la secuencia q_n es estrictamente creciente. Además, debido a que a_i no tiene repetición, es posible estimar cada q_n' mediante la serie

\sum _{i=0}^{\infty }2^{-i-1}=1.

Así, la sucesión (q_n) está limitada superiormente por 1. Clásicamente, esto significa que q_n tiene un supremo.

Se puede demuestra que x no es un número real computable. La demostración utiliza un hecho particular sobre los números reales computables: si x fuera computable, entonces habría una función computable r(n) tal que | q_j - q_i| < 1/n para todas las i,j > r(n). Para calcular r, se compara la expansión binaria de x con la expansión binaria de q_i para valores cada vez mayores de i. La definición de q_i' hace que un solo dígito binario pase de 0 a 1 cada vez que i aumenta en 1. Por lo tanto, habrá algún n donde un segmento inicial lo suficientemente grande de x ya ha sido determinado por qn que ningún dígito binario adicional en ese segmento podría activarse, lo que lleva a una estimación de la distancia entre qi y qj para i, j > n.

Si cualquier función de este tipo r fuera computable, daría lugar a un procedimiento de decisión para A, como sigue. Dada una entrada k, calcule r(2^k+1). Si k apareciera en la secuencia (a_i), esto tendría como consecuencia que la sucesión (q_i) aumentara en 2^−k-1, pero esto no puede suceder una vez que todos los elementos de (q_i) están dentro de 2^−k-1 entre sí. Por lo tanto, si k se va a enumerar en a_i, debe enumerarse para un valor de i menor que r(2^k+1). Esto deja un número finito de posibles lugares donde se podría enumerar k. Para completar el procedimiento de decisión, verifique estos de manera efectiva y luego devuelva 0 o 1 dependiendo de si se encuentra k.

Bibliografía

Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics, Oxford, 1987.
B.A. Kushner (1984), Lectures on constructive mathematical analysis, American Mathematical Society, Translations of Mathematical Monographs v. 60.
Jakob G. Simonsen (2005), "Specker sequences revisited", Mathematical Logic Quarterly, v. 51, pp. 532–540. doi 10.1002/malq.200410048
S. Simpson (1999), Subsystems of second-order arithmetic, Springer.
E. Specker (1949), "Nicht konstruktiv beweisbare Sätze der Analysis" Journal of Symbolic Logic, v. 14, pp. 145–158.

Datos: Q2308311