Forma normal de Skolem - Skolem normal form

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 capacidad de satisfacción a través de un proceso llamado Skolemización (a veces escrito Skolemnización ). La fórmula resultante no es necesariamente equivalente a la original, pero es igual de satisfactoria con ella: es satisfactoria si y sólo si la original es satisfactoria.

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 automático de teoremas .

Ejemplos de

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 es una nueva constante (no aparece en ningún otro lugar de la fórmula). ${\ Displaystyle \ existe xP (x)}$${\ Displaystyle P (c)}$${\ Displaystyle c}$

De manera más general, la Skolemización se realiza reemplazando cada variable cuantificada existencialmente con 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 se cuantifican universalmente y cuyos cuantificadores preceden al de . En general, son las variables que se cuantifican universalmente (suponemos que nos deshacemos de los cuantificadores existenciales en orden, por lo que todos los cuantificadores existenciales anteriores han sido eliminados) y tal que ocurre en el ámbito de sus cuantificadores. La función introducida en este proceso se llama función de Skolem (o constante de Skolem si es de cero aridad ) y el término se llama término de Skolem . ${\ Displaystyle y}$${\ Displaystyle f (x_ {1}, \ ldots, x_ {n})}$${\ Displaystyle f}$${\ Displaystyle x_ {1}, \ ldots, x_ {n}}$${\ Displaystyle y}$${\ Displaystyle \ existe y}$${\ Displaystyle \ existe y}$${\ Displaystyle f}$

Por ejemplo, la fórmula no está en la forma normal de Skolem porque contiene el cuantificador existencial . Skolemization reemplaza con , where es un nuevo símbolo de función y elimina el over de cuantificación . 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 por esta transformación es satisfactoria si y solo si la fórmula original lo es. ${\ Displaystyle \ forall x \ existe y \ forall zP (x, y, z)}$${\ Displaystyle \ existe 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 \ existe y}$${\ Displaystyle \ forall x}$${\ Displaystyle \ forall z}$${\ Displaystyle x}$${\ Displaystyle y}$${\ Displaystyle z}$

Cómo funciona la skolemización

La skolemización funciona aplicando una equivalencia de segundo orden junto con la definición de satisfacibilidad de primer orden. La equivalencia proporciona una forma de "mover" un cuantificador existencial antes que uno universal.

${\ Displaystyle \ forall x {\ Big (} R (g (x)) \ vee \ exist yR (x, y) {\ Big)} \ iff \ exist f \ forall x {\ Big (} R (g ( x)) \ vee R (x, f (x)) {\ Big)}}$

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 mapea cada uno en un tal que, para cada uno que contiene ". ${\ 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 sobre la evaluación de símbolos de función. 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úan la fórmula como verdadera . El modelo contiene la evaluación de todos los símbolos de función; por lo tanto, las funciones de Skolem se cuantifican existencialmente de manera implícita. En el ejemplo anterior, es satisfactorio si y solo si existe un modelo , que contiene una evaluación para , tal que sea ​​cierto para alguna evaluación de sus variables libres (ninguna en este caso). Esto se puede expresar en segundo orden como . Por 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 \ existe f \ forall xR (x, f (x))}$${\ Displaystyle \ forall x \ existe yR (x, y)}$

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

La corrección de la skolemización puede mostrarse en la fórmula de ejemplo como sigue. Esta fórmula es satisfecha por un modelo si y solo si, para cada valor posible para en el dominio del modelo, existe un valor para en el dominio del modelo que lo hace verdadero. Según el axioma de elección , existe una función tal que . Como resultado, la fórmula es satisfactoria, porque tiene el modelo obtenido al sumar la evaluación de a . Esto demuestra que es satisfactorio sólo si también lo es. Por el contrario, si es satisfactorio, entonces existe un modelo que lo satisface; este modelo incluye una evaluación de la función de modo que, para cada valor de , se cumple la fórmula . 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} \ existe 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 skolemización

Uno de los usos de Skolemization es la demostración automatizada de teoremas . Por ejemplo, en el método de cuadros analíticos , siempre que ocurre una fórmula cuyo cuantificador principal es existencial, se puede generar la fórmula obtenida al eliminar ese cuantificador mediante Skolemización. Por ejemplo, si ocurre en un cuadro, donde están las variables libres de , entonces puede agregarse a la misma rama del cuadro. Esta adición no altera la satisfacibilidad del cuadro: cada modelo de la fórmula anterior puede extenderse, agregando una evaluación adecuada de , a un modelo de la nueva fórmula. ${\ Displaystyle \ existe 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 Skolem. Esto es una mejora porque la semántica del cuadro puede colocar implícitamente la fórmula en el alcance de algunas variables cuantificadas universalmente que no están en la fórmula misma; estas variables no están en el término de Skolem, mientras que estarían allí de acuerdo con 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 que son idénticas hasta el cambio de nombre de variables.

Otro uso es 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 ver un ejemplo, consulte la paradoja del bebedor ).

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 que probablemente es una función de Skolem , entonces se llama teoría de Skolem . ${\ Displaystyle T}$ ${\ Displaystyle x_ {1}, \ dots, x_ {n}, y}$${\ Displaystyle F}$${\ Displaystyle y}$${\ Displaystyle T}$

Toda 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 Skolem T , la subestructura más pequeño que contiene un cierto conjunto A se llama el casco Skolem de A . El casco de Skolem A es un atómica modelo prime sobre una .

Historia

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

Ver también

• Herbrandization , el dual de Skolemization
• Lógica del functor de predicados

Notas

Referencias

• Hodges, Wilfrid (1997), A Shorter Model Theory , Cambridge University Press , ISBN   978-0-521-58713-6 CS1 maint: parámetro desalentado ( enlace )

enlaces externos

• "Función Skolem" , Enciclopedia de Matemáticas , EMS Press , 2001 [1994]
• Skolemización en PlanetMath.org
• Skolemization por Hector Zenil, The Wolfram Demonstrations Project .
• Weisstein, Eric W. "SkolemizedForm" . MathWorld .