Example of an UnDecidable Logical Theory which is an extension of a Logical Decidable Theory?

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.

• $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)

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$.

• Thanks for the detailed answer. Do you know any natural example? For example, what happens if we require a finite number of symbols in the language (i.e., a finite signature)? This assumption would avoid the trick based on constants. – boumol Jan 30 '11 at 21:25
• You can do it also with a unary relation $U$, adding it, say, to Presburger arithmetic. The point is that the base theory remains decidable, since nothing about $U$ is determined, but since you have a definable sequence of objects like $\mathbb{N}$, you can now create $T_2$ to describe a particular c.e. non-decidable set. In this case, you have a finite signature. – JDH Jan 30 '11 at 21:48
• But wait a minute, I have to think about whether Presburger plus a unary relation really is decidable... – JDH Jan 30 '11 at 22:21
• Yes, that's right. So let's use the same idea, but with a discrete order with a minimal and no maximal element, plus a unary relation. We can still define every element of the initial $\omega$-sequence, and so the trick of coding $U$ on that set will still work. So the question is just whether the theory of a discrete order with min + no max is still decidable in the language with an extra unary predicate, which I think is the case... – JDH Jan 31 '11 at 0:36
• To resolve the earlier question: I think that Presburger arithmetic with a unary predicate is NOT decidable. It seems possible to write down axioms that express that the unary predicate codes the graph of the multiplication function (or any binary or higher-arity relation), by having blocks of length $a$ and $b$ followed by a block of length $ab$, plus suitable separating blocks, in $U$. In the language of $+$ and $U$, it seems you could write down the inductive defining property of multiplication. This implies that Presburger arithmetic in the language with $U$ cannot be decidable. – JDH Jan 31 '11 at 1:34

Since you aren't requiring that $T_2$ is recursively axiomatized, you can do this in a silly way. Choose a nonrecursive subset $A$ of $\mathbb{N}$, and let the signature consist of countably many constants $c_n$. Let $T_1$ be the empty theory, and $T_2$ be the theory whose axioms are $c_i=c_j$ whenever $i$ and $j$ are both in $A$. Then $T_1$ is decidable but $T_2$ is not.

• OK. I edit the question to avoid these "pathological" cases. – boumol Jan 30 '11 at 18:44
• Your edit does not avoid this counterexample, since in fact every c.e. theory has a computable set of axioms. One just takes enormous conjunctions of the axioms above, so that the length of the conjunction tells you how long to wait in the computable enumeration. The result is a decidable set of axioms for the same theory. – JDH Jan 30 '11 at 20:50
• Yes, you are right (Craig's trick). – boumol Jan 30 '11 at 21:17