Hay dos implícito problemas con esta pregunta. Porque esta es la segunda vez en los últimos días y que este tipo de pregunta se ha hecho, quiero explicar las cuestiones en detalle, que no se puede hacer en un comentario.
Problema 1: Romper es difícil de hacer
En la mayoría de los de la norma clásica fundacional de los sistemas, no es sencillo romper con la ley del medio excluido.
Por ejemplo, si usted toma ZFC con un típico deductivo sistema y, a continuación, retire la ley del medio excluido del sistema deductivo, el resto del sistema aún demostrar la ley del medio excluido, y lo que en este sentido que usted nunca directamente el uso de la ley del medio excluido en una prueba, porque usted puede probar los casos, usted necesita directamente a partir de los otros axiomas y reglas deductivas.
Una reflexión formal de este fenómeno se llama Diaconescu del teorema (también llamado el Padre de familia supiese–teorema de Myhill). La cuestión fundamental es que, como los sistemas de ZFC son tan inmerso en la lógica clásica que es muy difícil de cortar la clásica lógica, dejando el resto de los axiomas sin cambios.
Así, usted realmente necesita para empezar con un sistema que se ha construido desde cero para ser "constructivo", en lugar de comenzar con un sistema clásico y el corte de la ley del medio excluido. Estos "constructiva" los sistemas son también algo a menudo llamado "intuitionistic", por el camino.
Por ejemplo, usted podría preguntar: "¿Qué es el teorema demostrable en ZFC teoría de conjuntos, pero no IZF la teoría de conjuntos?" o "¿Qué es el teorema demostrable en la aritmética de Peano, pero no Heyting aritmética?". Cada uno de esos es mucho más significativo pregunta que puede tener específicas y precisas respuestas.
Tema 2: la Prueba por Contradicción no es la misma como Prueba por Medio Excluido
Muchos de los sistemas que no incluyen la ley del medio excluido no incluyen la regla de la prueba por contradicción. Que la regla dice que si podemos probar $A \land \lnot A$ para algunos sentencia de $A$, entonces podemos concluir cualquier otra oración $B$ que nos gusta. Esta norma se incluye, por ejemplo, en Heyting aritmética, que es un bien establecido fundamentales del sistema constructivo de las matemáticas, y que no incluyen la ley del medio excluido.
Para tener una idea de cómo la ley del medio excluido funciona, puede ser mejor que pensar en la ley del medio excluido permite la prueba por casos. De esta forma, la ley del medio excluido dice que si usted puede probar $A \to B$, y además probar $\lnot A \to B$, entonces se puede concluir $B$, incluso sin saber si $A$ o $\lnot A$ es comprobable por su propia cuenta. (Esto es equivalente a través de una muy débil lógica constructiva a la habitual afirmación de que $C \lor \lnot C$ es comprobable para cada frase $C$.) Esta manera de ver en medio excluido ayuda a mostrar cómo se diferencia de la prueba por contradicción.
Aquí es otra manera de ver la diferencia. En el clásico de las matemáticas, si asumimos $C$, derivar una contradicción, y, a continuación, a la conclusión de $\lnot C$, lo que llamamos una "prueba por contradicción". Del mismo modo, si asumimos $\lnot C$, derivar una contradicción, y, a continuación, a la conclusión de $C$, llamamos también que "la prueba por contradicción". Sin embargo, sólo la segunda de las conclusiones a las que requiere la ley del medio excluido relación constructiva razonamiento. El primer ejemplo de este párrafo es en realidad un directo constructivo prueba de $\lnot C$, debido a que en sistemas constructivos $\lnot C$ es la abreviatura de "$C$ implica una contradicción". Así que no todo lo que llamamos una "prueba por contradicción" en el clásico de las matemáticas, en realidad se utiliza la prueba de la regla de "prueba por contradicción". Algunas maneras habituales en las que pensamos acerca de la lógica clásica, sin embargo, puede ocultar este problema. Hay una buena entrada de blog por Andrej Bauer sobre este tema.
