Download DECIDIBILIDAD DE LA LOGICA DE PREDICADOS MONADICOS
Document related concepts
Transcript
DECIDIBILIDAD DE LA LOGICA DE PREDICADOS MONADICOS POR EL IvlÉTODO DE LA RECUSACION:I(: Magí Cadevall Soler u niversidad Autónoma de Barcelona l. 1.1. DEClDmILIDAD y RECUSACIÓN EL PROBLEMA DE LA DECISIÓN EL OBJETODE ESTE ARTÍCULOes la presentación de un cálculo de recusación para la lógica de predicados monádicos (de 1.0 y 2.0 orden), seguido de la demostración resumida de su corrección y completitud semánticas. En los cálculos lógicos, al disponer de una definición recursiva de fórmulas, sabemos que el conjunto de las fórmulas de un cálculo es decidible. La axiomatización de un cálculo lógico, si es correcta y completa, debe permitir obtener todas y solas las fórmulas de un lenguaje formal que sean verdades lógicas. El conjunto de teoremas de dicho cálculo es generable, pero no necesariamente decidible, ya que no está fijado el orden en que deben aplicarse las reglas para deducir un teorema determinado. De forma análoga un cálculo de recusación debe permitir obtener todas y solas las fórmulas de un lenguaje forinal que no sean verdades lógicas. Consta de un conjunto de fórmulas no válidas elegidas como punto de partida (contraaxiomas o axiomas de recusación) y un conjunto de reglas de derivación que preserven la no valiEste artículo es un resumen de la Tesis Doctoral del autor dirigida por el Dr. Jesús Mosterín y leída el 26 de septiembre de 1975 en la Universidad de Barcelona, ante el tribunal presidido por o el Dr. Francisco Gomá, figurando como vocales los profesores Dr. Miguel Siguán, Dr. Manuel Garrido, Dr. Ramón ValIs. 8 455 ----- 456 Decidibilidad de la lc)gwll dt IJf, rlÍlud,1\ dez. La demostración de la corrección y completilud de un cálculo de recusación para una parcela de la lógica, consti~ tuye la demostración de la decidibilidad de dicha parcela. La recusación es un enfoque nuevo de un viejo tema. Conocida es la decibilidad del cálculo de predicados monádicos que engloba la mayor parte de la lógica tradi~ ciona!. El primero en establecerla fue Lowenheim en 1915,1 Y precisamente en su forma más fuerte: el cálculo de pre~ dicados monádicos de segundo orden con identidad es decidible. Aunque en algunos puntos no es posible fijar sin lugar a dudas el razonamiento del autor, la demostración de Lowenheim adolece de graves defectos, principalmente involucrar el desarrollo booleano de una expresión de lon~ gitud posiblemente infinita. A pesar de los defectos, Lowen~ heim no sólo acertó el resultado, sino que señaló una línea de demostración que será seguida por Skolem y por Beh~ mann, que consiste demostrar para toda fórmula la posi~ bilidad de hallar una cierta fórmula normal prenexa equivalente y practicar la decisión sobre la correspondiente fórmula normalizada. Skolem 2 mejoró la demostración de Lowenheim. Demuestra en primer lugar la decidibilidad de un cálculo de clases de segundo orden (con posibilidad de ligar mediante cuantificadores las variables de clase) cuyos enunciados primitivos son los enunciados numéricos. Entiende Skolem por enunciados numéricos los de la forma 'a > n', donde ea' es un símbolo de clase y en' es un número concreto. A continuación establece la posibilidad de traducir las fórmulas del cálculo de predicados monádicos con identidad a fórmulas equivalentes del cálculo de clases. La demostración de Behmann 3 es más enojosa por contener una traducción repetida del cálculo de, predicados al cálcu1 Loewenheim, L.: "Ueber Moglichkeiten im Relativkalkül". Math. Annalen, 76, 1915, pp: 447-470. Traducido en: van Heijenoort, From Frege to Godel, 1967. 2 Skolem, T.: "Untersuchungen über di Axiome des Klassenkal. küls...". Skrifter, Videnskabakademiet i Kristiania, 3, 1919. Reed. en: Skolem, Selected works in logic, 1970, pp. 67-101. 3 Behmann, H.H: "Beitrage zur AIgebra der Logik, insbesondere zum Entscheidungspobrlem". Math. Annalen, 86, 1922, pp. 163-229. -- - - Decidibilidad de la lógica de predicados... 457 lo de clases, realizando los distintos pasos de la demostración alternativamente en uno u otro lenguaje. Finalmente Ackermann 4 traza una demostración parecida, ya que demuestra que todo enunciado de la lógica de predicados monádicos con identidad (sin variables libres) se puede reducir a una fórmula equivalente de la lógica de pura identidad (cuyas fórmulas atómicas son todas del tipo Cx = y') y a su vez demuestra la decidibilidad de las fórmulas de la lógica de identidad mediante su reducción a forma normal prenexa, sin llegar a un resultado tan fuerte como el de Skolem, ya sugerido por Lowenheim, de que toda fórmula de la lógica de predicados monádicos con identidad puede ser reducida a un enunciado numérico equivalente. La decidibilidad de la lógica de predicados monádicos de primer orden con identidad puede ser reducida a la de la de segundo orden, considerando las fórmulas de primer orden como fórmulas de segundo orden con variables de predicado libres, que serán válidas si lo es la correspondiente clausura universal. Pero para la lógica de predicados monádicos de primer orden sin identidad aparecen métodos de decisión y demostraciones más simples a partir de Bemays-Schonfinkel 19285 Y de Hilbert-Ackermann.6 Otros métodos, basados en la forma normal completa o perfecta, son presentados con diversas variantes por Herbrand, Quine, von Wright. La demostración de la decidibilidad de la lógica de predicados monádicos no es más que el principio de la búsqueda de resultados positivos de decisión en la lógica de predicados o en algunas de sus partes. En 1928 BemaysSchonfinkel demuestran la decidibilidad respecto a la validez de la clase de fórmulas normales prenexas en que los 4 Ackennan, W.: Solvable cases 01 the decision problem. Amsterdam, North-Holland P. Co., 1954. Reed. 1968, pp. 24 Y ss. 5 Bemays, P. y Shoenfinkel, M.: uZum Entscheidungsproblem der mathematischen Logik". Math Annalen, 99, 1928, pp. 342-372. 6 Hilbert, D. y Ackennann, W.: Grundzüge der theoretischen Logik. Berlin, Springer, 1928, pp. 77-79. - - - - - - - - - - - - - 458 Decidibilidad de la lógica de predicados... cuantificado res universales preceden a cualquier cuantificador particular. Pero en 1936 Church 7 solucionó negativamente el problema global de la decidibilidad de la lógica de predicados, con lo que automáticamente resultaban indecidibles las clases de reducción ya conocidas. A partir de este momento se ha tratado de demostrar la decidibilidad de clases lo más extensas posibles de fórmulas lo más complejas posibles y paralelamente establecer la indecidibilidad de clases lo más reducidas posibles de fórmulas lo más simples posible. La demarcación entre clases de fórmulas decidibles e indecidibles ha sido trazada con precisión por lo que se refiere al grado de los predicados y también respecto a la forma del prefijo en las fórmulas normales prenexas. 2.2. OTROS ENFOQUES DE LA DECISIÓN: LA RECUSACIÓN Pero la existencia de métodos de decisión que podemos llamar clásicos, no ha hecho desaparecer el interés por otros enfoques del problema en aquellas partes de la lógica en que la decidibilidad está ya establecida. Además del método de la recusación usado en este artículo, también las tablas semánticas (Beth, Smullyan) 8 constituyen un nuevo enfoque del problema de la decisión, en tanto se pueda demostrar que para ciertas parcelas de la lógica no se requieren tablas infinitas. Lo mismo se puede decir de los estudios sobre la prueba automática de teoremas del calculo de enunciados por métodos algorítmicos (Hao Wang). 9 La idea de los cálculos de recusación es original de Lukasiewicz. En su obra "Aristotle's Syllogistic", expone la idea de derivar todos los modos silogísticos no válidos a 7 Church, A.: "A note on the Entscheidungsproblem". ]our. of Symb. Logic, 1, 1936, pp. 40-41. Reed. en: Davis, The Undecidable, Howlett, Raven Press, 1965, pp. 110-115. 8 Garrido, M.: Lógica simbólica, Madrid, Tecnos, 1974, pp. 264 Y 273. 9-De Torres, A. M.: "Los primeros intentos de prueba automática de teoremas en el cálculo de enunciados". En Teorema IV, 4, 1974. - - - - - - - Decidibilidad de la lógica de predicados... 459 partir de dos modos no válidos (AAI y EEI de la segunda figura), mediante dos reglas de recusación (regla recusativa de separación y de sustitución). Los cálculos de recusación pueden parecer a primera vista un pleonasmo axiomático. En realidad deben considerarse una nueva forma alternativa de enfocar la decidibilidad de una teoría. Es conveniente presentar el planteamiento del problema en un vocabulario más preciso que el usado por Lukasiewicz. La teoría de las funciones recursivas permite una formulación matemática precisa del problema de la decisión. Sea FLM2 el conjunto de fórmulas de la lógica de predicados monádicos de 2.° orden con identidad, TLM2, el conjunto de sus teoremas y VLM2 el conjunto de sus fórmulas válidas. Sea CDem(r, a)', donde r es una secuencia de filas de signos y a E FLM2, la abreviatura de cr es una demostración de a'. Podemos formular los fundamentos del método de la recusación, mediante las proposiciones siguientes: 1) FLM2 es un conjunto recursivo. 2) cDem' es una relación recursiva. 3) TLM2 es un conjunto recursivamente enumerable, ya que a E TLM2 si Y sólo si existe un r tal que Dem(r, a) donde a la relación recursiva cDem' se le ha prefijado un cuantificador. 4) VLM2 es un conjunto recursivamente enumerable. Puesto que si el conjunto de reglas que generan TLM2 es correcto y completo, coinciden los conjuntos TLM2 y VLM2. La definición precisa de decidibilidad puede ser 5) Un cálculo es decidible si y sólo si el conjunto de sus tesis (enfoque sintáctico) o el conjunto de sus fórmulas válidas (enfoque semántico) es recursivo. Ya que la lógica de predicados monádicos es decidible, sabemos que es posible construir para ella un cálculo de recusación. Al mismo tiempo la demostración de la corrección y completitud de dicho cálculo constituye una prueba de la decidibilidad de la lógica de predicados monádicos, ya que --- - - -- - - 460 ! : I I I Decidibilidad de la lógica de predicados... 6) Si VLM2 y FLM2 "'"'VLM2 son recursivamente enumerables y además FLM2 es recursivo, entonces los conjun- tos VLM2y FLM2"'"' VLM2 son recursivos. Una cuestión que puede presentarse es la de la simplicidad y elegancia del cálculo de recusación propuesto. Simplicidad y elegancia son términos escurridizos. Hay una oposición entre brevedad del bagaje axiomático y brevedad en el desarrollo de las derivaciones. En la práctica no siempre se adopta el sistema que puede considerarse más simple para los estudios teóricos: tal es el caso del método axiomático tradicional frente a la deducción natural de Gentzen. El cálculo de recusación que presenta Lukasiewicz para su formalización de la silogística debe ser considerado simple: " . :1 consta de dos axiomas y dos leyes de inferencia. lQ Pero en 1 Ir 1 \1 I I 11 '11 cambio no puede pensarse que aporte otra cosa que elegancia al problema de la decisión. Pues constando el formalismo de un número finito de fórmulas (256 modos silogísticos) y 24 tesis (24 modos válidos), la silogística es una teoría trivialmente decidible. Pero, dado que de la base axiomática asertiva de Lukasiewicz pueden derivarse un número infinito de expresiones (que podemos llamar aristatélicas por ser funciones de verdad de juicios categóricos) además de los modos silogísticos, Lukasiewicz planteó dos problemas: 1.0 ¿'Es infinito el número de expresiones aristotélicas no válidas, independientes de la base axiomática recusativa de Lukasiewicz? 2.° Caso de ser infinito su número ¿puede crearse un cálculo de recusación más potente para tales expresiones? La respuesta para ambos problemas no fue hallada por Lukasiewicz, sino propuesta por su discípulo Slupecki. El primer problema lo resuelve mediante la construcción de modelos (diagramas de círculos). El segundo mediante la regla de Slupecki: ~ex.~'Y ~~~'Y If- ex.~' (~ ~ 'Y) Lukasiewicz, J.: Aristotle's syllogistic. Oxford,.Clarendon Press, 1951. Reed. 1967, p. 96. 10 Decidibilidad de la lógica de predicados... 461 La elegancia de la regla de Slupecki es discutible, ya que no se aplica a fórmulas cualesquiera, sino sólo a ciertas clases de fórmulas: rJ. y ~ deben ser expresiones simples negativas (del tipo Eab y Oab), y debe ser una expresión elemental del tipo donde cada rJ.¡es una fórmula simple negativa. 11 Siendo relativa la elegancia y simplicidad de un cálculo, y no disponiendo de otras fuentes, he tomado como criterio de simplicidad, que ninguna regla supere en complejidad la regla de Slupecki. Criterio que me parece aceptable, ya que se trata de un cálculo más potente. 1.3. NOTAS A LA EXPOSICIÓN DE LUKASIEWICZ Finalmente hay que advertir que el prolongar la línea emprendida por Lukasiewicz no significa en modo alguno compartir todos sus planteamientos y motivaciones. Tres son principalmente las ideas sobre el tema que no puedo compartir: 1.0) Excesiva valoración de la recusación. 2.°) Desvaloración del método de los contraejemplos en Aristóteles, o tal vez de la interpretación en general. 3.°) La idea de que la existencia de fórmulas que no son verdaderas ni falsas depende únicamente de la presencia de variables libres, siendo inútil la recusación en la lógica de 2.° orden. Me ocuparé únicamente del último punto por ser central. «Sólo las proposiciones verdaderas pueden ser aseveradas, pues sería un error aseverar una proposición que no es verdadera. Una propiedad análoga no puede sostenerse de la recusación: no son sólo las proposiciones falsas que deben ser recusadas. Es verdad por supuesto que toda proposición es verdadera o falsa, pero existen expresiones proposicionales que no son verdaderas ni falsas. De tal clase son las llamadas funciones proposicionales, esto es, expre11 Lukasiewicz, J.: Op. cit., p. 104. ---- 462 Decidibilidad de la lógica de predicados... siones que contienen variables libres y resultan verdaderas para algunos de sus valores y falsas para otros." 12 Es evidente la asimetría señalada: sólo hay que aseverar las fórmulas válidas o lógicamente verdaderas, mientras que hay que rechazar tanto las fórmulas lógicamente falsas como las meramente satisfacibles. Lo que no es acertado es señalar como única causa de tal asimetría la presencia de variables libres. Ello supondría la inutilidad de la recusación en la lógica de segundo orden, donde todo enunciado sería verdadero o falso. Pero el que una fórmula de segundo orden sea satisfecha o no por una interpretación depende no sólo de la asignación de valores a las variables libres, sino también de la cardinalidad del dominio elegido. Si nos limitamos a un dominio dado D, sí que podemos afirmar que una fórmula de segundo orden sin variables libres es válida en D o bien no puede ser satisfecha en tal dominio D. Pero es evidente que existen enunciados de segundo orden meramente satisfacibles. Por ejemplo: VFVxVY(IFx A Fy) es una fórmula meramente satisfacible, que no puede ser satisfecha en los dominios de un solo ~lemento y que resulta válida para cualquier D, tal que 1J > 1. El no tener en cuenta el papel que juega la elección del dominio lleva a Lukasiewicz a afirmar que la introducción de cuantificadores en su formalización de la silogística haría innecesaria la recusación: "Introduciendo cuantificadores dentro del sistema podemos prescindir de la recusación. En lugar de recusar la forma (i) Abc A Eab ~ Iac podemos aseverar la tesis (k) VavbVc i(Abc A Eab ~ Iac) 12 Lukasiewicz, J.: Op. cit., p. 94. ----- - -- Decidibilidad de la lógica de predicados... 463 Esto significa: existen términos a, b y c que verifican la negación de (i). La fórmula (i), pues, no es verdadera para todo a, b y c,y no puede ser un silogismo válido". 13 Para facilitar la discusión podemos traducirlo al lenguaje del cálculo de predicados. Con ello no nos oponemos a la opinión de Lukasiewicz acerca del carácter especial de la silogística aristotélica, ya que este. carácter especial vendría dado por los axiomas. Tampoco es necesario adoptar como campo de interpretación conjuntos de círculos a la manera de Lukasie- wicz, ya que podemos establecer una biyección entre círculos y conjuntos. A su vez el número de conjuntos distintos determinables depende del número n de individuos del dominio. Por ejemplo para determinar dos conjuntos (o círculos) no vacuos precisamos un dominio de al menos 2 individuos, puesto que con un solo individuo el número de subconjuntos no vacuos del dominio es 21 l. Traduciremos las relaciones entre términos aristotélicos cAab~,cEab~, clab~, cOab~,respectivamentes por CAx(Fx-+ Gx)', CAx(Fx -+ ¡Gx!, CVx(FxA Gx!, CVx(FxA ¡Gx!. Las traducciones de (i) y (k) serán respectivamente - (i~) Ax(Gx -+ Hx) A Ax(Fx -+ ¡Gx) (k~) VFVGVH¡(Ax(Gx -+ Hx) -+ Vx(Fx A A -+ Vx(Fx A Hx) Ax(Fx -+ IGX) Hx) El que en este caso la fórmula (k') resulte válida 14 no demuestra el principio general de que la clausura existencial de la negación de una fórmula no válida resulta válida. Es fácil señalar contraejemplos como el modo inválido OOA de la primera figura. La fórmula a recusar sería: Vx(Gx A IHx) A Vx(Fx A ¡Gx) -+ Ax(Fx -+ Hx) y la clausura existencial de su negación: 13 Lukasiewicz, J.: Op. cit.~ p. 95. 14 En el sistema de Lukasiewicz no es válida por quedar los términos vacuos excluidos por los axiomas. -- -- - 464 Decidibilidad de la lógica de predicados... VFVGVHi(Vx(Gx A iHx) ~ Ax(Fx ~ A Vx(Fx A tGx) Hx)) que es equivalente a: VFVGVH(Vx(Gx A IHx) A Vx(Fx A Vx(Fx A IGX) I Hx)) Pero esta última fórmula no es universalmente válida, sino que es falsa en los dominios de un solo elemento. Frente al excesivo entusiasmo de Lukasiewicz por el método de la recusación, me parece que hay que limitarse a afirmar: a) La recusación axiomática es otro método de decisión. Es un enfoque digno de ser estudiado, pero no es un enfoque obligado. b) La recusación axiomática tiene los límites de todo método de decisión. c) La recusación axiomática no es un método de decisión puramente sintáctico. Para que un cálculo de recusación pueda considerarse una prueba de decidibilidad, debe demostrarse su completitud, además de su corrección. Y la prueba de completitud debe realizarse por medios semánticos. Además presupone la completitud semántica del calculo asertivo. 2. GRAMÁTICA, SINTAXIS Y SEMÁNTICA DE LA LÓGICA , DE PREDICADOS MONADICOS 2.1. TABLA DE SÍMBOLOS Constantes Conectivas: Lógicas: 1, A, V, ~, +~ Igualador: =. Cuantincadores: ------- V, A. - -- - Decidibilidad de la lógica de predicados... 465 Variables de predicado: F, G, H, 1, ], K, con o sin subíndices. Variables individuales: x, y, z, u, W, con o sin subíndices. 2.2. FÓRMULAS l. Una variable de predicado seguida de una variable individual es una fórmula. 11. Para cualesquiera variables individuales x, y, x = y es una fórmula. 111. Si a es una fórmula, entonces la IV. Si a. y ~ son fórmulas, entonces es una fórmula. (a A ~), (a v ~), (a. -4 ~), (a +-~ ~), son fórmulas. V. Si a es una fórmula, entonces para cualquier variable individual x, Axa. y Vxa son fórmulas. Diremos que a es el alcance del cuantwcador. AXI ... xna es abreviatura de AXI ... Axna. VXI... xna es abreviatura de VXl ... Vxna.. VI. Si a es una fórmula, entonces para cualquier variable de predicados F, AFa y VFa son fórmulas. a es el alcance del cuantWcador. Si y se ha formado por aplicación iterada de las reglas III y IV a partir de las fórmulas al, Q.2,..., an, diremos que y es una función veritativa de al, a.2, ..., ano Podemos considerar que las fórmulas de la lógica de predicados monádicos de l. er orden sin identidad son un subconjunto de las fórmulas de 2.0 orden, las formadas de acuerdo con las reglas 1, 111, IV, V. A fin de evitar un excesivo número de paréntesis se usarán las convenciones habituales: supresión del paréntesis exterior, supresión de paréntesis en las series de conjunciones o disyunciones, condicionador y bicondicionador separan más que coyuntor y disyuntor. Ejemplo de la última convención: a A ~ -4 Y es abreviatura de (a A ~) -4 y. 2.3. TERMINOLOGÍASINTÁCI'ICAADICIONAL Para abreviar las referencias a clases de fórmulas, es conveniente introducir las expresiones siguientes: - - --- - - ---- - - - - 466 Decidibilidad de la lógica de predicados... a) Fórmula elemental: fórmula atómica en que no ocurre el igualador. Son fórmulas atómicas las formadas de acuerdo con las reglas I y 11.Ejemplos de fórmula elemental: Fx, G1z. b) Expresión literal: es una fórmula elemental o negación de una fórmula elemental. Ejemplos: Fx, IG1z, Gz. c) Fórmula básica. Fórmula básica afirmativa: particularización (cuantificación existencial) de una conjunción de expresiones literales, con ocurrencia únicamente de la variable ligada por el cuantificador. Ejemplo: Vx(Fx A ¡Gx A Hx). Fórmula básica negativa: negación de una fórmula del tipo anterior. Ejemplo: jVx(Hx A IHx). d) P-componente. Una fórmula a es un P-componente de la fórmula ~ (siguiendo la nomenclatura de Church), si cumple las condiciones: i) a es una parte de ~; ii) a no ocurre en el alcance de un cuantificador de ~; iii) a no tiene ninguna de las formas I y, 'YA O, y v o, y -+ O, y ~* o. Ejemplo: v IHy)' 'Fx', 'Gx', 'Vy(Gy (1) son los P-componentes de (Fx v IGX) A (iFx Cualquier P-componente cuantificación. ~ Vy(Gy v iHy)) es una fórmula atómica o una e) P-fórmula o enunciado del CE asociado a una fórmula. Un enunciado ~ del CE (cálculo de enunciados) es una P-fórmula de a si y sólo si ~ puede obtenerse de a sustituyendo uniformemente las ocurrencias de cada P-componente en a por una letra enunciativa (P, Q, R, P1, ...), y además a puede obtenerse de ~ sustituyendo uniformemente cada letra enunciativa por una fórmula atómica o cuantmcación. La sustitución uniforme se define: supongamos que a' sustituye a a, y W cuando si a ~, entoncesal = W.Ejemplo:la P-fórmula == sustituye a ~, la sustitución es uniforme de (1) es (P v IQ) A (jp -+ R) - - --- Decidibilidad de la lógica de predicados... 467 f) Clausura. Una expresión es una serie de cuantmcadores si y sólo si es un cuantificador seguido de una variable, o bien es el resultado de anteponer un cuantificador seguido de una variable a una serie más corta. a es una clausura universal de ~ si y sólo si a es un enunciado y además o bien a ~ o bien a es el resultado de anteponer a ~ una serie de cuantmcadores universales. Ejemplo: tanto CAyA(Fx v IGy)' como CAxAy(Fxv IGy)" son clausuras universales de CFxv ley'. Análoga definición puede tomarse para clausura particular. = 2.4. SUSTITUCIÓN DE VARIABLES y FÓRMULAS Algunas reglas, como la de especificación universal, permiten la sustitución de una variable por otra o por un término. La sustitución es una aplicación que a cada secuencia formada por una variable, un término y una expresión, atribuye unívocamente una expresión. Usaré el signo S para la operación de sustitución, escribiendo S ~ o. en vez de S (x, 8, (J.).Para una definición recursiva de dicho operador, adaptándola a la lógica de 2.0 orden, nos podemos remitir a la exposición de J. Mosterín.15 Al formular las reglas de recusación se usará la operación de sustitución de una fórmula (que es parte de otra) por una fórmula, en la lógica de l.er orden. Definición de S para fórmulas elementales: sean F, G, letras de predicado cualesquiera, sean x, y, variables individuales cualesquiera, sea O. una fórmula abierta con ocurrencia solamente de la variable x. SFZ Gy { SFZ y SFz I a, si F == G, x Gy, si F == G o bien x == Y =y = z == y = z ~ == -, SF:r ~ . 15 Mosterin, J.: Lógica de primer orden. Barcelona, Ariel, 1970, pp. 41-43. 9 ¡ [,J 468 Decidibilidad de la lógica de predicados... i I" 1,1 ( S ¡ i A S1r ( I 1I j .111 1I i y) V y) SFIr ( S1r ( y) y) SFIr Az = 11" SF47 Vz . = S1r == S == == Az = VZ A V SaJ y S Ir Y S1r S1r y SF47 S Fa! y S 47 47 SFz. " II1 2.5. . 1II1 I il' SINTAXIS DE LA LÓGICA DE PREDICADOS MONÁDICOS Siguiendo la idea de Lukasiewicz, adoptaremos entre otras la regla recusativa de separación, que permite recusar una fórmula a partir de una tesis y de una fórmula previamente recusada. Por ello resulta necesario proponer un cálculo deductivo de aserción. Puede ser cualquier axiomatización correcta y completa. Para concretar he adoptado el ,( '''11 sistema presentado por Rogers, 16 con las simplificaciones oportunas al no tener en cuenta predicados poliádicos, functores ni constantes. 2.6. SEMÁNTICA DE LA LÓGICA DE PREDICADOS MONÁDICOS Al presentar un método de decisión para el cálculo de predicados monádicos, la mayoría de los autores lo formulan primariamente para los enunciados, ya que para ellos se definen primariamente verdad y validez. Siempre se puede hallar derivativamente la validez de fórmulas abiertas: las fórmulas con variables libres se llaman válidas si y sólo si su clausura universal es válida. En cambio en un cálculo de recusación parece mejor plantear la recusación directamente de fórmulas con variables libres. Igual que el cálculo de aserción permite deducir fórmulas abiertas, el cálculo de recusación debe permitir 1111: 11I1 iili d' derivar fórmulas insatisfacibles como 'Fx A ,Fx' o incluso fórmulas abiertas meramente satisfacibles como 'Fx A '"lGx'. Tomaremos como punto de partida la definición de interpre16 Rogers, R.: Mathematical logic and formalized theories. Amsterdam, North-Holand P. Co., 1971, pp. 43-45 Y 87-89. 1111 1!lli - - - - - - - Decidibilidad de la lógica de predicados... 469 tación (simbolizada por 1) y de satisfacción que figura en la obra citada de J. Mosterín,17 modificando la definición de verdad para la lógica de 1.er orden: una fórmula a. es verdadera bajo la interpretación 1, si y sólo si toda interpretación que coincide enteramente con!, con la posible excepción de la asignación de individuos de D a las variables, satisface a.. Para la lógica de 2.0 orden la definición de verdad queda: una fórmula a. es verdadera en D o válida en D, si y sólo si toda interpretación sobre D satisface a.. Para la semántica de la lógica de predicados de 2.0 orden se ha tenido especialmente en cuenta la exposición de Rogers. 18 3. DEClDmn..IDAD DE PRIMER DE LA LÓGICA DE PREDICADOS MONÁDICOS , ORDEN SIN IDENTIDAD MEDIANTE LA RECUSACION Se proponen los siguientes axiomas y reglas para hallar todas y solas las fórmulas no válidas de la lógica de predicados monádicos de 1.er orden. 3.1. AxIOMA ARl 3.2. ~ Fx REGLAS .RRl (regla recusativa de separación) !-fa. RR2 (regla recusativa de sustitución) bL SI3 a. Fx 17 Mosterin, donde F es una letra de predicado ~ es una fórmula abierta con ocurrencia de la sola variable x. cualquiera y J.: Op. cit., pp. 107 Y ss. 18 Rogers, R.: Op. cit., pp. 90 Y ss. r 470 Decidibilidad de la lógica de predicados... RR3 (regla recusativa de particularización) ~a. '11 I I I ~ Vxa. donde a. es una fórmula abierta en la que sólo ocurre la variable x. RR4 (regla recusativa de adición) donde aI, a2 son fórmulas básicas afirmativas, y f1 es una fórmula básica o disyunción de fórmulas básicas. RR5 (regla recusativa de especificación) bt- Axa ~a. 3.3. PRUEBA DE RECUSACIÓN Una prueba de recusación o simplemente recusación es una secuencia finita de líneas, cada una de las cuales es: a) una tesis del cálculo asertivo; b) un axioma de recusación; o bien c) una fórmula que se obtiene de las anteriores por aplicación de las reglas de recusación RRI-RR5. Las fórmulas de los grupos b) y c) van precedidas del signo de recusación '~', las del tipo a) van precedidas del signo' r-'. 1111'I 3.4. JUSTIFICACIÓNDE LAS RESTRICCIONES Es frecuente .que las reglas que versan acerca de cuantificadores tengan restricciones. Pero pueden parecer excesivamente complicadas las restricciones impuestas a RR4. Se exige que al y a2 sean fórmulas básicas afirmativas, como por ejemplo 'Vx(Fx A jCx A I Hx)'. El motivo de tal restricción no es dar una regla lo más débil posible, sino que al disminuir las restricciones se vuelve incorrecta. Ampliemos al grado inmediatamente superior de complejidad la clase de fórmulas a la que pueden pertenecer al y tX.2.Esto es, permitamos que al y a2 sean fórmulas básicas negativas. 1111 - - - -- -- - Decidibilidad de la lógica de predicados... = Hagamos: al ~ Vx(iFx = A IVx(Fx A Gx), a2 Gx) v VX(IFx = -'Vx(Fx A 471 I Gx), A I Gx). Vamos a probar: ~ 2.o no es válida I a.2v ~ 1.o no es válida I al v 3.o es en cambio válida 1.o I t1.2v I al v ~ La fórmula I al v ~, esto es IIVx(Fx A Gx) v VX(IFx A Gx) v Vx(l Fx A IGx) equivale a Vx(Fx A Gx) v Vx(-'Fx A Gx) v Vx(-'Fx A -'Gx) que por ser una disyunción de fórmulas básicas afirmativas será válida si y sólo si es válida la disyunción de matrices (Fx A Gx) v (IFx A Gx) v (-'Fx A ¡Gx) que por ser el desarro1lo incompleto en forma normal perfecta no es válido. 2.o Se procede análogamente. 3.o Si ampiáramos RR4 a fórmulas básicas negativas, como son en este caso al y a2, la regla sería incorrecta pues, partiendo de fórmulas no válidas, permitiría 1legar a la fórmula válida J al v I a2 v ~, que equivale a Vx(Fx A Gx) v Vx(Fx A IGx) v Vx(-'Fx v Vx(-'Fx A-'Gx) A Gx) que es válida por ser el desarrollo completo en forma normal perfecta. 19 Las restricciones impuestas a RR2 son fácilmente comprensibles por corresponder a idénticas restricciones en la 19 Herbrand, J.: Écrits logiques. Paris, P. U. F., 1968, pp. 82-84 Y 196. - - - - 472 I I Decidibilidad de la lógica de predicados... regla inversa para el cálculo asertivo, usada por Quine como I I regla derivada. ¡¡: 20 Tampoco la formulación de RR3 puede ser tan fuerte .que permita la ocurrencia en a de otras variables libres, además de x, sin volverse incorrecta. Evidentemente no es válida la fórmula ~Gx v IGy', que no es válida en dominios tales que D > 2. Pero ampliando RR2 podríamos pasar a la recusación de ~vx(Gx v I Gy)' a pesar de tratarse de una fórmula válida: para cualquier interpretación l existirá un aED tal que I~sat Gx v IGy. Basta hacer a = ! (y). 3.5. PRUEBA DE COMPLETITUD DEL CÁLCULO DE RECUSACIÓN EN , LA LOGICA DE PRIMER ORDEN La prueba de completitud sigue la línea siguiente: toda fórmula a tiene al menos una fórmula normal equivalente a'. Por ser equivalentes la recusación de al lleva aparejada la recusación de a por RR1 y el teorema asertivo a ~ a'. El segundo paso consiste en demostrar que todas las fórmulas normales no válidas pueden ser recusadas. 1' 11 1 I 3.5.1. FÓRMULASNORMALES Una fórmula está en forma normal si y sólo si cumple simultáneamente l,as cuatro condiciones siguientes: 1) No ocurren las constantes lógicas ~~',~ ~', 'A'. 2) La negación sólo afecta a fórmulas elementales o a particularizaciones. 3) El cuantmcador sólo afecta a expresiones literales o a conjunciones de expresiones literales. 4) La disyunción no afecta a la conjunción. Atendiendo a los límites de esta exposición se omite la prueba por inducción semiótica de que a cada fórmula corresponde al menos una fórmula normal 11 equivalente. 21 20 Quine, W. Methods of logic. Nueva York, Holt, Rinehart and Winston. Reed. 1963, p. 99. 21 Tal normalización procede de Behmann y es usada con las diferencias adecuadas por Hilbert-Ackermann para el cálculo de clases y por Quine para el análisis de satisfacibilidad. -- - -- -- - -- Decidibilidad de la lógica de predicados... 473 Aplicando la definición de fórmula normal, podemos or. denar por niveles los enunciados normales. Ya que por defi. nición en los enunciados normales ocurre una sola variab]e en el alcance de cada cuantificador, es posible reinscribir las variables usando solamente la variable x. Los niveles en que podemos estratificar los enunciados normales son: EN!. Fórmula básica afirmativa. Ejemplo: Vx(Fx EN2. A Gx A IHx) Fórmula básica negativa. Ejemplo: IVx(Fx EN3. plo: A Gx A IHx) Disyunción de fórmulas básicas afirmativas. Ejem- Vx(F1x A F2x A ... A 1Fnx) v Vx(Gx A IHx) v VxGx EN4. plo: Disyunción de fórmulas básicas negativas. EjemIVx(Fx A Hx) v IVx(IFx A Gx A IHx) v... v IVx(Fx A IGX) EN5. Disyunción de una fórmula básica negativa con otra u otras fórmulas básicas afirmativas. Ejemplo: Vx(Fx A Gx) v VXIFx v ... v Vx(Gx v IVx(IFx A Hx) A Hx) EN6. Disyunción de n fórmulas básicas negativas con m fórmulas básicas afirmativas (para n > 2 Y m > 1). Ejemplo: Vx(Fx A Hx) v VX(IFx A IGX) v I Vx(Fx A IGX) v IVxHx EN7. Conjunción de enunciados de las formas EN1EN6. El caso más complejo es una conjunción de disyunciones de fórmulas básicas. Ejemplo: -- - - - -- - - - - .. c t t ' \1 . 1I i¡ l' I l.. ... Ií' !! 474 iI Decidibaidad I de la lógica de predicados... (Vx(Fx A Gx) v Vx-,Gx v -'Vx(Fx A (VxGx v Vx(Fx A -'Hx)) A Hx)) 3.5.2. . V ALIDEZ DE FÓRMULAS Se resumen sin demostración las proposiciones acerca de la validez de fórmulas, necesarias para fundamentar la completitud y corrección. 1) Ninguna fórmula básica afirmativa es válida. 2) Una fórmula básica negativa es válida si y sólo si contiene una fórmula elemental y su negación. 3) La disyunción de fórmulas básicas afirmativas es válida si y sólo si el resultado de borrar los cuantincadores es válido veritativo-funcionalmente. 4) La disyunción de fórmulas básicas negativas es válida si y sólo si al menos uno de los disyuntos es válido. 5) La disyunción de una fórmula básica negativa con otra u otras fórmulas básicas afirmativas es válida, si y sólo si el resultado de borrar los cuantincadores es tautológico. 6) Una expresión de la forma -, VX~l V .oo v -, Vx~n V VXY1 V .oo v VxYn es válida si y sólo si por lo menos es válida alguna de las expresiones siguientes (1) -, VX~l v VXYl V (2) -, Vxfk (n) -'Vx~n V VXYl V V VXYl V ... V VXYn .oo oo. V VXYn V VXYn 7) Una conjunción de fórmulas es válida si y sólo si todos los conyuntos son válidos. 3.5.3. TEOREMAS DE COMPLETITUD Teorema 1. Si el cálculo de recusación permite obtener todos los enunciados no válidos, entonces permite obtener todas las fórmulas no válidas. Considérese cualquier fórmula abierta no válida a. Su clausura universal al no es válida. Por hipótesis del teorema al será recusable, por ser enunciaI '111 ---- Decidibilidad de la lógica de predicados... 475 do. Por. aplicación iterada de RR5 a ~lse llega a la recusación de ~. Teorema 2. Si el cálculo de recusación permite recusar todos los enunciados en forma normal que no son válidos, entonces permite recusar todos los enunciados no válidos. Sea ~ un enunciado cualquiera no válido y sea ~' su forma normal. ~ puede ser recusado mediante ~ ~ ~' Y aplicación de RRl. r- Estos dos teoremas permiten centrar el problema en los enunciados en forma normal. Teorema 3. El cálculo de recusación permite recusar todas las fórmulas básicas afirmativas. Si contiene al menos una fórmula atómica no negada, se propone el siguiente esquema de recusación (sea cada q>¡una expresión literal): (1) r- VX(q>lA ... A F¡x A ... A q>n)~ VxF¡x Teorema asertivo (2)~ (3)~ (4)~ (5)~ Fx Fix VxF¡x VX(q>lA ... AR1 (2) RR2 F¡xf Fx (3) RR3 A F¡x A ...A (1), (4) RR1 q>n) Si contiene al menos una fórmula atómica negada, el esquema es análogo partiendo (2) rf VxF iX (3)~ VXI IF¡x (4)I-f (5)t-f ~ VXI "lF¡x Vx"l F¡x VxF¡x de lf . VXIF¡x. recusado arriba teorema asertivo (2), (3) RRl (4) RR2 Fixf "lFix Teorema 4. El cálculo de recusación permite recusar todas las fórmulas básicas negativas no válidas (que nQ contengan una fórmula elemental y su negación). Esquema propuesto: (1)~ (2)r(3)~ (4)l-f Fx "1"1Fx ~ Fx "I,Fx "lFx ARl teorema asertivo (1), (2) RRl (3) RR2 Fx/ ,Fx -- - - - 476 Decidibilidad de la. lógica de predicados... (5) ~ I(Fx A ...A Fx A IIFx.A ¡ 11 ¡ 1I (6) ~ I(Fx A ... A IIFx) teorema asertivo ~ -,Fx ... A Fx A I IFx A ... A IIFx) (4), (5)RR1 (7) ~ I(F1x A ... A FnXA ,G1x A ... A IGmX) (6)RR2 F¡xf Fx, G¡xf I Fx (8) ~ Ax(J.,~ S~ (J.,. teorema (9) ~ AXI(F1x A ... A Fnx A ,Gtx A ... A asertivo ,Gmx) (7), (8) RR1 (10) ~ 1 VX(J., ~ AXI(J., teorema asertivo (11) b' IVx(F1x A ... A Fnx A ,G1x A... A 1 Gmx) (9), (10) RR1 . 11 1I 1 I Teorema 5. El cálculo de recusación permite recusar la disyunción de fórmulas básicas afirmativas si no es válida (si el resultado de borrar los cuantmcadores no es una tautología). Sea (J.,la disyunción de fórmulas y ~ el resultado de borrar los cuantificadores. Por hipótesis ~ no es válido y está en forma normal disyuntiva. Se transforma ~ en su equivalente (3' en forma normal conyuntiva. Por no ser válido tendrá al menos un conyunto que no contendrá la misma fórmula elemental afirmada y negada. Dicho conyunto tendrá la forma el esquema de recusación puede ser: (1) Ir Fx AR1 (2) r Fx v ... v Fx v ,'"l Fx v ... v 11 Fx ~ Fx teorema asertivo (3) ~ Fx v...vFxv IIFx v ...v IIFx (1), (2) RR1 (4) Ir F1x v... v Fnx v IG1X V... V ,Gnx (3)RR2 F¡xfFx, G¡xf IFx (5) r W~ F1x v ... v Fnx v IG1X v... v,Gnx teorema asertivo (6)~ W (4), (5) RR1 -- - Decidibilidad de la lógica de predicados... (7) r- 477 teorema asertivo W (8) bl (9) bl Vx (6), (7) RR1 (8) RR3 Sabemos que ~ es una disyunción de fórmulas básicas que podemos representar por ~1 v ... v ~p' La línea (9) tiene la estructura (9) b' VX(~lv... V ~p) (10) r- VX~lv... VVx~p~ VX(~l v... V ~p) teorema asertivo (9), (10) RR1 Pero la línea (11) es exactamente la fórmula a recusar rJ... Teorema 6. La disyunción de fórmulas básicas negativas es recusable si no es válida (si ninguno de los disyuntos es válido). Sea cada -,VxrJ..¡uno de los disyuntos. Por hipótesis no son válidos y recusables por el teorema 4. Sea ~ la fórmula insatisfacible 'Vx(Fx I VxrJ..¡V ~ -', I IFx)', entonces la fórmula A VxrJ..¡es un teorema asertivo. Por RR1 pode- mos recusar cada I VxrJ..¡v ~. Por aplicaciones sucesivas de RR4 tenemos r- I VxrJ..'2 v I VX(J.lV r- I VXrJ..g ~ v -, VXrJ..2 V -, VXrJ..l V ~ . r- I VXrJ..nV ... v IXrJ..2 V I finalmente como y tenemos ~ y V ~ es un r- IVXrJ..nv... V IXtX.2 V I Teorema 7. VXrJ..lV ~ teorema asertivo, por RR1 VXrJ..l Todas las expresiones de la forma (donde cada rJ..¡es una conjunción de expresiones literales) son recusables si no son válidas (si el resultado ~ de borrar - - - - - -- 478 Decidibi.lidad de la lógica de predicados... los cuantificadores no es tautológico). La demostración es análoga a la del teoren1a 5. Para completada, el teorema Vxal v Vxa'2 v ... V Vxan ~ Vx I al v VX2a2 v ... v Vxan r-I junto con RRl nos permite llegar al resultado esperado Teoren1a 8. Una expresión de la forma (siendo ~¡, Y¡ conjunciones de expresiones literales) es recusable si no es válida; esto es, si no es válida ninguna de las expresiones: (1) IVX~l (2) I Vx(3.~v VXYl V .., V VXYrn V VXYl v.,. V VXYrn .. (n) I VX~n V VXYl V ... V VXYrn Al no ser válidas por hipótesis, las expresiones (1), (2), .. " (11) son recusables por el teorema 7. Por RR4 es recusable -, VX~l V .., v -, VX~nV VXYlV ... V VXYrn Teorema 9. Una conjunción de disyunciones de fórmulas básicas es recusable si no es una fórmula válida (si alguno de los conyuntos no es válido). Si alguno de los conyuntas ai no es válido, será recusable en virtud de los teoremas anteriores. Los últimos pasos pueden ser: r- al V Ir ai I-f al - -- V .., V ai V ... V an ... V ai V... V an ~ ai teorema asertivo ya recusado RR1 -- -- D"cidibilidad de la lógica de predicados... 3.6. 479 LA CORRECCIÓN DEL CÁLCULO DE RECUSACIÓN PARA LA I I LOGICA DE PREDICADOS MONADICOS DE PRIMER ORDEN El único axioma de recusación es trivialmente no válido. Se puede demostrar que las reglas de recusación preservan la no validez. Para RRI, RR2, RR5 la demostración y parte de la corrección de una regla inversa en el cálculo aserti- vo. 22 Si las fórmulas recusadas fuesen válidas, lo serían contra la hipótesis respectivamente ~, S~ a, Axa. Para demostrar la corrección de RR3 tengamos en cuenta las restricciones. Si a es una fórmula abierta con ocurrencia solamente de la variable x (por tanto no contiene ningún cuantificador) y además es una fórmula no válida, entonces su P-fórmula no es tautológica y existirá una interpretación 11 que no la satisface. Entonces podrá construirse una interpretación! tal que 1 no sato Vxa. Los conjuntos asig- nados a una letra predicativa cualquiera serán !(F) I(F) Es evidente que =D =~ 1 no si I1(F) = T si 11(F) = .L sato Vxa pues no existe ningún aED tal que 1 ~ sato a~ . En el caso de RR4 las restricciones estipulan que ~ es una fórmula básica o disyunción de fórmulas básicas. Por lo tanto pertenece a una de las siguientes clases de fórmulas: i) Fórmula básica afirmativa. ii) Fórmula básica negativa. iii) Disyunción de fórmulas básicas afirmativas. iv) Disyunción de fórmulas básicas negativas. v) Disyunción de una fórmula básica negativa con fórmulas básicas afirmativas. vi) Disyunción de fórmulas básicas afirmativas y negativas. Demostrando la corrección de RR4 para cada uno de estos casos habremos demostrado la corrección de RR4 en general. A título de ejemplo daremos la demostración para el primer caso. Sean al y a2 fórmulas básicas afirmativas lo mismo que ~. Por hipótesis no son válidas 22 Para RR2 ver Quine, W.: Methods of logic, 1963, p. 99. 480 Decidibilidad de la lógica de predicados... (1) 1a.1 v ~ (2) lat2 v ~ tenemos que demostrar que bajo esta hipótesis no es válida Según los teoremas de validez existirá una interpretación veritativo funcional 11 que no satisface la fórmula resultante de (1) al borrar los cuantificadores. Igualmente existirá una interpretación ~2 que no satisface la fórmula que resulta de borrar los cuantificadores en (2). Puede construirse una interpretación ! que no satisface (3). La interpretación será: D = {1, 2}, sea Fj cualquiera de los relatores que ocurren en (3) y sea i cualquiera de los elementos del dominio D. Entonces 1 E (F) 4. y s.s. IlFj) = T DECIDIBILIDAD DE LA LÓGICA DE PREDICADOS MONÁDICOS DE 4.1. si 2.0 ORDEN CON IDENTIDAD MEDIANTE LA RECUSACIÓN ENUNCIADOS BÁSICOS DE IDENTIDAD Llamaremos enunciados básicos de identidad a los que tengan una de las dos formas siguientes: donde ocurren todas las fórmulas de la forma Xi ;é Xj, tales que i < j. Su sentido intuitivo es que existen al menos m individuos en el universo: D > m. en la matriz ocurren todas las fórmulas je tales que i --- --- - < la forma Xi j. Su sentido intuitivo es D < n - = Xj 1. -- -- -- Decidibilidad de la lógica de predicados... Adaptando las abreviaturas de Hilbert-Bernays 481 a las fórmulas de identidad, vamos a convenir que para m > 2, n > 2, la expresión cym(x ~ x')' es una abreviatura de (1) y la expresión CAn(x = x')' es una abreviatura de (2). 23 4.2. AxIOMAS 24 Se proponen los siguientes esquemas axiomáticos. Sean x, y, variables individuales cualesquiera, sean m, n, números naturales, m > 2 Y n > 2 AR21 1+ YxYyx ~ y AR22 1+ ym(x ~ 4.3. x') v An(x = x') SI n < m REGLAS RR21 (Regla recusativa de separación) RR22 (Regla recusativa de especificación universal) sea e cualquier variable. r4.4. (J. CORRECCIÓN DEL CÁLCULO DE RECUSACIÓN PARA LA LÓGICA I DE PREDICADOS MONADICOS DE SEGUNDO ORDEN Los axiomas de recusación son fórmulas no válidas. Bas~ ta considerar cualquier interpretación con D = 1, para com- probar la no validez de AR21. El axioma AR22 tampoco es válido. Resultará falso para toda interpretación que cumpla . su negaclon I 23 Hilbert-Bernays. Grundlagen der Mathematik. Vol. 1, Berlín, J. Springer, 1934, p. 174. 24 El axioma AR21 puede - --- - -- derivarse de AR22. --- 482 Decidibilidad de la lógica de predicados... iym(x ~ x') v An(x = x')) siendo n < m que equivale a -,ym(x ~ x') A iAn(x = X') Am(x = X') A yn(x = X') siendo n < m siendo n < m pero_la última fórmula es claramente satisfacible, basta hacer D = n = ID - 1, ya que la fórmula significa que existen exactamente n objetos en el universo. Las reglas de recusación preservan la no validez. Su corrección se basa en la de la regla inversa del cálculo asertivo. 4.5. COMPLETlTUD DEL CÁLCULO DE RECUSACIÓNPARA LA LÓGI, CA DE PREDICADOS MONADICOS CON IDENTIDAD DE SEGUNDO ORDEN Podemos partir de la normalización mann. 20 A partir de los teoremas -,yn(x An(x = x') iAn(x = x') +--+ yn(x ~ x') yn+k(x ~ x') ~ yn(x ~ x') An(x = x') ~ An+k(x = x') de Skolem 25 y Beh- ~ x~) ~ para k > O para k > O se demuestra que un enunciado normal de Skolem, que no se reduce previamente a una fórmula válida o insatisfacible, se puede reducir a una fórmula en forma normal conyuntiva, cuyos conyuntos tienen una de las tres formas siguientes: 1) yn(x ~ x~) 11) An(x = x') 111) ym(x ~ x') v An(x = x'). Podemos plantear los siguientes casos para una fórmula: 25 Skolem, Th.: Selected works in logic, 1970, p. 97. 26 Behmann, H.: «Beitrage zur Algebra der Logik, insbesondere zum entscheidungsproblem". Math Annalen, 86, 1922, p. 225. Decidibilidad de la lógica de predicados... 483 Caso 1. Se reduce a una fórmula válida y no debe ser recusada. Caso 2. La fórmula a se reduce a una fónnula insatisfacible. Su negación "1a es un teorema. El esquema de recusación puede ser (1) ~ la. (2) ~ a ~ YxYyx ~ y (3) bl- YxYyx ~ y (4) ~ a por hipótesis teorema asertivo AR21 (2), (3) RR21 Caso 3. Si a se reduce a un enunciado del tipo 1, el esquema de recusación puede ser (1) (2) (3) (4) (5) 1- ym(x ~ x') ~ YxYyx ~ y bl YxYyx ~ y I-f-ym(x ~ x') 1- a ~ ym(x ~ x') ¡,t a Caso 4. Si se reduce a un enunciado del tipo quema de recusación (1) AR21 (1), (2) RR21 normalización (3), (4) RR21 If.- yn+l(x ~ x') 11, el es- puede ser v An(x = x') (2) ~ An(x = x') ~ yn+l((x ~ x') v An(x = x')) (3) bl An(x = x') teorema asertivo (1), (2), RR21 ... ... ... ... ... ... ... ... Caso 5. Se reduce a un enunciadG del tipo 111. Tal enunciado no será válido si n < m. En este caso es fácilmente recusable por el esquema axiomático AR22. Caso 6. a se reduce a a', que es una conjunción de enunciados de los tipos 1-111.Hagamos a' == ~1 A fk A ... A ~n' Si al no es válido existirá !tal menos un conyunto que no es válido, por ejemplo ~i' El esquema de recusación puede ser I (1) I-f ~i (2) 1- ~1 A ~2 A ... I (3) 1-1 ~1 I 10 t A ~2 A ... A A ~n ~n ~ ~i por los casos 3-5 teorema asertivo (1), (2), RR21 I! 484 Decidibilidad de la lógica de predicados... (4) 1- a (5) I-f i! \! ! i, 1 : 1' : .11I 1 1 I a ~ a' normalización (3), (4) RR21 Finalmente una fórmula abierta es válida si y sólo si su clausura universal es válida. Si dicha clausura no es válida será recusable por los casos 2-6. A partir de aquí, la fórmula abierta será recusable por RR22. - -