Quantifier Elimination - Algorithms and Decidability

Algorithms and Decidability

If a theory has quantifier elimination, then a specific question can be addressed: Is there a method of determining for each ? If there is such a method we call it a quantifier elimination algorithm. If there is such an algorithm, then decidability for the theory reduces to deciding the truth of the quantifier-free sentences. Quantifier-free sentences have no variables, so their validity in a given theory can often be computed, which enables the use of quantifier elimination algorithms to decide validity of sentences.