Hay ejemplos de conjuntos de números naturales que han demostrado ser decidable pero no constructiva pruebas solamente?
Respuestas
¿Demasiados anuncios?
Cuando enseño la computabilidad, yo suelo utilizar el siguiente ejemplo para ilustrar el punto.
Deje $f(n)=1$, si no se $n$ consecutivo $1$s en algún lugar de la expansión decimal de $\pi$, e $f(n)=0$ lo contrario. Esta es una función computable?
Algunos estudiantes podrían probar, ingenuamente, para calcular así: en la entrada de $n$, de empezar a enumerar los dígitos de $\pi$, y en busca de $n$ consecutivo $1$s. Si lo encuentra, entonces la salida de $1$. Pero luego se dan cuenta de: ¿y si en una entrada en particular, ha buscado durante 10 años, y todavía no se encuentra la instancia? No parece justificado en la salida $0$ bastante, sin embargo, ya que tal vez podría encontrar el consecutivo $1$s buscando un poco más.
Sin embargo, se puede demostrar que la función es computable como sigue. Tampoco hay arbitrariamente largas cadenas de $1$ $\pi$ o hay una cadena más larga de $1$s de cierta longitud $N$. En el primer caso, la función de $f$ es la constante de $1$ función, que es, sin duda computable. En el último caso, $f$ es la función con el valor de $1$ para todos los de entrada de $n\lt N$ y el valor de $0$$n\geq N$, que para cualquier fija $N$ es también una función computable.
Así hemos demostrado que $f$ es computable en efecto proporcionando una lista infinita de programas y demostrando que uno de ellos se calcula el $f$, pero no sabemos cuál exactamente. De hecho, creo que es una pregunta abierta de la teoría de números cuyo caso es la correcta. En este sentido, este ejemplo tiene un resemblence a Gerhard ejemplos.
Paul
Puntos
4500
El Robertson–Seymour teorema implica que cada menor de edad-cerrado de la familia $F$ de grafos finitos es decidable en el tiempo $O(n^3)$. Sin embargo, no se proporciona un algoritmo explícito hasta que uno de los suministros explícito finito lista de prohibidos a los menores que caracterizan $F$; la prueba de que dicha lista siempre existe no es constructivo.
Draemon
Puntos
387
CINCO NOTAS SOBRE LA APLICACIÓN de la PRUEBA DE la TEORÍA A la CIENCIA de la computación por Georg Kreisel, p. 32. Kreisel notas, que su conjunto "es recursiva por el mero hecho de) decidability y recursiva enumerability de los teoremas de cualquier sistema formal. No hay aparente forma de refinación de [este] brutal definición".
Jim B
Puntos
18849
No es el estándar de ejemplo que participaron Último Teorema de Fermat, excepto que ahora tenemos una buena idea de lo que el conjunto es. Así que vamos a reemplazar con "el menor entero positivo n que es un múltiplo de 4 y para los que no la matriz de Hadamard de orden n existe, o 1 si las matrices de Hadamard de todos los órdenes posibles de existir." Esto define un singleton, que es la decidable. Se podría argumentar que, en principio, es constructivo, mientras que yo diría que, dado que todavía no sabemos máxima determinantes para los pequeños pedidos de menos de 100, a usted y a su supuesta nietos no verán un valor para n, entonces usted tendrá un tiempo difícil de mostrar, para mí, una construcción basada en esta definición existe, como no existe ninguna garantía de terminación de la construcción.
Alternativamente, cualquier conjunto finito que es a la que llegó no constructiva medios (E. g. codificaciones de contraejemplos para Frankl la union-cerrado familias conjetura, donde la supuesta prueba que hay sólo un número finito es no constructiva) debe contar como un ejemplo.
Las mejores respuestas surgirán una vez que una buena idea de no constructiva ha sido especificado. En cuanto a dicha noción, voy a dejar las discusiones filosóficas a los demás.
Gerhard "Me Preguntan Sobre El Diseño Del Sistema" Paseman, 2010.02.10
LorenzCK
Puntos
2819
Asumir su conjunto $A\subseteq\mathbb{N}$ es decidable, que es, $\forall_n (n\in A\vee n\not\in A)$. Markov en Principio asegura que su conjunto es computable. Como es computable, que puede ser descrito por una $\Pi_2^0$-Fórmula, y esto es comprobable en la Aritmética de Peano. Por lo tanto, el uso de la Friedman-Traducción, usted encontrará una constructivo prueba de su decidability de Heyting Aritmética.
Tanto para los conjuntos con decidability comprobable de la Aritmética de Peano. Por supuesto, hay cosas como el Teorema de Goodstein, en el que este Teorema puede no ser aplicable. En este caso, usted tiene que especificar qué más fuertes del Sistema constructivo que usted desea. Pero, probablemente, similar teoremas también tienen a continuación.
