Este equipo especializado pasados varios días de trabajo y de recopilar de información, encontramos los datos necesarios, deseamos que te sea útil en tu plan.
Solución:
Como rober arthan dicho en los comentarios, una forma de distinguir entre (un tipo de) prueba directa y prueba indirecta es simplemente distinguir entre pruebas que usan reglas deductivas intuicionistamente válidas y pruebas que no lo hacen.
Para mostrar que hay algunos teoremas (utilizando la lógica clásica) que no tienen pruebas intuicionistamente válidas, basta con mostrar que hay una manera de interpretar la lógica intuicionista tal que las reglas deductivas intuicionistas son válidas para esa interpretación, y además que hay una tautología de la lógica clásica que no es una tautología bajo esa interpretación. Uno popular es LEM (es decir, $A∨¬A$), pero puede no ser convincente. Aquí está otro:
$(A⇒B)∨(B⇒A)$.
No se puede probar esta tautología clásica en la lógica intuicionista. En ese sentido preciso no puede haber prueba directa de esta tautología. Esto es más convincente que LEM porque es incluso un poco contrario a la intuición y realmente necesita ‘verificar casos’ (basándose en LEM) para probarlo. Para que no piense que ‘comprobar casos’ es directo, observe que toda prueba intuicionista de ( $¬B⇒¬A$ ) se puede traducir a una prueba que es intuicionista excepto por una sola verificación de caso LEM:
Si $A$:
$B∨¬B$.
Si $B$:
$B$.
Si $¬B$:
[Insert proof of ( $¬B⇒¬A$ ) here.]
$¬A$.
contradicción (es decir $A,¬A$).
$B$.[by explosion]
$B$.
$A⇒B$.
Hay muchas interpretaciones de la lógica intuicionista bajo las cuales esta tautología clásica no se sostiene. Uno son los marcos de Kripke (ver aquí un boceto) y otro es la interpretación de BHK. Comprender cualquiera de ellos le dará una idea clara de cómo se puede considerar exactamente que una prueba intuicionista es ‘directa’.
De wikipedia en https://en.wikipedia.org/wiki/Direct_proof
“En matemáticas y lógica, una prueba directa es una forma de mostrar la verdad o falsedad de una declaración dada mediante una combinación directa de hechos establecidos, generalmente axiomas, lemas y teoremas existentes, sin hacer más suposiciones. Para probar directamente una enunciado condicional de la forma “Si p, entonces q”, basta con considerar las situaciones en las que el enunciado p es true. La deducción lógica se emplea para razonar desde las suposiciones hasta la conclusión”.
Esta oración “Para probar directamente un enunciado condicional de la forma “Si p, entonces q”, basta con considerar las situaciones en las que el enunciado p es true.”, es particularmente importante porque nos dice que una prueba directa solo examina lo que sucede si la hipótesis es true. A true la hipótesis no puede producir una false conclusión, por lo que una prueba directa no examina false conclusiones, tampoco. Sin embargo, una prueba indirecta examina lo que sucedería si la conclusión fuera false por su prueba.
No estoy seguro de si hay algún teorema que haya demostrado tener una prueba indirecta, pero aquí hay una prueba indirecta de la irracionalidad de $sqrt2$ como ejemplo. https://www.math.utah.edu/~pa/math/q1.html