Skolemización

Definición

La skolemización elimina cuantificadores existenciales de una fórmula de primer orden introduciendo símbolos nuevos que representan testigos de existencia.

• Si el existencial no depende de ningún universal en alcance, se usa una constante de Skolem.
• Si depende de variables universales $x_1,\dots ,x_n$, se usa una función de Skolem $F(x_1,\dots ,x_n)$.

Ejemplos

Sin dependencia universal:

$\exists yGato(y)⇝Gato(c).$

Con dependencia de $x$:

$\forall x\exists yAma(y,x)⇝\forall xAma(F(x),x).$

$F(x)$ expresa «algún objeto que ama a $x$». No es necesario conocer cuál objeto es, pero puede variar con $x$.

flowchart LR
    X[∀x: x] --> W[∃y: el testigo puede depender de x]
    W --> FX[F(x)]
    FX --> R[R(x,F(x))]
    C[∃y: no hay universales en alcance] --> K[constante c]
    K --> S[S(c)]

La aridad de la función de Skolem refleja las variables universales que están en alcance cuando aparece el existencial. Los universales no relacionados no se añaden como argumentos.

Propiedad clave

La fórmula original y su forma skolemizada son equisatisfactibles: una tiene modelo si y solo si la otra tiene un modelo apropiado para el vocabulario ampliado. No son, en general, fórmulas lógicamente equivalentes porque la versión skolemizada contiene símbolos nuevos.

Esta propiedad es suficiente para preparar una FNC de primer orden y buscar una contradicción mediante resolución.

Error frecuente

En $\forall x\exists yR(x,y)$, sustituir $y$ por una sola constante $c$ afirmaría que el mismo objeto sirve para todos los $x$. La fórmula original solo exige que cada $x$ tenga algún testigo, por lo que corresponde $R(x,F(x))$.

Procedencia y referencias

• Clase: Inferencia en lógica de primer orden, diapositivas 4–7.
• Russell, S. J. y Norvig, P. (2020). Artificial Intelligence: A Modern Approach (4.ª ed.), §9.5; sitio oficial.
• Enderton, H. B. (2001). A Mathematical Introduction to Logic (2.ª ed.), capítulo 2. Academic Press. Presenta formas prenexas, testigos y transformación a formas normales.