¿Por qué algunas personas no creen en la ley del medio excluido?

Las pruebas tienen que ver con convencer . Con la ley del medio excluido, equiparamos dos tipos diferentes de pruebas que no son igualmente convincentes o poderosas.

Si desea probar algo y construir un ejemplo, o al menos mostrar cómo construir un ejemplo, es muy convincente. Quiero decir, ¡tengo exactamente lo mismo aquí! Esta es una prueba constructiva .

Sin embargo, también podría probar que algo existe sin realmente construirlo. En efecto, estás diciendo que ” x no conduce a una contradicción, por lo tanto x “. Esto es bastante menos convincente: no tengo un ejemplo ni ninguna forma de obtener un ejemplo. De hecho, ¡podría ser imposible obtener un ejemplo! Esta es una prueba de existencia .

Ahora, hay una pregunta filosófica para responder aquí: si puedo demostrar que algo “existe” (es decir, no es inconsistente) y que es incuestionable (es decir, nunca puedo tenerlo de manera significativa) ¿existe realmente ? En un sentido muy práctico, no lo hace: no importa cuánto trabaje, no puedo acceder a él.

Estos dos tipos diferentes de pruebas no son igualmente convincentes . Idealmente, nos gustaría alguna forma de diferenciar entre ellos. Resulta que eliminar la ley del medio excluido nos permite distinguir los dos tipos de pruebas .

El sistema lógico que simplemente elimina la ley del medio excluido de la lógica clásica se llama lógica constructiva o intuicionista . En la lógica constructiva, las pruebas constructivas permanecen sin cambios. Si tuviéramos una prueba constructiva de x en la lógica clásica, aún podemos probar x en la lógica constructiva. Además, si tenemos una prueba para x en lógica constructiva, tenemos una prueba constructiva para x .

Pero, ¿qué pasa con las pruebas de existencia? Bueno, una prueba de existencia ya no es suficiente para probar x . Pero resulta que las pruebas de existencia todavía existen (heh): ¡en realidad podemos integrar la lógica clásica en la lógica constructiva! El truco viene de notar que en lógica constructiva, no tenemos la regla ¬¬x ⇒ x . Entonces ¬¬x y x son proposiciones diferentes . Lo bueno es que si tenemos una prueba clásica de x , ¡tenemos una prueba constructiva de ¬¬x !

En lógica constructiva x significa x pero ¬¬x significa algo así como ” x no conduce a una contradicción”. Una declaración diferente pero profundamente relacionada que no podríamos elaborar en la lógica clásica.

Entonces: en la práctica, deshacerse de la ley del medio excluido no hace que nuestra lógica sea menos poderosa. Más bien, simplemente nos da un nuevo medio para distinguir entre pruebas constructivas y de existencia, ¡permitiéndonos distinguirlas fácilmente! La lógica constructiva se convierte en un nuevo sistema donde las pruebas de x y ¬¬x ofrecen evidencia de x , solo que con diferentes puntos fuertes .

En otras palabras, no es que la gente no “crea” en la ley del medio excluido, es que eliminarla hace que las pruebas normales sean más convincentes y las pruebas de existencia más explícitas.

Además, si se pregunta cómo funciona realmente la incrustación de doble negación, probablemente sea más fácil pensarlo en términos de la correspondencia de Curry-Howard, donde es equivalente a transformar el código en un estilo de paso de continuación (CPS).

Porque no es verdad.

O más bien, es cierto, dentro de los límites de la lógica, que están completamente divorciados del mundo real. El mundo real solo entra en la lógica cuando alguien elabora una propuesta, una declaración que puede interpretarse como sobre el mundo real (también conocido como “semántica”).

Para ciertas cosas simplificadas pero importantes sobre el mundo real, se pueden hacer tales proposiciones. Estos son importantes, ya que le permiten manipular la lógica en lugar del mundo real y obtener resultados que se correlacionan con el mundo real. La semántica tiene que ir en ambos sentidos, o toda la empresa no tiene sentido. Para muchos hechos del mundo real, podemos hacer esto; Es la base de la ciencia.

Pero no todo sobre el mundo real se modela tan fácilmente. La ciencia trata de la simplificación: las poleas no tienen fricción ni masa, no hay resistencia al aire, las gallinas son esféricas, etc. Para un conjunto mucho más amplio de facetas del mundo real, las traducciones a proposiciones simples arrojan conclusiones inválidas cuando son manipuladas por la lógica.

La semántica tiene que ir en ambos sentidos, y “violar la lógica” es irrelevante. Es el mundo real el que no puede ser violado. El mundo real tiene prioridad. La lógica es solo una herramienta para modelarla.

Entonces, cuando alguien dice: “Estás con nosotros o contra nosotros”, eso no es válido: puedo estar en parte contigo y en parte contra ti. Encuadra mal las proposiciones, y la ley del medio excluido sale por la ventana.

Hay una historia de supuestos contraejemplos de LEM, pero tienden a involucrar una confusión entre la verificabilidad de la proposición matemática y su verdad.

Por ejemplo, la conjetura de Goldbach se cita típicamente como una de esas proposiciones que no estamos en condiciones de probar o refutar. La idea de que esta dificultad socava la validez de LEM, ya que la declaración de LEM es una afirmación universal sobre el valor de verdad de las declaraciones matemáticas.

El núcleo del debate es sobre la naturaleza de la verdad matemática. Los defensores de LEM a menudo parecen exigir la noción de que las verdades matemáticas están fijadas en algún reino platónico (ya sea verdadero o falso, nada menos o más), mientras que el intuicionista piensa que este tipo de metafísica es absurda e injustificada por la práctica matemática.

http://plato.stanford.edu/entrie