This is an old revision of the document!
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 ?
Fix an ordering on the set of all first-order variables. If is a term, formula, or a set of formulas, let denote the ordered list of its free variables.
Let denote the set of formulas in language . Define
\[
L' = \{ R_{F} \mid F \in {\cal F} \}
\]
where is a new relation symbol whose arity is equal to . In other words, we introduce a relation symbol for each formula of the original language.
For each formula in language we define relation-form of , denoted , which is a formula in the original language given by
\[
\begin{array}{l}
rf(F_1 \land F_2) = R_{rf(F_1) \land rf(F_2)} \\
rf(F_1 \lor F_2) = R_{rf(F_1) \lor rf(F_2)} \\
rf(\lnot F_1) = R_{\lnot rf(F_1)} \\
rf(\forall x. F_1) = R_{\forall x.rf(F_1)} \\
rf(\exists x. F_1) = R_{\exists x.rf(F_1)} \\
rf(\, R_{F(x_1,\ldots,x_n)}(t_1,\ldots,t_n) \,) = R_{F(t_1,\ldots,t_n)}
\end{array}
\]
in the last definition, is a formula in and is the sorted list of its free variables.
How to define ?
We let
\[
T' = \{ F \mid rf(F) \in Conseq(T) \}
\]
The quantifier-free version of is then simply where . This quantifier elimination is easy and effective (and trivial).
End Proof.
Question: When is the question for from the proof decidable for ground formulas? exactly when is decidable.
Note: often we can have nicer representations instead of , but this depends on particular theory.