La clase más común de la lógica que no admiten prueba por contradicción se intuitionistic o constructivo de la lógica. (Voy a usar "constructiva" y "intuitionistic" más o menos indistintamente aquí.) Específicamente, esto significa que no se admite cualquiera de las siguientes instrucciones equivalentes (o cualquier otra declaración equivalente): la Ley de Medio Excluido ($P\lor\neg P$), la Doble Negación Eliminación ($\neg\neg P\implies P$), Peirce la Ley de ($((P\implies Q)\implies P)\implies P$), en Contraposición ($(\neg Q\implies \neg P)\implies (P\implies Q)$).
La prueba por contradicción corresponde a una ligera variante de la Doble Negación de la Eliminación. Es decir, incluso intuitionistically $\neg P \equiv (P\implies \bot)$. (De hecho, esto ocurre con frecuencia, por definición, en intuitionistic de los sistemas). La prueba por contradicción es la que, a continuación,$(\neg P \implies \bot)\implies P$. Esto no debe confundirse con la reductio ad absurdum que es $(P\implies \bot)\implies\neg P$ que es válido intuitionistically. (De nuevo, a menudo por definición.) Observe cómo que no podemos usar reductio ad absurdum para conseguir la prueba por contradicción simplemente crear instancias de con $\neg P$; que sólo nos da $(\neg P \implies \bot)\implies \neg\neg P$. Aún estaríamos necesidad de Eliminación de la Doble Negación para obtener $P$.
Es muy común confundir las reglas anteriores así que a menudo no está claro que la gente quiere decir cuando dicen que "la prueba por contradicción" o "reductio ad absurdum". Puedo hacer la elección que hago, porque reductio ad absurdum (como he definido) no es prueba de algo, se refuta, mientras que la prueba por contradicción no demostrar algo. Cuando quiero ser clara, sin embargo, por lo general llamada uso de la Doble Negación de la Eliminación de la prueba por contradicción y $\neg$ introducción de reductio ad absurdum como $\neg$ introducción es inequívoca (pero esta terminología no suele ser familiar para aquellos que no han estudiado un poco de [estructurales] prueba de la teoría).
La terminología de la forma y responder a sus inquietudes, teoremas que puede ser comprobado de forma constructiva (es decir, en la construcción o intuitionistic lógica) no "esencialmente" de exigir la prueba por contradicción, incluso si hay una prueba de que hace uso de ella. Los teoremas que no son verdad en intuitionistic lógica de hacer "esencialmente" de exigir la prueba por contradicción (asumiendo que son verdadero clásico). Si interpretamos la "verdad" como "no rebatible", entonces podemos incrustar la lógica clásica en intuitionistic lógica. Este proceso es mecánico y no sólo nos permiten traducen mecánicamente clásicamente comprobable teoremas en intuitionistically comprobable teoremas, sino que también se traduce mecánicamente clásicas pruebas en intuitionistic pruebas. Por supuesto, los teoremas son más "débiles" en la intuitionistic lado, por ejemplo, la Doble Negación Eliminación sería traducido a $\neg\neg P \implies \neg\neg P$ por estas traducciones.
Teóricamente, constructivo pruebas puede ser más fácil que las clásicas pruebas desde constructiva de la prueba es un clásico de la prueba. En la práctica, muchos clásicas pruebas son constructivas y limitarse a un constructiva a prueba los límites en el espacio de búsqueda un poco (y lo hace un poco mejor estructurado). Es muy fácil argumentar que el clásico de principios como el de la Doble Negación de la Eliminación son no-intuitivo, y me va a tocar que un poco. Sin embargo, una constructivo de la prueba, en general, contiene mucha más información de la clásica prueba. El término "constructiva" proviene de la idea de que una prueba debe proporcionar un medio para "construir" un "testigo". Constructiva de la prueba corresponde a un algoritmo para la construcción de un testigo a una declaración. Esto es más dramático para existencial declaraciones. Constructivamente demostrar una verdadera declaración significa que usted tiene que construir la cosa que se reivindica para existir. Esto puede ser un trabajo mucho más (e incluso imposible) que simplemente alegando que algo existe sin proporcionar cualquier medio (y no puede ser de ninguna manera) de la creación de lo que supuestamente existe como muchos clásicas pruebas hacer. Por otro lado, explícita construcciones son a menudo altamente informativos, y una parte significativa de los contenidos de un teorema puede ser en realidad la construcción explícita utilizado en la prueba. (Por ejemplo, estoy leyendo "Complejidad Computacional: Un Enfoque Moderno". El famoso Cocinero-Levin teorema que demuestra que el SAT es NP-completo es probada mediante la codificación de la ejecución de una máquina de Turing como un (polinomio de tamaño) de fórmula Booleana. Esta construcción puede entonces ser usado para demostrar que un problema es en P si y sólo si existe un polinomio de tamaño logspace uniforme de la familia de los circuitos que resolver el problema. No está del todo claro por qué se SENTÓ ser NP-completo implicaría esto, pero a partir de la prueba de Cocinar-Levin no es tan difícil de ver).
De modo constructivo pruebas pueden requerir (potencialmente) más trabajo que las clásicas pruebas no "sólo" porque están trabajando en un débil sistema (que en sí es muy valioso como muchas de las cosas más interesantes son los modelos de intuitionistic la lógica de la lógica clásica), sino también las pruebas son de carácter más divulgativo. Otra forma de ver la diferencia en el trabajo es buscar en el cómputo de la interpretación de estos sistemas. El Curry-Howard correspondencia famosa muestra que las proposiciones, de las pruebas y la prueba de transformaciones corresponden a tipos de programas, y el programa de transformaciones. La mayoría de interpretación específica de "Curry-Howard correspondencia", que en este punto se toma a menudo más como un principio, es el resultado específico que la Deducción Natural de la presentación de Intuitionistic Lógica Proposicional corresponde a la de tipo simple Cálculo Lambda. Más recientemente, una correspondencia similar se ha encontrado en la clásica de la lógica. Lo más importante aquí es que los principios clásicos corresponden a operadores de control como call/cc. De hecho, el tipo de call/cc es $((A\to B)\to A)\to A)$ que se ve exactamente como la de Peirce Ley! Estos son (en)la famosa frase expresiva, pero difícil de entender (como prueba por contradicción). Esto significa que el uso de call/cc puede resultar en mucho más corto de los programas, pero call/cc sí es difícil de entender y se complica la comprensión de cada parte del programa, incluso las partes que no encuentran el uso de call/cc. La incorporación de la lógica clásica en intuitionistic lógica que he mencionado anteriormente corresponde a Continuación el Estilo de pases (CPS), que es un método que se suele utilizar para entender y aplicar el control de los operadores. Aquí está una descripción interactiva en la historia de la forma que ilustra lo que en realidad ocurre con la Ley de Medio Excluido de cómputo (modulo licencia artística, pero consulte la referencia de papel por Phil Wadler la historia original [que yo prefiero] y el menos coloridos presentan detalles).
Como nota final, hay una diferencia entre un específico teorema de ser probada de manera constructiva y trabajando en una lógica constructiva. Podemos tener una constructivo prueba de que manipula no de manera constructiva comprobable declaraciones. Esto corresponde a la escritura de un programa que tiene acceso a subrutinas que son en sí no aplicable (a menudo esto se llama una de oracle). De trabajo dentro de la lógica constructiva en general, requiere una cantidad decente de la reelaboración de los diferentes definiciones. Por ejemplo, en forma constructiva las diversas clásicamente equivalente formulaciones de "finito" se convierten de manera constructiva no equivalentes, y por lo que es importante la forma de especificar que un conjunto es "finito". Del mismo modo, la costumbre de la formulación del Teorema del Valor Intermedio no es cierto de manera constructiva, pero una adecuada declaración similar se puede probar (en el contexto de una constructivo formulación de los números reales). En este punto, gran parte de las matemáticas ha sido rehecho en la construcción de marcos. Sin embargo, incluso dentro de un marco clásico, hay un montón de valor constructivo de las pruebas, y hay un montón de valor de a sabiendo que los resultados son constructivamente demostrable.
