Transformación de fórmulas (Cálculo de predicados)

Transformación de fórmulas del cálculo de predicados

Transformación de fórmulas del cálculo de predicados: En las “Formas normales proposicionales” La relación de equivalencia establece, para cada fórmula, una clase de equivalencia. Dentro de cada una de estas clases, hay un conjunto de miembros (fórmulas) que poseen una estructura particular que las hace objeto de especial interés. Estas son las formas normales (...). Evidentemente, si la relación “equivalencia lógica“ está presente también en los Cálculos de predicados, es lógico esperar que exista algún tipo de “Forma normal” entre las fórmulas del cálculo de predicados.

Forma normal prenexada.

Una fórmula del cálculo de predicados, se dice que está en forma normal prenexada, si es de la forma:
Q(x1)Q(x2)... Q(xn)M
Donde cada Q(xi) es un cuantificador ( o ), mientras M es una fórmula sin cuantificadores y en forma normal conjuntiva, de M se dice que es la matriz de la fórmula. Los siguientes son ejemplos de formas normales prenexadas:
a)Ɐ(x)∃(y)[(¬P(x, y) v R(x)) ʌ (P(y, x)v¬R(y))]
b)Ɐ(x)∃(y)[P(x, y) ʌ (¬P(y, x) v R(y))]
c)Ɐ(x)∃(y)[P(y, x) v ¬R(y)]
d)Ɐ(x)∃(y) P(y, x)
e)P(a, b) ʌ (¬P(b, a)v R(b))
Sin embargo, las fórmulas que a continuación se presentan no están en forma normal prenexada:
a)Ɐ(x)[ ∃(y)(¬P(x, y) v R(x)) ʌ ¬R(x)]
b)Ɐ(x) ∃(y) [(¬P(x, y) ʌ R(x)) v ¬R(x)]
En el caso a), el cuantificador existencial (∃(y)) no afecta a toda la forma normal conjuntiva o visto de otro modo, en la matriz está presente un cuantificador. En el caso b), los cuantificadores están bien posicionados, pero la matriz no está en forma normal conjuntiva.
Aunque evidentemente no toda fórmula del cálculo de predicados es una forma normal prenexada, sí puede encontrarse para cada una, otra fórmula que le sea lógicamente equivalente y esté en forma normal prenexada. El modo de lograr esto es a través de las leyes de equivalencia estudiadas siguiendo el orden lógico que aparece a continuación:
1.Eliminar todas las condicionales ( → ) y bicondicionales ( ⇔ ). Para esto se aplican tantas veces como sea necesario las leyes:
A → B ⇔ ¬A v B
A ↔ B ⇔ A → B ʌ B → A
2.Remover las negaciones (¬) hacia el interior de la matriz, hasta que afecten sólo a átomos. Esto se hace apoyándose en las leyes de D` Morgan, las leyes de D` Morgan generalizadas y la ley de la doble negación:
¬ (A ʌ B) ⇔ ¬A v¬B
¬ (A v B) ⇔ ¬A ʌ ¬B
¬Ɐ(x)A(x) ⇔ ∃(x)¬A(x)
Ɐ(x) ¬A(x) ⇔ ¬∃(x)A(x)
¬¬A ⇔ A
3.Remover los cuantificadores (Ɐ, ∃) a la izquierda, aumentando su alcance hasta que cada uno afecte a toda la matriz. Las leyes que posibilitan este objetivo son:
Ɐ(x)A(x) v B ⇔ Ɐ(x)[A(x) v B]
∃(x)A(x) v B ⇔ ∃(x)[A(x) v B]
Ɐ(x)A(x) ʌ B ⇔ Ɐ(x)[A(x) ʌ B]
∃(x)A(x) ʌ B ⇔ ∃(x)[A(x) ʌ B]
Ɐ(x)A(x) ʌ Ɐ(x)B(x) ⇔ Ɐ(x)[A(x) ʌ B(x)]
∃(x)A(x) v∃(x)B(x) ⇔ ∃(x)[A(x) v B(x)]
Ɐ(x)A(x) ⇔ Ɐ(y)A(y)
∃(x)A(x) ⇔ ∃(y)A(y)
4.Transformar la matriz en una forma normal conjuntiva. Debido a que llegado a este paso, en la matriz las negaciones sólo afectan a literales y no existen condicionales ni bicondicionales, lo único que es necesario para obtener una forma normal conjuntiva es aplicar las leyes distributivas convenientemente:
A ʌ (B v C) ⇔ (A ʌ B) v(A ʌ C)
A v (B ʌ C) ⇔ (A v B) ʌ (A v C)
El siguiente ejemplo ilustra como transformar una fórmula del cálculo de predicados en una forma normal prenexada equivalente:
Sea la fórmula Ɐ(x)Ɐ(y)[S(x, y) ↔ Ɐ(z)[P(z, x) → P(z, y)]]
Primeramente se elimina la doble implicación, quedando:
Ɐ(x)Ɐ(y)[(S(x, y) → Ɐ(z)[P(z, x) → P(z, y)]) ʌ (Ɐ(z)[P(z, x) → P(z, y)] → S(x, y))]
Acto seguido se eliminan las implicaciones, resultando:
Ɐ(x)Ɐ(y)[(¬S(x, y) v Ɐ(z)[¬P(z, x) v P(z, y)]) ʌ (¬Ɐ(z)[¬P(z, x) v P(z, y)] v S(x, y))]
El próximo paso es remover los negadores hacia el interior de la matriz, buscando que afecten sólo átomos, en este caso se tiene simplemente un negador que no afecta un átomo (¬Ɐ(z)[... ), al aplicar la ley de D’ Morgan (Augustus De Morgan) generalizada se obtiene:
Ɐ(x)Ɐ(y)[(¬S(x, y) v Ɐ(z)[¬P(z, x) v P(z, y)]) ʌ (∃(z)¬ [¬P(z, x) v P(z, y)] v S(x, y))]
Como puede apreciarse, aún el negador no afecta directamente un átomo, lo que hace necesario aplicar la ley de D’ Morgan para obtener:
Ɐ(x)Ɐ(y)[(¬S(x, y) v Ɐ(z)[¬P(z, x) v P(z, y)]) ʌ (∃(z)[P(z, x) ʌ ¬P(z, y)] v S(x, y))]
Una vez que todos los negadores afectan sólo átomos, es necesario remover los cuantificadores hacia la izquierda, en este caso primeramente el cuantificador existencial (puede ser cualquiera), quedando en un primer paso:
Ɐ(x)Ɐ(y)[(¬S(x, y) v Ɐ(z)[¬P(z, x) v P(z, y)]) ʌ ∃(z)([P(z, x) ʌ ¬P(z, y)] v S(x, y))]
Es necesario un segundo paso para seguir aumentando el alcance del cuantificador, como resultado de este se obtiene:
Ɐ(x)Ɐ(y)∃(z)[(¬S(x, y) v Ɐ(z)[¬P(z, x) v P(z, y)]) ʌ ([P(z, x) ʌ ¬P(z, y)] v S(x, y))]
Todavía queda un cuantificador en la matriz, el primer paso para removerlo fuera da como resultado:
Ɐ(x)Ɐ(y)∃(z)[Ɐ(z)(¬S(x, y) v[¬P(z, x) v P(z, y)]) ʌ ([P(z, x) ʌ ¬P(z, y)] v S(x, y))]
Antes de dar el próximo paso para extraer el cuantificador de la matriz, hay que resolver el problema que se presenta al ocurrir libre z en:
[P(z, x) ʌ ¬P(z, y)] v S(x, y)
Un modo de resolverlo es sustituyendo z en Ɐ(z)(¬S(x,... ) por otra variable no utilizada en la fórmula, en este caso v:
Ɐ(x)Ɐ(y)∃(z)[Ɐ(v)(¬S(x, y) v[¬P(v, x) v P(v, y)]) ʌ ([P(z, x) ʌ ¬P(z, y)] v S(x, y))]
Ahora ya es posible terminar de extraer el cuantificador de la matriz:
Ɐ(x)Ɐ(y)∃(z)Ɐ(v)[(¬S(x, y) v [¬P(v, x) v P(v, y)]) ʌ ([P(z, x) ʌ ¬P(z, y)] v S(x, y))]
Para finalmente obtener la forma normal prenexada sólo hay que transformar la matriz en una forma normal conjuntiva, lo que se logra mediante la ley distributiva:
Ɐ(x)Ɐ(y)∃(z)Ɐ(v)[(¬S(x, y) v ¬P(v, x) v P(v, y)) ʌ (P(z, x) v S(x, y)) ʌ (¬P(z, y) v S(x, y))]

Forma de Skölem

La forma de Skölem, es una forma normal prenexada, donde no aparecen cuantificadores existenciales, toda fórmula puede transformarse en una forma de Skölem partiendo de los siguientes principios:
1.Si en una fórmula, un cuantificador existencial no está precedido por ningún cuantificador universal, como en ∃(x)A(x), este expresa la existencia de un elemento del universo que hace verdadera la fórmula acotada al sustituir a la variable (x). Dicho de otro modo ∃(x)A(x) ⇔ A(a), donde a es el elemento antes mencionado. De lo anterior se desprende que todo cuantificador existencial no precedido por cuantificador universal alguno puede ser eliminado si la variable que acota es sustituida por un símbolo de constante que no ocurra en la fórmula.
2.Si en una fórmula, un cuantificador existencial está precedido por cuantificadores universales, como en Ɐ(x)Ɐ(y)∃(z)A(x, y, z), este expresa la existencia de un elemento del universo que hace verdadera la fórmula acotada al sustituir a la variable (z). Pero este elemento está determinado por x e y, es decir para cada par x e y que se tome el elemento puede ser distinto. Esta dependencia puede expresarse como una función que toma por argumentos a x e y. Entonces:
Ɐ(x)Ɐ(y)∃(z)A(x, y, z) ⇔ Ɐ(x)Ɐ(y) A(x, y, f(x, y))
De lo anterior se desprende que todo cuantificador existencial precedido por cuantificadores universales puede ser eliminado si la variable que acota es sustituida por un símbolo de función que no ocurra en la fórmula y que reciba como argumentos, todas las variables acotadas por los cuantificadores universales que lo preceden.
El siguiente ejemplo ilustra como transformar una fórmula del cálculo de predicados en una forma de Skölem equivalente:
Sea la fórmula ∃(x)Ɐ(y)∃(z)Ɐ(u)∃(v)[(¬S(x, y) v¬P(v, z)) ʌ (P(z, u) v S(z, y)) ʌ (¬P(u, x) v S(x, y))]
Como puede apreciarse la fórmula ya se encuentra en forma normal prenexada, entonces se procede directamente a eliminar los cuantificadores existenciales (∃(x) ∃(z) ∃(v)). El primero de ellos no esta precedido por cuantificador universal alguno, por lo tanto al eliminarlo, se sustituye la variable (x) por un símbolo de constante que no ocurra en la fórmula (a), quedando:
Ɐ(y)∃(z)Ɐ(u)∃(v)[(¬S(a, y) v¬P(v, z)) ʌ (P(z, u) v S(z, y)) ʌ (¬P(u, a) v S(a, y))]
El próximo cuantificador existencial (∃(z)), está precedido por Ɐ(y), lo que provoca que al eliminarlo, la variable (z) sea sustituida por un símbolo de función que no ocurra en la fórmula y tome como argumento a y, en este caso f(y):
Ɐ(y)Ɐ(u)∃(v)[(¬S(a, y) v¬P(v, f(y))) ʌ (P(f(y), u) v S(f(y), y)) ʌ (¬P(u, a) v S(a, y))]
Sólo queda un cuantificador existencial (∃(v)), el que está precedido por Ɐ(y) y Ɐ(u), por tanto al eliminarlo, la variable (u) debe ser sustituida por un símbolo de función que no ocurra en la fórmula y tome como argumentos las variables y y u , en este caso g(y, u), obteniéndose la forma de Skölem:
Ɐ(y)Ɐ(u) [(¬S(a, y) v¬P(g(y, u), f(y))) ʌ (P(f(y), u) v S(f(y), y)) ʌ (¬P(u, a) v S(a, y))]

Conjuntos de cláusulas

Una cláusula no es mas que una disyunción de literales. De este modo, un conjunto de cláusulas será un conjunto de disyunciones de literales. La representación de formulas mediante conjuntos de
La transformación de una forma de Skölem en un conjunto de cláusulas es por tanto un procedimiento bastante directo y sencillo. En primer lugar se eliminan todos los cuantificadores universales, esto es perfectamente posible puesto que al estar todas las variables cuantificadas universalmente, su omisión no crea ambigüedad. Acto seguido se toma cada una de las disyunciones (la fórmula está en fnc) como una cláusula y se omiten las conjunciones. El ejemplo anterior:
Ɐ(y)Ɐ(u) [(¬S(a, y) v ¬P(g(y, u), f(y))) ʌ (P(f(y), u) v S(f(y), y)) ʌ (¬P(u, a) v S(a, y))]
Daría lugar al siguiente conjunto de cláusulas:
{¬S(a, y) v ¬P(g(y, u), f(y)) ,
P(f(y), u) v S(f(y), y),
¬P(u, a) v S(a, y) }

Enlaces externos

http://mathworld.wolfram.com/Calculus.html
http://www.cenidet.edu.mx/dda/docs/aplicacionteoriaactividad.pdf.
http://es.wikiversity.org/wiki/L%C3%B3gica/Constru %C3%B3n_de_sistemas%C3%B3gicos#Reglas_de_transformaci.C3.B3n_de_f.C3.B3rmulas

Bibliogarfía

DEAÑO, ALFREDO (1974). INTRODUCCIÓN A LA LÓGICA FORMAL. MADRID: ALIANZA EDITORIAL. ISBN 84-206-2064-5. 
MITCHELL, D. (1968). INTRODUCCIÓN A LA LÓGICA. BARCELONA: EDITORIAL LABOR. 
QUINE, W.V. (1981). FILOSOFÍA DE LA LÓGICA. MADRID: ALIANZA EDITORIAL. ISBN 84-206-2043-2. 
COPI, IRVING M. (1982). LÓGICA SIMBÓLICA. MEXICO 22 D.F: EDITORIAL CONTINENTAL S.A. DE C.V.. ISBN 968-26-0134-7. 
GARRIDO, M. (1974). LÓGICA SIMBÓLICA. MADRID. EDITORIAL TECNOS S.A.. ISBN 84-309-0537-5. 
NAVARRO, C. Y NADAL, B. (1982). Aspectos de la Matemática en el siglo XX. Historia de la Ciencia. BARCELONA.ED.PLANETA. 81-320-0840-0.