¿Por qué?
El punto principal para encontrar la forma normal de Skolem de una fórmula es la eliminación de los cuantificadores existenciales.
¿Cómo es?
-
Si un cuantificador existencial no se encuentra dentro del ámbito de ningún cuantificador universal, entonces hay que sustituir la variable cuantificada existencialmente por una constante que todavía no ha sido utilizada, y eliminar el cuantificador existencial. La constante no se podrá utilizar posteriormente.
-
Si un cuantificador existencial se encuentra dentro del ámbito de un cuantificador universal, entonces hay que sustituir la variable cuantificada existencialmente por una función de la variable cuantificada universalmente, y eliminar el cuantificador existencial. La función no se puede haber utilizado previamente ni se podrá utilizar posteriormente.
-
Si un cuantificador existencial se encuentra dentro del ámbito de más de un cuantificador universal, entonces hay que sustituir la variable cuantificada existencialmente por una función de todas las variables afectadas por estos cuantificadores universales y eliminar el cuantificador existencial. La función no se puede haber utilizado previamente ni se podrá utilizar posteriormente.
Los cuantificadores universales afectan a las variables cuantificadas existencialmente que están dentro de su ámbito, pero no afectan a las otras variables cuantificadas universalmente.
Los cuantificadores existenciales no afectan ni a las variables cuantificadas universalmente ni a ninguna otra variable cuantificada existencialmente.
Las funciones utilizadas para eliminar los cuantificadores existenciales afectados por cuantificadores universales reciben el nombre de funciones de Skolem y se deben considerar términos. Como las constantes, no se pueden cuantificar. Estas funciones ponen en evidencia las relaciones funcionales que existen entre las variables cuantificadas existencialmente y las cuantificadas universalmente.