LARA

Extending Languages of Decidable Theories

Recall from Quantifier elimination definition that if has effective quantifier elimination and there is an algorithm for deciding validity of ground formulas, then the theory is decidable. Now we show a sort of converse.

Lemma: Consider a set of formulas . Then there exists an extended language and a set of formulas such that has effective quantifier elimination, and such that is exactly the set of those formulas in that contain only symbols from .

Proof:

How to define ?

How to define ?

How to do quantifier elimination in ?

End Proof.

Question: When is the question for from the proof decidable for ground formulas?

Note: often we can have nicer representations instead of , but this depends on particular theory.