Note: By "theory" I mean a set of sentences, not assumed to be closed under logical consequence (otherwise the question would be trivial).
Comments/ideas:
- There's a well-known result that every complete axiomatizable theory is decidable. This is asking a converse question. (If adding completeness as a hypothesis changes things, I'm interested in that as well.)
- Suppose $T$ is known to be decidable. Given an input $n$ which is the Godel code of a sentence $\phi$, we can computably determine whether $\phi$ is a theorem of $T$. Then, if we could computably come up with at least one proof of $\phi$, a bounded-minimalization construction ought to yield (I think) the shortest proof of $\phi$, and by checking whether this proof had length 1 we could determine whether $\phi$ is an axiom of $T$. The question is whether, knowing that $\phi$ is a theorem of $T$, we can effectively produce at least one proof of it without knowing that $T$ is axiomatizable.
- The unary relation Thm$_T(\cdot)$ such that Thm$_T(n)$ means "$n$ is the code of a sentence $\phi$ which is a theorem of $T$" can be defined in terms of the binary relation Prf$_T(\cdot,\cdot)$ such that Prf$_T(n,x)$ means "$n$ is the code of a sentence $\phi$ and $x$ is the code of a proof of $\phi$ from $T$"; explicitly, Thm$_T(n)$ is equivalent to $\exists x $Prf$_T(n,x)$. Hence, if we know Prf$_T(\cdot,\cdot)$ to be recursive (e.g. if $T$ is axiomatizable), we could conclude that Thm$_T(\cdot)$ is semirecursive. What about the converse? If we know Thm$_T(\cdot)$ is recursive, can we conclude anything about Prf$_T(\cdot,\cdot)$?
- The only non-axiomatizable theories I can think of off the top of my head (e.g. the set of sentences in the language of arithmetic which are true in $\mathbb{N}$) are also undecidable, so that doesn't help in looking for a possible counterexample.
Best Answer
I assume that "axiomatizable" means that there's a decidable set of axioms (which are all theorems of $T$) such that every theorem of $T$ can be proved from these axioms.
I assume that "$T$ is decidable" means that there's an algorithm that determines whether a given wff is a theorem of $T$.
In that case, simply declare that every theorem of $T$ is now an axiom. There, you have (decidably) axiomatized it, so it must have been axiomatizable.
If you mean finitely axiomatizable, then Presburger arithmetic is an example of a theory that is complete and decidable but not finitely axiomatizable.
It was clarified in comments that you're looking for (I think) a non-decidable set of axioms whose set of consequences is decidable. But that is easy enough too:
Let $U$ be the set of theorems in your favorite decidable theory (such as, again, Presburger arithmetic). Let $A$ be your favorite undecidable set of natural numbers (such as the set of indices of halting Turing machines). Then consider $$ T=U\setminus\{\underbrace{x=x\land x=x\land\cdots\land x=x}_{n\text{ conjuncts}} \mid n\in A\}$$