A theory has quantifier elimination if for every formula f of the theory, there exists another formula f' without quantifiers that is equivalent to it (modulo the theory).
A common technique to show that the validity of a theory is decidable is to show that the theory admits decidable quantifier elimination and then prove the decidability of quantifier-free sentences. This technique is used to show that Presburger arithmetic, i.e. the theory of the additive natural numbers, is decidable.
Note that theories could be decidable yet not admit quantifier elimination. For example, Example: Nullstellensatz in ACF and DCF. On the other hand, whenever a theory in a countable language is decidable, it is possible to extend its language with countably many relations to ensure that it admits quantifier elimination.
No comments:
Post a Comment