En la teoría de la computabilidad , una secuencia de Specker es una secuencia acotada computable , monótonamente creciente , 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 secuencias de Specker tiene consecuencias para el análisis computable . El hecho de que existan tales secuencias significa que la colección de todos los números reales computables no satisface el principio de límite mínimo superior del análisis real, incluso cuando se consideran solo secuencias computables. Una forma común de resolver esta dificultad es considerar solo secuencias que van acompañadas de un módulo de convergencia ; ninguna secuencia de Specker tiene un módulo de convergencia computable. De manera más general, una secuencia de Specker se denomina contraejemplo recursivo del principio del límite mínimo superior, es decir, una construcción que muestra que este teorema es falso cuando se restringe a reales computables.
El principio del límite mínimo superior también se ha analizado en el programa de matemáticas inversas , donde se ha determinado la fuerza exacta de este principio. En la terminología de ese programa, el principio de límite superior mínimo es equivalente a ACA 0 sobre RCA 0 . De hecho, la prueba de la implicación directa, es decir, que el principio del límite superior mínimo implica ACA 0 , se obtiene fácilmente a partir de la prueba del libro de texto (véase Simpson, 1999) de la no computabilidad del supremum en el principio del límite superior mínimo.
Construcción
Kushner (1984) describe la siguiente construcción. 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. Definir una secuencia ( q n ) de números racionales con la regla
Está claro que cada q n es no negativo 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 contra la serie
Por tanto, la secuencia ( q n ) está acotada por encima de 1. Clásicamente, esto significa que q n tiene un x superior .
Se muestra que x no es un número real calculable. La demostración usa un hecho particular sobre números reales computables. Si x fuera calculable, habría una función calculable r ( n ) tal que | q j - q i | <1 / n para todo i , j > r ( n ). Para calcular r , compare 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 vaya de 0 a 1 cada vez que i aumenta en 1. Por lo tanto, habrá algunos n donde q n ya haya determinado un segmento inicial suficientemente grande de x que no haya dígitos binarios adicionales en ese segmento podría activarse alguna vez, lo que conduce a una estimación de la distancia entre q i y q j para i , j > n .
Si cualquiera de tales funciones r fuera computable, conduciría 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 haría que la secuencia ( q i ) aumente 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 el uno del otro. Por lo tanto, si k se va a enumerar en una i , debe enumerarse para un valor de i menor que r (2 k +1 ). Esto deja un número finito de posibles lugares donde k podría enumerarse. Para completar el procedimiento de decisión, verifíquelos de manera efectiva y devuelva 0 o 1 según se encuentre k .
Ver también
Referencias
- Douglas Bridges y Fred Richman. Variedades de matemáticas constructivas, Oxford, 1987.
- BA Kushner (1984), Conferencias sobre análisis matemático constructivo , American Mathematical Society, Translations of Mathematical Monographs v. 60.
- Jakob G. Simonsen (2005), "Se revisan las secuencias de Specker", Mathematical Logic Quarterly , v. 51, págs. 532–540. doi : 10.1002 / malq.200410048
- S. Simpson (1999), Subsistemas de aritmética de segundo orden , Springer.
- E. Specker (1949), "Nicht konstruktiv beweisbare Sätze der Analysis" Journal of Symbolic Logic , v. 14, págs. 145-158.