Esta ha sido una pregunta interesante, aunque averiguar cómo formular una respuesta no fue trivial para mí. Me gustaría ver una respuesta más formal. Pero ahí va:
Permítanme aclarar primero que mi respuesta se refiere a las fórmulas en forma normal prenex (PNF). Pero no pasa nada, porque todas las fórmulas pueden convertirse a una PNF equivalente y viceversa.
Una forma normal de skolem, $\text{Sk}(\phi)$ de una fórmula $\phi$ que está en PNF, no es equivalente a $\phi$ pero es equisalible con ella. La razón por la que no son equivalentes es porque las dos fórmulas "viven" en diferentes "mundos" (modelos). La skolemización elimina los existenciales introduciendo nuevos sin interpretar constantes. No se interpretan en el sentido de que no tienen sentido en el modelo original. Así que, en cierto modo, son nuevos objetos abstractos, pero aceptan una interpretación (un "mapeo" a objetos del modelo original), de modo que las fórmulas skolemizadas se mantienen en un modelo si existe un modelo (posiblemente diferente) en el que la fórmula original se mantiene.
Como nota al margen, aquí $\text{Sk}(-)$ denota la conversión de la entrada en la forma normal de Skolem (SNF). Sin embargo, no se trata exactamente de una función, porque hay muchas SNF de una fórmula en PNF. Pero qué SNF tomamos no importa, así que abusaré de la notación y escribiré $\text{Sk}(-)$ .
Por lo tanto, queremos demostrar $\{\Sigma,\neg\phi\}$ incoherente (y, por tanto, no satisfacible). Por razones técnicas, decidimos que es mejor convertir primero estas fórmulas en CNF (un proceso que, entre otras transformaciones que aplica, también skolemiza las fórmulas de entrada). En mi notación abusiva, esto significaría que nos "movemos" a este modelo extendido y tratamos de demostrar la inconsistencia del conjunto $\text{Sk}(\{\Sigma,\neg\phi\}) = \{\text{Sk}(\Sigma),\text{Sk}(\neg\phi)\}$ . Aquí queda claro por qué se aplica primero la negación y luego viene la esquematización.
La parte de resolución del algoritmo funciona con $\text{Sk}(\{\Sigma,\neg\phi\})$ y el resultado se mantendrá para $\{\Sigma,\neg\phi\}$ . Estos dos conjuntos de fórmulas están conectados con una relación específica: la equisatisfacción. Así, si la segunda es inconsistente (y por tanto insatisfactible), la primera también es insatisfactible.
Ahora bien, tenga en cuenta que $\text{Sk}(\neg\phi)\not\equiv\neg\text{Sk}(\phi)$ . En terminología matemática, la negación y la esquematización no son conmutativas ni congruentes con respecto a la equivalencia lógica, si se consideran como operaciones sobre fórmulas PNF. Dicho de otro modo, importa cuál de las dos operaciones aplicamos primero, porque una orden puede devolver una fórmula diferente que ni siquiera es lógicamente equivalente a la fórmula que se obtendría con otra orden.
Por lo tanto, no se puede aplicar la resolución en $\{\text{Sk}(\Sigma),\neg\text{Sk}(\phi)\}$ y esperar que se obtengan resultados correctos. Esto se debe a que $\{\text{Sk}(\Sigma),\neg\text{Sk}(\phi)\}$ no conserva la igualabilidad con el conjunto original $\{\Sigma,\neg\phi\}$ . En otras palabras, en el caso general, $\{\text{Sk}(\Sigma),\neg\text{Sk}(\phi)\} \neq \text{Sk}(\{\Sigma,\neg\phi\})$ .
Informalmente, la negación de una fórmula skolemizada no es equivalente a la negación de la fórmula original. La fórmula skolemizada vive en un modelo diferente y por lo tanto, con este orden de aplicación, se niega una fórmula que posiblemente se refiera a alguna constante ajena que no forma parte del modelo original.
Otro problema que surge si se niega después de skolemizar: La negación puede hacer que algunas variables se cuantifiquen existencialmente. Estas variables permanecen sin negar, ya que la fase de esquematización ocurrió justo antes. ¿Cómo debería manejar el algoritmo estos existenciales?
