Un procedimiento o propiedad de una teoría de primer orden o de un lenguaje formal por la cual toda fórmula que contiene cuantificadores existenciales o universales se transforma en una fórmula equivalente que no contiene cuantificadores, con respecto a la semántica de la teoría.

Principio

Si una teoría admite eliminación de cuantificadores, entonces para toda fórmula φ(x) existe una fórmula sin cuantificadores ψ(x) tal que φ y ψ definen el mismo conjunto en cada modelo de la teoría; el procedimiento reescribe sistemáticamente las expresiones cuantificadas usando las primitivas del lenguaje y los axiomas de la teoría.

Demostración

En la teoría de cuerpos reales cerrados, el procedimiento de Tarski (implementado mediante descomposición algebraica cilíndrica) transforma una fórmula con desigualdades polinómicas y cuantificadores en una combinación booleana equivalente de condiciones sobre signos de polinomios, permitiendo decidir la verdad de enunciados sobre números reales.

Aplicación incorrecta

Asumir que la eliminación de cuantificadores está disponible para teorías arbitrarias (por ejemplo la aritmética de Peano) o usar una transformación de 'eliminación' que solo preserva satisfacibilidad en lugar de equivalencia; aplicar el procedimiento sin comprobar si el lenguaje destino puede expresar la fórmula eliminada conduce a reescrituras inválidas.

Consecuencia

Cuando se aplica con éxito a una teoría, la eliminación de cuantificadores produce un procedimiento de decisión efectivo para oraciones, caracterizaciones de conjuntos definibles y fórmulas más simples para la construcción de modelos y la consulta; sin embargo puede implicar un gran aumento en el tamaño de las fórmulas o en la complejidad computacional.

Inversión

Introducir cuantificadores (o reintroducirlos) incrementa la potencia expresiva y permite describir de forma compacta familias de estructuras o comportamientos infinitos que una fórmula sin cuantificadores no captura; la inversión muestra pérdida de concisión o de comodidad definicional.

Límite

Se aplica a entornos de primer orden y depende de la teoría y el lenguaje; algunas teorías admiten eliminación completa, otras admiten eliminación parcial o relativa, y lógicas de orden superior o teorías con construcciones no interpretadas pueden no admitir eliminación. Los límites prácticos son el coste computacional y la representabilidad en el lenguaje sin cuantificadores destino.

Tensión semántica

Hay tensión entre eliminación de cuantificadores y skolemización: la skolemización elimina existenciales añadiendo símbolos de función pero solo preserva satisfacibilidad, no equivalencia; la eliminación de cuantificadores preserva equivalencia pero puede requerir construcciones booleanas o algebraicas más ricas.

Síntesis

La eliminación de cuantificadores es a la vez una propiedad semántica de una teoría y una familia de procedimientos sintácticos que reemplazan descripciones cuantificadas por fórmulas equivalentes sin cuantificadores; su presencia conduce a decidibilidad y a descripciones concretas de conjuntos definibles, y su ausencia señala barreras expresivas o computacionales.