¿Cómo probar que la ley del tercero excluido es necesaria?

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?

Demostrar es el verbo, la prueba es el sustantivo.

Respuestas (2)

¿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 a , b , ambos irracionales, de modo que a b es racional". Esto considera a = b = 2 , luego dice a b 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 X 2 = 0 implica X = 0 bajo la lógica intuicionista, porque la tricotomía no se cumple sin la ley del tercero excluido.

¡Gracias por tu respuesta! Actualicé mi pregunta: quiero saber qué métodos existen para mostrar que cada prueba de un determinado teorema necesita la ley del medio excluido ...
¿Tiene referencia para el reclamo qué X R ( X < 0 X = 0 X > 0 ) no se sostiene intuicionistamente?
tc.umn.edu/~hellm001/Publications/MathematicalPluralismSIA.pdf Esencialmente, cualquier otro manual básico sobre el análisis infinitesimal suave hará el trabajo. Este no es un texto de lógica, por supuesto.
@Ian Gracias, también lo encontré aquí .
@Git Gud: el análisis intuicionista es compatible con el axioma de que todas las funciones son continuas. Entonces no pueden probar la tricotomía, porque si pudieran, podrían construir la función que es 1 en 0 y 0 en otra parte, que es discontinua.
Desafortunadamente, estos argumentos con un análisis infinitesimal suave no se aplican aquí. Que es llamado " R " en SIA no es el conjunto de los reales de Dedekind (o el conjunto de los reales de Cauchy, para el caso). Para los reales de Dedekind y para los reales de Cauchy se puede probar intuitivamente X 2 = 0 X = 0 , aunque no apelando a la tricotomía, que de hecho no es intuicionistamente demostrable. En cambio, lo haces observando que a = 0 es equivalente a ¬ ( a # 0 ) , dónde a # 0 ("separación") significa q q > 0 . | a | q , y eso X # 0 X 2 # 0 .
Además del esquema de prueba de Carl, una forma topológica divertida de mostrar que la tricotomía no es demostrable es observar que (1) las declaraciones demostrables intuitivamente son "estables en familias continuas" y que (2) ser cero no lo es. ¡Intenté escribir esto para una audiencia de filósofos de las matemáticas aquí , y estoy disponible para cualquier pregunta o comentario que pueda tener!

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.

Cuando dices "todos los teoremas en la lógica clásica se convierten en consecuencias de la ley del tercero excluido", ¿quieres decir que todo lo que se puede probar clásicamente también se puede probar solo con la ley del tercero excluido y algunas reglas de transformación y reemplazo?
@tampis En ese sistema, todas las pruebas comienzan con la ley del medio excluido y, por lo tanto, solo puede probar algo con la ley del medio excluido y (algunas de todas) esas reglas.
Si tomo un teorema demostrado en el nuevo sistema con solo la ley del medio excluido (+ algunas reglas de reemplazo). ¿Por qué no puedo demostrar el mismo teorema con lógica intuicionista?
@tampis Es posible que pueda probar el mismo teorema con lógica intuicionista o puede que no. Depende del teorema. La lógica intuicionista no tiene la ley del tercero excluido.