Clásicamente, el condicional (o directa), contrapositivo y pruebas por la contradicción son equivalentes, en el sentido de que una prueba de que uno se puede convertir en una prueba de otro.
Tomemos, por ejemplo, una prueba formal de las $$¬Q\rightarrow ¬P \vdash P \rightarrow Q$$
En el siguiente yo uso Gentzen del método de deducción natural (1934):
1) $¬Q\rightarrow ¬P$, Premisa
2) $P$, Asunción
3) $\neg Q$, Asunción
4) $\neg P$, 1,2, Modus Ponens
5) $\bot$, 2,3, Junto Introducción
6) $\neg\neg Q$, 3-5, La Negación Introduciton
7) $Q$, 6, Eliminación De La Doble Negación
8) $P \rightarrow Q$, 2-7, Introducción Condicional
En algunas otras lógicas, en particular Intuitionistic Lógica - que surgió de la L. E. J. Brouwer's insatisfaction con el no de los métodos constructivos de los clásicos de las matemáticas - esta prueba es imposible.
Si se mira atentamente, verá que en el paso 7, teníamos que utilizar la doble negación de la eliminación de la regla. De hecho, esta regla es equivalente con el Medio Excluido Principio $\alpha \vee \neg \alpha$ que dice que cada frase $\alpha$ es verdadero o falso.
Pero intuitionists no niegan el medio excluido principio: sólo dicen que no pueden mantener generalmente, en particular para los infinitos dominios. Por ejemplo, considere la frase "hay números primos más grandes que $10^{10}$". Bueno, podría ser cierto: para demostrar su verdad-la campana es "suficiente" para examinar para cada $n > 10^{10}$ si hay algo de $n$ que es primo, uno por uno. Pero si esta frase es falsa seguramente no puede demostrar que!
La conclusión que se extrae es que depende de cuál sea el sistema que estamos hablando: las pruebas son equivalentes o no en algunos lógica subyacente.
