Una transformación sintáctica que elimina cuantificadores existenciales introduciendo funciones o constantes de Skolem, produciendo una fórmula equisatisfiable en la que los existenciales se han suprimido, comúnmente como paso hacia la forma de cláusulas o el razonamiento automático.

Principio

Reemplazar variables cuantificadas existencialmente por funciones de Skolem nuevas cuyos argumentos son las variables universalmente cuantificadas en cuyo alcance aparece el existencial; esto preserva la satisfacibilidad (pero no la equivalencia lógica) y produce fórmulas adecuadas para resolución.

Demostración

A partir de ∀x ∃y P(x,y) transformar a ∀x P(x, f(x)) introduciendo una función de Skolem f; los modelos satisfactibles del original corresponden a modelos de la forma skolemizada con la interpretación apropiada de f.

Aplicación incorrecta

Tratar la skolemización como preservadora de la equivalencia en lugar de solo la satisfacibilidad conduce a sustituciones no válidas en contextos que requieren equivalencia lógica (por ejemplo al extraer consecuencias deductivas en lugar de verificar satisfacibilidad).

Consecuencia

La skolemización posibilita procedimientos de prueba mecanizados (generación de cláusulas, resolución) al eliminar cuantificadores existenciales y producir una forma apta para unificación y búsqueda automática; simplifica el manejo de testigos pero puede ocultar contenido constructivo.

Inversión

La inversión es reintroducir cuantificadores existenciales o testigos explícitamente (términos testigo o constantes de Skolem constructivas) para recuperar equivalencia e información constructiva; esto suele requerir información adicional o una prueba de existencia.

Límite

Garantiza equisatisfactibilidad para fórmulas de primer orden cuando se aplica correctamente, pero no preserva en general la validez ni la dirección de implicación; no es directamente aplicable sin adaptación en algunos entornos de orden superior o constructivos.

Tensión semántica

Tensión con interpretaciones constructivas: la skolemización es clásica y model-teórica (preserva satisfacibilidad) y entra en conflicto con la necesidad constructiva de producir testigos explícitos o mantener afirmaciones de existencia demostrables.

Síntesis

La skolemización es una reescritura sintáctica que preserva modelos y sustituye cuantificadores existenciales por símbolos de función nuevos dependientes de las variables universales circundantes, intercambiando equivalencia lógica por equisatisfactibilidad para facilitar el razonamiento automático basado en cláusulas.