LARA

Extending Languages of Decidable Theories

Recall from Quantifier elimination definition that if $T$ 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 $T$. Then there exists an extended language $L' \supseteq L$ and a set of formulas $T'$ such that $T'$ has effective quantifier elimination, and such that $Conseq(T)$ is exactly the set of those formulas in $Conseq(T')$ that contain only symbols from $L$.

Proof:

How to define $L'$?

How to define $T'$?

How to do quantifier elimination in $T'$?

End Proof.

Question: When is the question $F \in Conseq(T')$ for $T'$ from the proof decidable for ground formulas?

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