Eliminação de quantificadores é um conceito de simplificação usado na lógica matemática, teoria dos modelos, e ciência da computação teórica. Um meio de classificar fórmulas é pelo número de quantificadores. Fórmulas com menos alternância entre os quantificadores são consideradas mais simples, sendo a fórmula livre de quantificadores a mais simples. Uma teoria possui eliminação de quantificadores se para cada fórmula , existe outra fórmula sem quantificadores que é logicamente equivalente a ela.