En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la deducción natural en la lógica proposicional.

Se ha comenzado repasando las cuestiones fundamentales estudiadas en el tema 1:

• ¿Qué es una fórmula?
• ¿Qué significa que una fórmula sea verdadera?

y planteando una nueva cuestión

• ¿Qué es un teorema?

para responderla, de forma análoga al uso de modelos para responder a la 2ª cuestión, se comenta el uso de las demostraciones.

El primer método de demostración que se presenta es el de deducción natural. Se han estudiado las siguientes reglas:

• Reglas de la conjunción
• Reglas de la doble negación
• Regla de eliminación del condicional
• Regla derivada de modus tollens (MT)
• Regla de introducción del condicional
• Reglas de la disyunción
• Regla de copia
• Reglas de la negación
• Reglas del bicondicional

Las transparencias de esta clase son las 1-17 del tema 2.

Además, se ha explicado el uso de Pandora para construir demostraciones por deducción natural. Como aplicación, se han resuelto los ejercicios 2.5.19 y 2.5.26 del Libro de ejercicios.

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

• la de la clasificación de los grupos finitos simples que tiene más de 10.000 páginas,
• la del teorema de los 4 colores que requiere el uso del ordenador para resolver algunos casos,
• la de la conjetura de Kepler que requiere aún más cálculo por ordenador que la anterior.

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.