LARA – Lab for Automated Reasoning and Analysis -

This is an old revision of the document!

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 ${\cal L}$ .

Proof:

How to define $L'$ ?

Fix an ordering on the set $V$ of all first-order variables. If $G$ is a term, formula, or a set of formulas, let $fv(G)$ denote the ordered list of its free variables.

Let ${\cal F}$ denote the set of formulas in language ${\cal L}$ . Define \[

  L' = \{ R_{F} \mid F \in {\cal F} \}

\] where $R_{F}$ is a new relation symbol whose arity is equal to $|FV(F)|$ . In other words, we introduce a relation symbol for each formula of the original language.

For each formula $F$ in language $L'$ we define relation-form of $F$ , denoted $rf(F)$ , which is a formula in the original language $L$ 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, $F$ is a formula in $L$ and $fv(F) = x_1,\ldots,x_n$ is the sorted list of its free variables.

How to define $T'$ ?

We let \[

 T' = \{ F \mid rf(F) \in Conseq(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? exactly when $F \in Conseq(T)$ is decidable.

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