Eliminación de cuantificadores

La eliminación de cuantificadores es un concepto de simplificación utilizado en lógica matemática, teoría de modelos, y teoría de la computación. Informalmente, una proposición cuantificada, por ejemplo " tal que " puede verse como una pregunta: "¿Cuándo hay un tal que ?",y la proposición sin cuantificadores puede verse como la respuesta a esa pregunta.​ Un criterio de clasificación de fórmulas es atendiendo a su cantidad de cuantificadores. 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 , existe otra fórmula sin cuantificadores que es equivalente a ella ( de ese teorema).