LMF2017: Consecuencia lógica y demostrabilidad

La clase de hoy del curso Lógica matemática y fundamentos ha empezado analizando el problema fundamental de los estudiados en el tema 1 sobre la sintaxis y demática de la lógica proposicional. Dicho problema es el de la consecuencia lógica (es decir, dado un conjunto de fórmulas S y una fórmula F decidir si F es consecuencia lógica de S). En el caso proposicional dicho problema se puee resolver mediante tablas de verdad, pero este método presenta dos inconvenientes: su complejidad exponencial y la imposibilidad de ampliarlo para lógicas de primer orden.

Como solución al problema se comentó la posibilidad de transformar el problema de consecuencia al de demostrabilidad de forma que F es consecuencia lógica de S si, y sólo si, se puede demostrar F a partir de S. El nuevo problema que se plantea es precisar qué es una demostración.

Ambos problemas, el verdad y el demostración se manifiestan en la crisis de los fundamentos de la matemáticas (como se ilustra en el libro de Morris Kline Matemáticas (La pérdida de la certidumbre),

En la aproximción al concepto de la demostración hemos comentado algunas demostraciones enormes, como

Las dos últimas demostraciones han sido formalmente verificadas con ayuda de ordenador. La del teorema de los 4 colores fue verificada en 2005 por Benjamin Werner y Georges Gonthier usando Coq. La conjetura de Kepler fue verificada en el proyecto Flyspec usando los sistemas de demostración Isabelle y HOL Light.

Además de las demostraciones enormes, hemos comentado las demostraciones incorrectas. En dicha lista aparece inconsistencia de Frege en su libro sobre los fundamentos de la aritmética. Para explicar esta última, y su relación con los fundamentos de la programación, hemos comentado las presentación de Benjamin Peirce especialmente las páginas 8 a 10 donde se comenta la inconsistencia de Frege.