Una normalización sintáctica de fórmulas de primer orden que desplaza todos los cuantificadores al frente para producir una fórmula equivalente con un prefijo de cuantificadores seguido de una matriz sin cuantificadores.

Principio

Separar la estructura de enlace (cuantificadores) del núcleo proposicional mediante permutación y renombrado de variables, de modo que todos los cuantificadores formen un prefijo contiguo y se preserve la propiedad buscada (equivalencia lógica o satisfactibilidad).

Demostración

A partir de ∀x (P(x) → ∃y Q(y,x)) se convierte a forma prenexa renombrando y moviendo cuantificadores para obtener ∀x ∃y (¬P(x) ∨ Q(y,x)) o, tras esquelonización para satisfactibilidad, ∀x (¬P(x) ∨ Q(f(x),x)). Esto muestra el traslado de cuantificadores y la matriz sin cuantificadores.

Aplicación incorrecta

Mover cuantificadores sin atender a la captura de variables, cambios de alcance o a la diferencia entre preservar equivalencia y preservar satisfactibilidad. Por ejemplo, eliminar dependencias durante la esquelonización puede falsear la dependencia existencial respecto a variables universales.

Consecuencia

Las fórmulas en forma prenexa facilitan la comparación, la resolución y muchos procedimientos metateóricos (p. ej. clasificación por prefijo de cuantificadores), a costa de ocultar los alcances locales originales y, a menudo, de requerir esquelonización para preservar satisfactibilidad.

Inversión

La inversión consiste en reconstruir los alcances variables originales y mover cuantificadores hacia dentro de la matriz para reflejar dependencias locales; la forma prenexa aplana esta información local.

Límite

Se aplica a la lógica de primer orden clásica y a lógicas relacionadas; no siempre preserva la verdad en lógicas no clásicas sin precauciones, y la esquelonización elimina cuantificadores existenciales solo en contextos de satisfactibilidad, no siempre en equivalencia estricta.

Tensión semántica

Tensión entre uniformidad sintáctica (todos los cuantificadores al frente) y localidad semántica (cuantificadores cuyo sentido depende de conectivos próximos), así como entre preservar equivalencia lógica o solo satisfactibilidad.

Síntesis

La forma prenexa es una normalización sintáctica que extrae la estructura cuantificadora a un prefijo para facilitar el razonamiento mecánico y la clasificación, sacrificando la claridad de los alcances locales; su uso requiere atención a dependencias de variables y al objetivo de preservación (equivalencia vs satisfactibilidad).