Download DECIDIBILIDAD DE LA LOGICA DE PREDICADOS MONADICOS

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.
-
-