La pregunta no me queda muy clara, así que hablaré de un par de interpretaciones de la misma y espero que las respuestas sean útiles.
La lógica intuicionista es básicamente lógica clásica sin medio excluido ( $P \vee \neg P$ ). Podemos recuperar la lógica clásica habitual a partir de la lógica intuicionista bien añadiendo el medio excluido, bien añadiendo el principio de eliminación de la doble negación , $\neg \neg P \rightarrow P$ . Si definimos una prueba directa como aquella que es válida en lógica intuicionista, entonces la pregunta es: ¿es la lógica intuicionista diferente de la lógica clásica?
La respuesta a esta pregunta es sí. Resulta que el medio excluido no es demostrable en lógica intuicionista.
Alternativamente, por prueba directa se puede entender una prueba sin cortes. Esto no está realmente relacionado con la prueba por contradicción como tal, pero podría estar más cerca de lo que quieres decir. La regla del corte es una de las reglas de el cálculo secuencial y afirma que a partir de $\Gamma \vdash \Delta,A$ y $A, \Sigma \vdash \Pi$ podemos deducir $\Gamma,\Sigma \vdash \Delta,\Pi$ . Observe que $A$ aparece en el antecedente pero no en el consecuente. El proceso de convertir una prueba en una prueba sin cortes se conoce como eliminación de cortes .
En este caso, la respuesta a la pregunta es que la eliminación de cortes puede realizarse normalmente para la lógica por sí sola (esto es cierto tanto para la lógica clásica como para la lógica intuicionista) pero no en general cuando se añaden axiomas al sistema. En $PA$ (y si no recuerdo mal incluso en $HA$ la contrapartida intuicionista de $PA$ ) es posible realizar la eliminación de cortes, pero sólo pasando a pruebas infinitas. Hay teoremas en $PA$ que no tienen una prueba sin cortes (finita).
