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.
- ¿Hay idiomas casi completos de Turing?
- ¿Cómo ha cambiado tu vida Euclides?
- ¿Cuál es la filosofía detrás de Fight Club? ¿Cuáles son los motivos y filosofías de Tyler Durden?
- ¿Los libertarios están menos interesados en la idea de la lógica?
- ¿Cómo funciona un sitio de chat aleatorio?
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).