Formalización en Isar de la metalógica de primer orden

Abstract

El objetivo del trabajo es formalizar razonamiento complejo de forma legible por los humanos y procesable por las máquinas. Más precisamente, formalizar en el sistema de razonamiento Isabelle/HOL/Isar la metateoría de la lógica de primer orden como se expone en capítulo 1 del libro "Introduction to mathematical logic" de Elliott Mendelson y en los primeros cinco capítulos del libro "First-Order Logic and Automated Theorem Proving" de M. Fitting. 1) Se presenta una formalización de un sistema axiomático de la lógica proposicional y la demostración de la completitud del sistema usando el método de Kalmar de eliminación de variables. 2) Se presenta una formalización de la terminación y corrección de un algoritmo para calcular una forma normal conjuntiva de una fórmula proposicional. El algoritmo está descrito en términos de la notación uniforme para las fórmulas de la lógica proposicional; para demostrar su terminación se define una función de medida en términos de los conceptos de "multiconjunto" y "rango" de una fórmula. 3) Se formaliza la corrección de un procedimiento de prueba de tautologías usando tableros semánticos. La terminación se demuestra de la misma forma que en el caso del algoritmo de la forma normal conjuntiva. Para la formalización de la completitud de este método de prueba se utiliza el lemma de Hintikka. 4) Se formaliza la demostración del teorema de existencia de modelos para un conjunto consistente S de fórmulas pertenecientes a un lenguaje proposicional L. Esta demostración está basada en extender S a un conjunto consistente maximal M el cual resulta ser satisfacible (por ser un conjunto de Hintikka) y por tanto S también. Como una aplicación del teorema de existencia de modelos en la lógica proposicional, se formalizan el teorema de compacidad y el teorema de interpolación de Craig. 6) Se presenta la formalización de la sintaxis y semántica de la lógica de primer orden. Para la representación de las fórmulas se emplea la notación de de Bruijn y se formaliza el teorema de existencia de modelos en la lógica de primer orden siguiendo el mismo orden de ideas que en el caso proposicional, y como una aplicación se formaliza la demostracion del teorema de Löwenheim-Skolem. 7) Por último, se define un sistema de deducción natural para lo lógica de primer orden. Se formaliza su corrección y como una consecuencia del teorema de existencia de modelos para la lógica de primer orden, se formaliza su completitud.