Sucesión de Specker

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:

${\displaystyle 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

${\displaystyle \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.

• 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.