# A recursively enumerable theory without a decidable set of axioms.

A theory is a set of first order sentences over some signature. A set of sentences are called axioms for the theory, if the deductive closure of the axioms equals the theory.

Now, if I have a recursively enumerable set of axioms, then the theory is recursively enumerable. For example we could enumerate up to the $i$-th axiom, compute all deductions of length $i$, then continue with $i+1$.

Do you know an example of a recursively enumerable theory, that does not has a decidable set of axioms?

• There is a standard theorem that an r.e. theory always has a computable set of axioms, and in fact a primitive recursive set of axioms. – Carl Mummert Apr 11 '18 at 12:24

This is not particularly deep: If you have a machine accepting the axioms of the theory, just replace every axiom $\phi$ with $$\phi\land (\underbrace{(x=x)\lor (x=x) \lor \cdots \lor (x=x)}_n )$$ where $n$ is exactly the number of steps the machine takes to accept $\phi$. Then whether you're looking at one of these new axioms can be decided simply by counting the number of $(x=x)$ disjuncts on the right and running the acceptor for that many steps on the formula on the left of $\land$.
• +1 You can also look at $\phi\wedge\phi\wedge ...\wedge\phi$ ($n$ times), which has the same effect. – Noah Schweber Apr 11 '18 at 14:59