",y la proposición sin cuantificadores puede verse como la respuesta a esa pregunta.
Las fórmulas con menos cuantificadores anidados son más simples, siendo las fórmulas en las que no aparecen cuanficiadores las más sencillas.
Una teoría lógica tiene eliminación de cuantificadores si para cada fórmula
sin cuantificadores que es equivalente a ella (módulo de ese teorema).
Otros ejemplos de teorías en las que se puede aplicar la eliminación de cuantificadores son Aritmética Presburger,[2] Campos algebraicamente cerrados, campos reales cerrados,[2][3] atomless Boolean algebras, term algebras, orden lineal denso,[2] grupos abelianos,[4] grafos arbitrarios, así como muchas de sus combinaciones como el álgebra de Boole con la aritmética de Presburger, y term algebras con colas.
[2] La eliminación de cuantificadores también se utiliza para mostrar que "combinando" teorías lógicas decidibles se da lugar a nuevas teorías lógicas decidibles.
Si una teoría tiene eliminación de cuantificadores, podemos formular la siguiente pregunta: ¿Hay algún método para determinar
Si existe dicho algoritmo, entonces la decidibilidad de esa teoría se reduce a evaluar la veracidad de las proposiciones sin cuantificadores.
Es decir, mostrar que cualquier fórmula expresada de la siguiente forma: donde cada
es una fórmula sin cuantificadores, podemos escribirla en forma normal disyuntiva: y teniendo en cuenta que es equivalente a Finalmente, para eliminar un cuantificador universal donde
en forma normal disyuntiva, y aprovechamos que
Una técnica común era demostrar primero que una teoría admite la eliminación de cuantificadores y después demostrar la decidibilidad o completitud considerando únicamente las fórmulas sin cuantificadores.
Esta técnica sirve para demostrar que la aritmética de Presburger es decidible.
Algunas teorías pueden ser decidibles y no admitir eliminación de cuantificadores.
Siempre que una teoría en un countable language es decidible, es posible extender su lenguaje con muchas relaciones para garantizar que admite la eliminación de cuantificadores (por ejemplo, se puede introducir un símbolo de relación para cada fórmula).