Let $T_1$ and $T_2$ be two first-order logical theories (over the same signature) such that $T_1 \subseteq T_2$ and both are recursively axiomatized.
My question is the following: is it possible that $T_1$ is finitely axiomatizable and decidable, while its extension $T_2$ is undecidable?
I would like to know whether there is or not a pair of logical theories with the previous requirements, but I have not been able to find any answer surfing the web. There is a paper by Verena Huber Dyson with the title "On the decision problem for theories of finite models" where there is an example for all these conditions except for requiring finitary axiomatizability. This paper is quite old (1964), so maybe someone here (if not, I will try mathoverflow) can provide me a better answer.
Addendum: By @JDH comments it is clear that
-
$T_1$ cannot be a complete theory (because then there are no consistent extensions).
-
$T_2$ cannot be finitely axiomatizable (because finite extensions of decidable theories are decidable)
Best Answer
Here are a few observations:
Any finite extension of a decidable theory is decidable. That is, if $T_1$ is decidable and $T_2$ is obtained by adding finitely many additional axioms $\varphi$, then $T_2$ is also decidable, since $T_2\vdash\psi$ is the same as $T_1\vdash\varphi\to\psi$.
If $T_2$ is c.e. and complete, then it is decidable, since to decide whether $T_2\vdash\varphi$ one searches either for $\varphi$ or for $\neg\varphi$ in $T_2$.
As I point out in the comment to Chris's answer, a theory is c.e. if and only if it is computably axiomatizable. The reverse implication is just enumerating proofs. For the forward direction, replace each axiom $\varphi$ with an enormous conjunction $\varphi\wedge\cdots\wedge\varphi$ whose length is the time it takes to appear in the computable enumeration. The set of these conjunctions (although a silly trick) axiomatizes the same theory and is decidable.
There are finitely axiomatizable theories in the language of arithmetic that have no decidable extensions. For example, Robinson's $Q$ is an example of this. One reason is that if $Q\subset T$ and $T$ were decidable and consistent, then we could find a computable separation of the two sets $A$ and $B$ consisting of the TM programs that halt with output $0$ and $1$, respectively. The reason is that any such halting behavior would be provable by $Q$ and hence also by $T$, and so we would find a computable set $C$ containing $A$ and disjoint from $B$. But this contradicts that these sets are computably inseparable---by the recursion theorem we could create a program that halts without output $0$ iff it is not in $C$, a contradiction.
There are numerous examples of finitely axiomatizable $T_1$ with c.e. $T_2$ that are not decidable. Chris Eagle gave one in his answer, if you take his set $A$ to be c.e. but not decidable. You can do his trick with any decidable theory $T_1$, provided that it has models with at least two elements. Just add new constant symbols $c_i$ and add the axioms $c_i=c_j$ whenever $i,j\in A$, for some fixed c.e. non-decidable set $A$. We can enumerate these axioms, so the resulting theory $T_2$ is c.e., but not decidable, since from a decision procedure for $T_2$ we could decide membership in $A$.