A recursively enumerable theory without a decidable set of axioms.

791 Views Asked by At

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?

1

There are 1 best solutions below

4
On BEST ANSWER

As Carl Mummert pointed out in comments, Craig's theorem says that this is impossible. Every r.e. theory has a decidable (or even a primitive recursive) axiomatization.

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