Definición de "no constructiva"a prueba de

Question

Me preguntaba si es posible definir exactamente lo que un no-constructivas (nc) es la prueba. He visto a menudo el concepto asociado con el uso de principios tales como el axioma de elección o de la ley de medio excluido, (y lo anterior implica la última, esto es Diaconescu del teorema). Sería correcto decir que un nc prueba es una prueba que utiliza algo que implica el principio de excluidos middele? Aquí hay otro par de dudas que tengo sobre el tema:

1) Frecuencia de uso de determinados tipos de teoremas del análisis se dijo "no constructiva". Por ejemplo, el de Picard–Lindelöf teorema sobre la existencia y unicidad de soluciones para ciertos tipos de ecuaciones diferenciales es a menudo caracterizado como tal, ya que no proporcionan una explícita expresión analítica para la solución. Sin embargo no parece como si la demostración de este teorema se basa en cualquier nc principios, sino que se basa en el punto fijo de Banach teorema, que proporciona una secuencia definida por una relación de recurrencia que converge pointwise a la solución. Aunque analíticamente inútil, no de esta manera de definir la solución formalmente como constructivo como cualquier?

2) Son prueba por contradicción nc? Por ejemplo, como se explica en este post hay un intuitionist (es decir, constructiva) la prueba de la infinitud de los números primos?, la clásica prueba de la infinitud de los números primos es nc si sólo se llega a una contradicción, pero como se señaló en las respuestas puede ser fácilmente modificado para que se define un algoritmo, el cual viene con la (n+1)ésimo primo. Si las pruebas por las contradicciones son nc, ¿cuál es la nc principio de su uso?

Answer 1

Me disculpo si esta respuesta termina un poco vago.

No hay una definición de lo "constructivo" o "no constructiva". Incluso en la comunidad de matemáticos constructivismo, hay muchos desacuerdos. Sólo el título de un libro clásico, "Variedades de análisis constructivo", ya que sugiere esto.

Puedo señalar dos problemas comunes con constructivas o no constructivas de las pruebas.

• La construcción depende de métodos de prueba. Por ejemplo, la clásica regla de inferencia de la doble negación eliminación ("$\lnot \lnot P$ derivan $P$") es generalmente visto como no constructiva. Pero algo parecido a la regla de la ex falso quodlibet ("$P$$\lnot P$ se derivan de la sentencia $Q$") fue considerado como aceptable para los defensores de intuitionism. El estado de el axioma de elección varía mucho de un programa constructivo de las matemáticas para el otro.

• La construcción depende de las representaciones. Las cosas que se pueden hacer de forma constructiva con un objeto matemático dependen de cómo el objeto se representa. Por ejemplo, en general no se puede demostrar de manera constructiva que para cualquier número real $a$ $a < 0$, $a = 0$, o $a > 0$. Esto es debido a que el sistema habitual para la representación de números reales no permite esta pregunta para ser contestada en forma constructiva, acaba de dar una representación de $a$. Por otro lado, es posible en muchos sistemas constructivos para demostrar que el entero es negativo, 0 o positivo", porque la representación de un número entero utilizado en este tipo de sistemas es lo suficientemente agradable para permitir que la respuesta sea de manera constructiva determina a partir de la representación. Tenga en cuenta que para algunos constructivistas de la "representación" lo que importa es la representación mental que tienen.

Estos dos elementos están relacionados debido a la forma constructiva permitido métodos de prueba dependen en gran medida de las representaciones que se utiliza. Por ejemplo, las formas apropiadas de el axioma de elección no son constructivo en relación a CZF la teoría de conjuntos, pero son constructivas en relación a Martin-Löf tipo de teoría.

Volvemos a la pregunta original. Hay muchos constructivo pruebas de que no utilice cualquiera de los métodos que implican la totalidad de la ley del medio excluido. Por ejemplo, la prueba podría usar el llamado "menor limitada principio de la omnisciencia", que no implica el medio excluido. De hecho no sé si hay una frase en el idioma de Heyting aritmética que implica la totalidad de la ley del medio excluido por el resto de la HA.

Answer 2

Dos buenos recursos en línea para empezar a aprender sobre constructivo de las matemáticas son de Wikipedia y de la SEP. También hay varios buenos libros y estudios sobre constructivo de la matemática y sus variedades. Aquí están algunas de las que más me gusta:

Encuesta:

• A. S. Troelstra, "Una Historia del Constructivismo en el Siglo 20", 1991

Libros:

• A. Heyting, "Intuitionism - Una Introducción", 1971

• M. Beeson, "Fundamentos de Constructivo de las Matemáticas", 1985

• D. van Dalen y A. S. Troelstra, "el Constructivismo en Matemáticas: Una Introducción", en dos volúmenes, 1988

• D. Puentes, F. Richman, "Variedades de Constructivo de las Matemáticas", 1987

• Por Martin-Löf "Intuitionistic Tipo De Teoría", 1984 (nota: esto es bastante antiguo y Martin-Löf ha hecho varios cambios significativos a este vistas a lo largo del tiempo que son al mejor de mi conocimiento, no son publicados en un bonito formulario por desgracia.)

Para la mayoría de los constructivo matemáticos, la esencia de las matemáticas no son pruebas, sino construcciones. Qué quieren decir con la construcción varía, por ejemplo, para Brouwer estas son construcciones mentales, los objetos matemáticos (particularmente infinita de los objetos matemáticos) no tienen una existencia independiente de la mente. Así que para demostrar algún objeto existe, usted debe construir. Cómo se puede construir un mental de los objetos matemáticos? Según algunos intuitionist, un matemático puede entender lo que una construcción por su intuición. Existen métodos de construcción que ha sido aceptado pero no hay un a priori obligado métodos posibles, algunos matemático puede venir para arriba con un nuevo método de construcción de la mañana. Con esto en mente, se vuelve más claro por qué esperan que la justificación de la inexistencia de un objeto a ser una construcción de la conversión de una hipotética construcción para la construcción de la contradicción. Un buen punto de partida para entender a estos, es el BHK interpretación. Como Carl ha señalado que hay puntos sutiles acerca de cómo estas construcciones están representados, en particular, ¿cuál es la representación de las entradas y las salidas de una construcción funcional. Muchos clásicamente idénticos conceptos no son constructivamente idénticos, por ejemplo, hay diferencias entre una función y una operación (ver Beeson 1985 para más detalles). De manera constructiva en matemáticas tenemos más fundamentales conceptos de lo que tenemos en la clásica de las matemáticas, donde muchos de estos conceptos puede ser reducido a definiciones basadas en otros y uno debe tener cuidado con el sentido de los enunciados. Cuando uno escribe $\forall f \ldots$ $f$ una operación o una función? y así sucesivamente.

Otras de las variaciones de Bouwer del intuitionism, hay otras tres versiones activas de constructivismo: 1. Recursivo/Matemática Computable interpreta construcción como función computable (relacionados con la escuela rusa del constructivismo y de Markov), 2. El obispo de estilo el constructivismo, lo cual es consistente con la clásica de las matemáticas y también con intuitionism y computable de las matemáticas, y 3. Martin-Löf's tipo de teoría que es más delicado que los otros (al menos en mi humilde opinión).

Así que no es fácil ¿cómo puede descartar la posibilidad de que un teorema no tiene constructiva de la prueba en el sentido de intuitionism (a menos que uno haya constructiva de la prueba que se iba a convertir esas hipotéticas pruebas para constructivo pruebas de contradicción), ya que las posibles construcciones no están limitados a los que tenemos actualmente, y la comprobación de si una determinada prueba es constructiva de la prueba es un intuitivo concepto que no está definido formalmente y no se puede comprobar basado en un conjunto fijo de reglas (por ejemplo, mediante un programa de ordenador). Así que en teoría, cada clásico teorema de que no se ha descartado por una constructivo prueba puede tener potencialmente un constructiva prueba y es difícil dar contraejemplos a los clásicos del razonamiento. Por otro lado Brouwer desarrollado lo que se llama débil-contador de ejemplos, las declaraciones que a su corrección implicaría que conocemos algo en este momento que no sabemos, por ejemplo, la convergencia de todas las secuencias de Cauchy de números racionales implica que sabemos que la GC (Goldbach de la Conjetura) es verdadera o que sabemos GC es falso, y ahora no sabemos. (GC no es esencial para el argumento, se puede reemplazar con cualquier $\Pi_1$ fórmula que no sabemos es la verdad y no sabemos que es falso).