Forma normal de skolem

Formalismo de la lógica de primer orden

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 prenex con solo cuantificadores universales de primer orden .

Cada fórmula de primer orden se puede convertir a la forma normal de Skolem sin cambiar su satisfacibilidad mediante un proceso llamado 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 sólo 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 lógicos formales , que a menudo se realiza como el primer paso en un demostrador de teoremas automatizado .

Ejemplos

La forma más simple de Skolemización es para variables cuantificadas existencialmente que no están dentro del alcance de un cuantificador universal. Estos pueden reemplazarse simplemente creando nuevas constantes. Por ejemplo, se puede cambiar a , donde hay una nueva constante (no aparece en ningún otro lugar de la fórmula). ${\displaystyle \exists xP(x)}$ ${\displaystyle P(c)}$ ${\displaystyle c}$

De manera más general, la eskolemización se realiza reemplazando cada variable cuantificada existencialmente por un término cuyo símbolo de función es nuevo. Las variables de este término son las siguientes. Si la fórmula está en forma normal prenex , entonces son las variables que están universalmente cuantificadas y cuyos cuantificadores preceden al de . En general, son las variables que se cuantifican universalmente (asumimos que nos deshacemos de los cuantificadores existenciales en orden, por lo que se han eliminado todos los cuantificadores existenciales anteriores) y las que ocurren en el alcance de sus cuantificadores. 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 . ${\displaystyle y}$ ${\displaystyle f(x_{1},\ldots ,x_{n})}$ ${\displaystyle f}$ ${\displaystyle x_{1},\ldots ,x_{n}}$ ${\displaystyle y}$ ${\displaystyle \exists y}$ ${\displaystyle \exists y}$ ${\displaystyle f}$

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

Cómo funciona la eskolemización

La eskolemización funciona aplicando una equivalencia de segundo orden junto con la definición de satisfacibilidad de primer orden. La equivalencia proporciona una manera de "mover" un cuantificador existencial antes que 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 se asigna a . ${\displaystyle x}$ ${\displaystyle y}$

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

Esta equivalencia es útil porque la definición de satisfacibilidad de primer orden cuantifica implícitamente existencialmente las funciones que interpretan los símbolos de las funciones. En particular, una fórmula de primer orden es satisfactoria si existe un modelo y una evaluación de las variables libres de la fórmula que evalúen 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, es satisfactorio si y sólo si existe un modelo que contenga una interpretación para tal que sea verdadera para alguna evaluación de sus variables libres (ninguna en este caso). Esto se puede expresar en segundo orden como . Según la equivalencia anterior, esto es lo mismo que la satisfacibilidad de . ${\displaystyle \Phi }$ ${\displaystyle M}$ ${\displaystyle \mu }$ ${\displaystyle \forall xR(x,f(x))}$ ${\displaystyle M}$ ${\displaystyle f}$ ${\displaystyle \forall xR(x,f(x))}$ ${\displaystyle \exists f\forall xR(x,f(x))}$ ${\displaystyle \forall x\exists yR(x,y)}$

En el metanivel, la satisfacibilidad de primer orden de una fórmula se puede escribir con un pequeño abuso de notación como , donde es un modelo, es una evaluación de las variables libres y significa que es verdadera en virtud de . Dado que los modelos de primer orden contienen la interpretación de todos los símbolos de funciones, cualquier función de Skolem que los contenga se cuantifica implícitamente existencialmente mediante . Como resultado, después de reemplazar los cuantificadores existenciales sobre las variables por cuantificadores existenciales sobre las funciones al principio de la fórmula, la fórmula aún puede tratarse como de primer orden eliminando estos cuantificadores existenciales. Este paso final de tratar como puede completarse porque las funciones están implícitamente cuantificadas existencialmente en la definición de satisfacibilidad de primer orden. ${\displaystyle \Phi }$ ${\displaystyle \exists M\exists \mu (M,\mu \models \Phi )}$ ${\displaystyle M}$ ${\displaystyle \mu }$ ${\displaystyle \models }$ ${\displaystyle \Phi }$ ${\displaystyle M}$ ${\displaystyle \mu }$ ${\displaystyle \Phi }$ ${\displaystyle \exists M}$ ${\displaystyle \exists f\forall xR(x,f(x))}$ ${\displaystyle \forall xR(x,f(x))}$ ${\displaystyle \exists M}$

La exactitud de la skolemización se puede mostrar en la fórmula de ejemplo de la siguiente manera. Un modelo satisface esta fórmula si y sólo si, para cada valor posible de en el dominio del modelo, existe un valor de en el dominio del modelo que sea verdadero. Por el axioma de elección , existe una función tal que . Como resultado, la fórmula es satisfactoria, porque tiene el modelo obtenido sumando la interpretación de a . Esto demuestra que es satisfacible sólo si también lo es. Por el contrario, si es satisfacible, entonces existe un modelo que lo satisfaga; este modelo incluye una interpretación de la función tal que, para cada valor de , la fórmula se cumple. Como resultado, se satisface con el mismo modelo porque se puede elegir, para cada valor de , el valor , donde se evalúa según . ${\displaystyle F_{1}=\forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)}$ ${\displaystyle M}$ ${\displaystyle x_{1},\dots ,x_{n}}$ ${\displaystyle y}$ ${\displaystyle R(x_{1},\dots ,x_{n},y)}$ ${\displaystyle f}$ ${\displaystyle y=f(x_{1},\dots ,x_{n})}$ ${\displaystyle F_{2}=\forall x_{1}\dots \forall x_{n}R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))}$ ${\displaystyle f}$ ${\displaystyle M}$ ${\displaystyle F_{1}}$ ${\displaystyle F_{2}}$ ${\displaystyle F_{2}}$ ${\displaystyle M'}$ ${\displaystyle f}$ ${\displaystyle x_{1},\dots ,x_{n}}$ ${\displaystyle R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))}$ ${\displaystyle F_{1}}$ ${\displaystyle x_{1},\ldots ,x_{n}}$ ${\displaystyle y=f(x_{1},\dots ,x_{n})}$ ${\displaystyle f}$ ${\displaystyle M'}$

Usos de la eskolemización

Uno de los usos de la Skolemización es la demostración automatizada de teoremas . Por ejemplo, en el método de cuadros analíticos , siempre que aparece una fórmula cuyo cuantificador principal es existencial, se puede generar la fórmula obtenida eliminando ese cuantificador mediante la eskolemización. Por ejemplo, si ocurre en un cuadro, donde están las variables libres de , entonces se puede agregar a la misma rama del cuadro. Esta adición no altera la satisfacibilidad del cuadro: cada modelo de la antigua fórmula puede ampliarse añadiendo una interpretación adecuada de , a un modelo de la nueva fórmula. ${\displaystyle \exists x\Phi (x,y_{1},\ldots ,y_{n})}$ ${\displaystyle x,y_{1},\ldots ,y_{n}}$ ${\displaystyle \Phi (x,y_{1},\ldots ,y_{n})}$ ${\displaystyle \Phi (f(y_{1},\ldots ,y_{n}),y_{1},\ldots ,y_{n})}$ ${\displaystyle f}$

Esta forma de Skolemización es una mejora con respecto a la Skolemización "clásica" en el sentido de que sólo las variables que están libres en la fórmula se colocan en el término de Skolem. Esto es una mejora porque la semántica de los cuadros puede colocar implícitamente la fórmula en el alcance de algunas variables universalmente cuantificadas que no están en la fórmula misma; estas variables no están en el término Skolem, mientras que estarían ahí según la definición original de Skolemización. Otra mejora que se puede utilizar es aplicar el mismo símbolo de función de Skolem para fórmulas idénticas hasta el cambio de nombre de variable. ^[2]

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

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

teorías de skolem

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

Cada teoría de Skolem es un modelo completo , es decir, cada 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 que contiene un determinado conjunto A se llama casco de Skolem de A. El casco Skolem de A es un modelo primo atómico sobre A.

Historia

La forma normal de Skolem lleva el nombre del fallecido matemático noruego Thoralf Skolem .

Ver también

• Herbrandización , el dual de la Skolemización
• Lógica de functor predicado

Notas

1. "Formas normales y eskolemización" (PDF) . Instituto Max Planck de Informática . Consultado el 15 de diciembre de 2012 .
2. Reiner Hähnle. Tableaux y métodos relacionados. Manual de razonamiento automatizado .
3. Scott Weinstein, El teorema de Lowenheim-Skolem, notas de clase (2009). Consultado el 6 de enero de 2023.
4. "Conjuntos, modelos y pruebas" (3.3) de I. Moerdijk y J. van Oosten

Referencias

• Hodges, Wilfrid (1997), Una teoría del modelo más corto , Cambridge University Press , ISBN 978-0-521-58713-6

enlaces externos

• "Función Skolem", Enciclopedia de Matemáticas , EMS Press , 2001 [1994]
• Eskolemización en PlanetMath.org
• Skolemización de Héctor Zenil, The Wolfram Demonstrations Project .
• Weisstein, Eric W. "Forma eskolemizada". MundoMatemático .