Forma normal de Skolem

En lógica matemática , una fórmula de lógica de primer orden está en forma normal de Skolem si está en forma normal prenexa con solo cuantificadores universales de primer orden .

Toda fórmula de primer orden puede convertirse a la forma normal de Skolem sin alterar su satisfacibilidad mediante un proceso denominado skolemización (a veces escrito skolemnización ). La fórmula resultante no es necesariamente equivalente a la original, pero es equisatisfacible con ella: es satisfacible si y solo si la original es satisfacible. ^{[ 1 ]}

La reducción a la forma normal de Skolem es un método para eliminar cuantificadores existenciales de enunciados de lógica formal , que a menudo se realiza como primer paso en un demostrador automático de teoremas .

La forma más simple de skolemización es para variables cuantificadas existencialmente que no están dentro del alcance de un cuantificador universal. Estas pueden ser reemplazadas simplemente creando nuevas constantes. Por ejemplo,${\displaystyle \exists xP(x)}$puede cambiarse a${\displaystyle P(c)}$, dónde${\displaystyle c}$es una nueva constante (no aparece en ninguna otra parte de la fórmula).

En términos más generales, la skolemización se realiza reemplazando cada variable cuantificada existencialmente.${\displaystyle y}$con un término${\displaystyle f(x_{1},\ldots ,x_{n})}$cuyo símbolo de función${\displaystyle f}$es nuevo. Las variables de este término son las siguientes. Si la fórmula está en forma normal prenexa , entonces${\displaystyle x_{1},\ldots ,x_{n}}$son las variables que se cuantifican universalmente y cuyos cuantificadores preceden a los de${\displaystyle y}$En general, son las variables que se cuantifican universalmente (suponemos que eliminamos los cuantificadores existenciales en orden, por lo que todos los cuantificadores existenciales anteriores${\displaystyle \exists y}$han sido eliminados) y tales que${\displaystyle \exists y}$ocurre dentro del alcance de sus cuantificadores. La función${\displaystyle f}$La función introducida en este proceso se denomina función de Skolem (o constante de Skolem si es de aridad cero ) y el término se denomina término de Skolem .

Como ejemplo, la fórmula${\displaystyle \forall x\exists y\forall zP(x,y,z)}$no está en forma normal de Skolem porque contiene el cuantificador existencial${\displaystyle \exists y}$. La skolemización reemplaza${\displaystyle y}$con${\displaystyle f(x)}$, dónde${\displaystyle f}$es un nuevo símbolo de función y elimina la cuantificación sobre${\displaystyle y}$La fórmula resultante es${\displaystyle \forall x\forall zP(x,f(x),z)}$El término Skolem${\displaystyle f(x)}$contiene${\displaystyle x}$pero no${\displaystyle z}$, porque el cuantificador que se va a eliminar${\displaystyle \exists y}$está dentro del alcance de${\displaystyle \forall x}$, pero no en el de${\displaystyle \forall z}$; dado que esta fórmula está en forma normal prenexa, esto es equivalente a decir que, en la lista de cuantificadores,${\displaystyle x}$precede${\displaystyle y}$mientras${\displaystyle z}$No. La fórmula obtenida mediante esta transformación es satisfacible si y solo si la fórmula original lo es.

La skolemización funciona aplicando una equivalencia de segundo orden junto con la definición de satisfacibilidad de primer orden. Esta equivalencia permite "trasladar" un cuantificador existencial ante uno universal.

${\displaystyle \forall x\exists yR(x,y)\iff \exists f\forall xR(x,f(x))}$

dónde

${\displaystyle f(x)}$es una función que mapea${\displaystyle x}$a${\displaystyle y}$.

Intuitivamente, la frase "por cada${\displaystyle x}$existe un${\displaystyle y}$de tal manera que${\displaystyle R(x,y)}$" se convierte en la forma equivalente "existe una función${\displaystyle f}$mapeando cada${\displaystyle x}$en un${\displaystyle y}$de tal manera que, para cada${\displaystyle x}$sostiene que${\displaystyle R(x,f(x))}$".

Esta equivalencia es útil porque la definición de satisfacibilidad de primer orden cuantifica implícitamente de forma existencial sobre funciones que interpretan los símbolos de función. En particular, una fórmula de primer orden${\displaystyle \Phi }$es satisfacible si existe un modelo${\displaystyle M}$y una evaluación${\displaystyle \mu }$de las variables libres de la fórmula que evalúan la fórmula como verdadera . El modelo contiene la interpretación de todos los símbolos de función; por lo tanto, las funciones de Skolem están implícitamente cuantificadas existencialmente. En el ejemplo anterior,${\displaystyle \forall xR(x,f(x))}$es satisfacible si y solo si existe un modelo${\displaystyle M}$, que contiene una interpretación para${\displaystyle f}$, de tal manera que${\displaystyle \forall xR(x,f(x))}$es cierto para alguna evaluación de sus variables libres (ninguna en este caso). Esto puede expresarse en segundo orden como${\displaystyle \exists f\forall xR(x,f(x))}$. Por la equivalencia anterior, esto es lo mismo que la satisfacibilidad de${\displaystyle \forall x\exists yR(x,y)}$.

A nivel meta, la satisfacibilidad de primer orden de una fórmula${\displaystyle \Phi }$puede escribirse con un pequeño abuso de notación como${\displaystyle \exists M\exists \mu (M,\mu \models \Phi )}$, dónde${\displaystyle M}$es un modelo,${\displaystyle \mu }$es una evaluación de las variables libres, y${\displaystyle \models }$significa que${\displaystyle \Phi }$es cierto en${\displaystyle M}$bajo${\displaystyle \mu }$. Dado que los modelos de primer orden contienen la interpretación de todos los símbolos de función, cualquier función de Skolem que${\displaystyle \Phi }$contiene está implícitamente cuantificado existencialmente por${\displaystyle \exists M}$Como resultado, después de reemplazar los cuantificadores existenciales sobre variables por cuantificadores existenciales sobre funciones al principio de la fórmula, esta aún puede tratarse como una de primer orden eliminando dichos cuantificadores existenciales. Este paso final de tratamiento${\displaystyle \exists f\forall xR(x,f(x))}$como${\displaystyle \forall xR(x,f(x))}$puede completarse porque las funciones están implícitamente cuantificadas existencialmente por${\displaystyle \exists M}$en la definición de satisfacibilidad de primer orden.

La corrección de la skolemización puede demostrarse en la fórmula de ejemplo.${\displaystyle F_{1}=\forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)}$de la siguiente manera. Esta fórmula es satisfecha por un modelo.${\displaystyle M}$si y solo si, para cada posible valor de${\displaystyle x_{1},\dots ,x_{n}}$en el dominio del modelo, existe un valor para${\displaystyle y}$en el dominio del modelo que hace${\displaystyle R(x_{1},\dots ,x_{n},y)}$verdadero. Por el axioma de elección , existe una función${\displaystyle f}$de tal manera que${\displaystyle y=f(x_{1},\dots ,x_{n})}$. Como resultado, la fórmula${\displaystyle F_{2}=\forall x_{1}\dots \forall x_{n}R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))}$es satisfacible, porque tiene el modelo obtenido al agregar la interpretación de${\displaystyle f}$a${\displaystyle M}$Esto demuestra que${\displaystyle F_{1}}$es satisfacible solo si${\displaystyle F_{2}}$también es satisfacible. Por el contrario, si${\displaystyle F_{2}}$Si es satisfacible, entonces existe un modelo.${\displaystyle M'}$que lo satisface; este modelo incluye una interpretación para la función${\displaystyle f}$de tal manera que, para cada valor de${\displaystyle x_{1},\dots ,x_{n}}$, la fórmula${\displaystyle R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))}$sostiene. Como resultado,${\displaystyle F_{1}}$se satisface con el mismo modelo porque se puede elegir, para cada valor de${\displaystyle x_{1},\ldots ,x_{n}}$, el valor${\displaystyle y=f(x_{1},\dots ,x_{n})}$, dónde${\displaystyle f}$se evalúa según${\displaystyle M'}$.

Uno de los usos de la skolemización se encuentra en la demostración automática de teoremas . Por ejemplo, en el método de los tableaux analíticos , siempre que aparece una fórmula cuyo cuantificador principal es existencial, se puede generar la fórmula obtenida al eliminar dicho cuantificador mediante la skolemización. Por ejemplo, si${\displaystyle \exists x\Phi (x,y_{1},\ldots ,y_{n})}$ocurre en un cuadro, donde${\displaystyle x,y_{1},\ldots ,y_{n}}$son las variables libres de${\displaystyle \Phi (x,y_{1},\ldots ,y_{n})}$, entonces${\displaystyle \Phi (f(y_{1},\ldots ,y_{n}),y_{1},\ldots ,y_{n})}$puede agregarse a la misma rama del tablero. Esta adición no altera la satisfacibilidad del tablero: cada modelo de la fórmula antigua puede extenderse agregando una interpretación adecuada de${\displaystyle f}$, a un modelo de la nueva fórmula.

Esta forma de skolemización supone una mejora respecto a la skolemización "clásica", ya que solo las variables libres en la fórmula se incluyen en el término de skolem. Esto representa una mejora porque la semántica de los tableaux puede situar implícitamente la fórmula en el ámbito de algunas variables cuantificadas universalmente que no están presentes en la fórmula misma; estas variables no se incluyen en el término de skolem, aunque sí lo estarían según la definición original de skolemización. Otra mejora que se puede utilizar consiste en aplicar el mismo símbolo de función de skolem a fórmulas idénticas salvo por el cambio de nombre de las variables. ^{[ 2 ]}

Otro uso se encuentra en el método de resolución para la lógica de primer orden , donde las fórmulas se representan como conjuntos de cláusulas que se entienden cuantificadas universalmente. (Para un ejemplo, véase la paradoja del bebedor ).

Un resultado importante en la teoría de modelos es el teorema de Löwenheim-Skolem , que puede demostrarse mediante la skolemización de la teoría y el cierre bajo las funciones de Skolem resultantes. ^{[ 3 ]}

En general, si${\displaystyle T}$es una teoría y para cada fórmula con variables libres${\displaystyle x_{1},\dots ,x_{n},y}$Hay un símbolo de función n -aria${\displaystyle F}$que es demostrablemente una función de Skolem para${\displaystyle y}$, entonces${\displaystyle T}$Se denomina teoría de Skolem . ^{[ 4 ]}

Toda teoría de Skolem es modelo-completa , es decir, toda subestructura de un modelo es una subestructura elemental . Dado un modelo M de una teoría de Skolem T , la subestructura más pequeña de M que contiene un conjunto A determinado se denomina envoltura de Skolem de A. La envoltura de Skolem de A es un modelo atómico primo sobre A.

La forma normal de Skolem recibe su nombre del difunto matemático noruego Thoralf Skolem .

• Herbrandización , el dual de Skolemización
• lógica de functores de predicados

• "Función de Skolem" , Enciclopedia de Matemáticas , EMS Press , 2001 [1994]
• Eskolemización en PlanetMath.org
• Skolemización por Hector Zenil, El Proyecto de Demostraciones de Wolfram .
• Weisstein, Eric W. "Forma skolemizada" . MathWorld .