PDF de programación - Formalización en Isar de la metalógica de primer orden

DEPARTAMENTO DE CIENCIAS DE LA COMPUTACI ÓN

E INTELIGENCIA ARTIFICIAL

Formalización en Isar de la metalógica de

primer orden

Memoria presentada por
Fabián Fernando Serrano Suárez
para optar al grado de
Doctor en el Programa de
Lógica, Computación e
Inteligencia Artificial
por la Universidad de Sevilla

V. B. Directores

José Antonio Alonso Jiménez

Francisco Jes ús Martín Mateos

Sevilla, 6 de febrero de 2012

2

Creo poder hacer muy clara la relación de mi conceptografía con el
lenguaje común si la comparo con la que hay entre el microscopio y el
ojo. Este último, por el campo de su aplicabilidad y la movilidad con
que se sabe adaptar a las más diversas situaciones, posee gran superio-
ridad frente al microscopio. Considerado como aparato óptico, mues-
tra sin duda muchas imperfecciones, las cuales pasan desapercibidas,
por lo común, sólo como consecuencia de su estrecha conexión con la
vida mental. Pero tan pronto como los propósitos científicos establecen
mayores exigencia en la precisión de las distinciones, el ojo resulta in-
suficiente. Por el contrario, el microscopio es de lo más apropiado para
tales fines, aunque, por ello, no es utilizable para otros.

Gottlob Frege (1879) Conceptografía (Un lenguaje de fórmulas,

semejante al de la aritmética, para el pensamiento puro) p. 8–9.

4

Agradecimientos

A la Secretaria y al Grupo de Lógica Computacional del Departamento de Cien-
cias de la Computación e Inteligencia Artificial de la Universidad de Sevilla por su
hospitalidad durante mi permanencia en Sevilla; un reconocimiento especial a Fran-
cisco J. Martín por sus oportunas observaciones a la versión preliminar del trabajo de
tesis.

Hoy que vuelvo a mis labores docentes recordé de José Antonio, mi asesor de tesis,
que la sencillez es un principio esencial para que un Sistema de Razonamiento Complejo
sea completo, correcto y eficiente.

Índice

1

2

.

.

11
Introducción
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.1 Antecedentes
.
1.2 Hipótesis y objetivos .
.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.3 Metodología y plan de trabajo . . . . . . . . . . . . . . . . . . . . . . . . . . 16
1.4 Estructura de la memoria . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

.

.

.

.

.

.

Introducción a Isabelle/HOL/Isar
21
2.1 Elementos básicos de Isabelle/HOL . . . . . . . . . . . . . . . . . . . . . . 22
2.1.1 Teorías .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
Inducción estructural . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.1.2
Funciones recursivas . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.1.3
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.1.4 Definiciones .
. . . . . . . . . . . . . . . . . . . . . . . . . 28
2.1.5 Definiciones inductivas
2.1.6 Pruebas en Isabelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.2 Pruebas estructuradas en Isar . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.2.1 Esquemas de demostración . . . . . . . . . . . . . . . . . . . . . . . 33
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

2.3 Ejemplo .

. .

. .

.

.

.

.

.

.

.

3 Completitud de un sistema axiomático de la lógica proposicional

39
3.1 Formalización del sistema axiomático . . . . . . . . . . . . . . . . . . . . . 39
3.1.1 La regla de debilitamiento . . . . . . . . . . . . . . . . . . . . . . . . 42
3.1.2 Teoremas elementales . . . . . . . . . . . . . . . . . . . . . . . . . . 43
3.1.3 Teorema de la deducción . . . . . . . . . . . . . . . . . . . . . . . . 46

5

6

Índice

3.2 Semántica de la lógica proposicional
. . . . . . . . . . . . . . . . . . . . . . 52
3.3 Teorema de corrección del cálculo proposicional
. . . . . . . . . . . . . . . 59
3.4 Teorema de completitud . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
3.4.1 Prueba informal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
3.4.2 Prueba formal del teorema de completitud de la lógica proposicional 63

4 Forma normal conjuntiva

Sintaxis y semántica proposicional

77
4.1
. . . . . . . . . . . . . . . . . . . . . . . 77
4.2 Notación uniforme .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
4.3 Disyunciones y conjunciones generalizadas . . . . . . . . . . . . . . . . . . 87
Semántica de las disyunciones y conjunciones generalizadas . . . . 87
4.3.1
4.3.2 Equivalencia entre fórmulas . . . . . . . . . . . . . . . . . . . . . . . 89
4.4 Descripción de la formalización del algoritmo FNC . . . . . . . . . . . . . 90
4.5 Reglas de reescritura .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
4.6 Algoritmo para hallar una forma normal conjuntiva . . . . . . . . . . . . . 94
4.7 Formalización de la terminación de la función FNC . . . . . . . . . . . . . 96
4.7.1 La funciones de medida . . . . . . . . . . . . . . . . . . . . . . . . . 97
4.8 Corrección del algoritmo FNC . . . . . . . . . . . . . . . . . . . . . . . . . 104

5 Método de prueba basado en tableros semánticos

107

5.1 Descripción de la formalización de la deducibilidad mediante tableros

5.2

5.3

.

.

.

.

.

.

semánticos .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
5.1.1 Definición de tablero semántico . . . . . . . . . . . . . . . . . . . . . 107
Sistema de prueba por tableros . . . . . . . . . . . . . . . . . . . . . . . . . 110
5.2.1 Terminación de la función PruebaTablero . . . . . . . . . . . . . . . . 112
Semántica de los tableros semánticos . . . . . . . . . . . . . . . . . . . . . . 114
5.3.1 Equivalencia entre tableros . . . . . . . . . . . . . . . . . . . . . . . 116
5.3.2 Corrección del algoritmo PruebaTablero
. . . . . . . . . . . . . . . . 118

6 Teorema de existencia de modelos proposicionales

121
6.1
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121
6.2 Conjuntos consistentes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123

Introducción .

.

.

.

.

.

.

Índice

7

6.3 Conjuntos consistentes y clausura por subconjuntos . . . . . . . . . . . . . 124
6.4 Propiedad de carácter finito . . . . . . . . . . . . . . . . . . . . . . . . . . . 127
6.5 Extensión a una propiedad de carácter finito . . . . . . . . . . . . . . . . . 128
6.6 Extensión a conjuntos consistentes maximales
. . . . . . . . . . . . . . . . 133
6.7 Conjuntos de Hintikka y modelos de Hintikka . . . . . . . . . . . . . . . . 139
6.7.1 Conjuntos de Hintikka . . . . . . . . . . . . . . . . . . . . . . . . . . 139
Satisfacibilidad de conjuntos de Hintikka . . . . . . . . . . . . . . . 139
6.7.2
6.8 Completitud del método de prueba basado en tableros semánticos
. . . . 145
6.9 Conjuntos maximales y conjuntos de Hintikka . . . . . . . . . . . . . . . . 150
6.10 Enumeración de fórmulas proposicionales . . . . . . . . . . . . . . . . . . . 152
6.10.1 Enumeración de árboles binarios . . . . . . . . . . . . . . . . . . . . 153
6.10.2 Enumeración de fórmulas proposicionales . . . . . . . . . . . . . . 156
6.11 Formalización de la existencia de modelos proposicionales . . . . . . . . . 159

7 Aplicaciones del teorema de existencia de modelos proposicionales

167
7.1 Teorema de compacidad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
7.2 Teorema de interpolación de Craig . . . . . . . . . . . . . . . . . . . . . . . 176

8.1

.

8 Sintaxis y semántica de la lógica de primer orden

203
Sintaxis de la lógica de primer orden . . . . . . . . . . . . . . . . . . . . . . 203
Índices de de Bruijn . . . . . . . . . . . . . . . . . . . . . . . . . . . 205
8.1.1
Símbolos de función de una fórmula . . . . . . . . . . . . . . . . . . 206
8.1.2
8.1.3
Sustituciones
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 207
8.2 Semántica de la lógica de primer orden . . . . . . . . . . . . . . . . . . . . 210
8.2.1 Valor de verdad de una fórmula . . . . . . . . . . . . . . . . . . . . 210
Satisfacibilidad y Consecuencia lógica . . . . . . . . . . . . . . . . . 214
8.2.2

9 Teorema de existencia de modelos de primer orden

217
9.1 Conjuntos consistentes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 217
9.1.1 Conjuntos consistentes y clausura por subconjuntos . . . . . . . . . 219
9.2 Propiedad de consistencia y consistencia alternativa . . . . . . . . . . . . . 222
9.2.1 Propiedad de consistencia alternativa . . . . . . . . . . . . . . . . . 222

8

Índice

9.3 Extensión de una propiedad de consistencia alternativa a una de carácter

.

.

.

.

.

.

.

.

.

.

.

. .

finito .

Sentencias .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 231
9.4 Extensión a conjuntos consistentes maximales
. . . . . . . . . . . . . . . . 235
9.5 Conjuntos de Hintikka y modelos de Herbrand . . . . . . . . . . . . . . . . 243
9.5.1
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243
9.5.2 Conjuntos de Hintikka . . . . . . . . . . . . . . . . . . . . . . . . . . 244
9.5.3 Estructuras de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . 245
9.5.4
Satisfacibilidad de conjuntos de Hintikka . . . . . . . . . . . . . . . 247
9.6 Conjuntos maximales y conjuntos de Hintikka . . . . . . . . . . . . . . . . 254
9.7 Enumeración de fórmulas proposicionales . . . . . . . . . . . . . . . . . . . 267
9.7.1 Enumeración de árboles binarios . . . . . . . . . . . . . . . . . . . . 268
9.8 Enumeración de las fórmulas de un lenguaje de primer orden . . . . . . . 270
9.8.1 Enumeración de términos . . . . . . . . . . . . . . . . . . . . . . . . 271
9.8.2 Enumeración de fórmulas . . . . . . . . . . . . . . . . . . . . . . . . 275
9.9 Formalización de la existencia de modelos de primer orden . . . . . . . . . 279
9.10 Teorema de L¨owenheim-Skolem . . . . . . . . . . . . . . . . . . . . . . . . 288

10 Deducción natural para la lógica de primer orden

299
10.1 Un sistema de deducción natural para la lógica de primer orden . . . . . . 29