Esta es una pregunta de seguimiento de esta respuesta de Carl Mummert a la pregunta de si toda prueba con contradicción también puede probarse sin contradicción. Como señaló Carl Mummert, hay demostraciones en la lógica clásica que no se pueden probar con la lógica intuicionista, es decir, que necesitan la ley del tercero excluido.
¿Hay alguna forma o método para mostrar que un teorema solo se puede demostrar con la ley del tercero excluido?
Porque en la lógica mínima tampoco existe el principio de explosión: ¿es posible mostrar/demostrar que cualquier prueba de un teorema necesita el principio de explosión?
¿Te refieres a teoremas que no pueden probarse en lógica intuicionista, o pruebas clásicas de teoremas que no tienen una mera traducción a lógica intuicionista? Para un ejemplo de esto último, existe la prueba elemental clásica de que "existen , , ambos irracionales, de modo que es racional". Esto considera , luego dice es racional o irracional y divide el problema en casos, sin decir qué caso se aplica realmente. Como recuerdo, el caso relevante se ha identificado desde entonces, por lo que existe una prueba intuicionista de este resultado.
Un ejemplo de lo primero es relevante para el análisis infinitesimal suave: no se puede demostrar que implica bajo la lógica intuicionista, porque la tricotomía no se cumple sin la ley del tercero excluido.
Convierta la ley del medio excluido ApNp en su único axioma para la lógica clásica y seleccione reglas adecuadas de transformación y reemplazo. Esto se hace en el Apéndice D del libro de texto Elementary Symbolic Logic de Ulrich y Gustason. En consecuencia, todos los teoremas de la lógica clásica se convierten en consecuencias de la ley del tercero excluido.
También se podría convertir el principio de explosión CKpNpq, o CpCNpq, o CNpCpq en el único axioma si se tienen las reglas adecuadas.
pedro