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?

  • 3
    $\begingroup$ 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. $\endgroup$ – Carl Mummert Apr 11 '18 at 12:24

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

  • 1
    $\begingroup$ +1 You can also look at $\phi\wedge\phi\wedge ...\wedge\phi$ ($n$ times), which has the same effect. $\endgroup$ – Noah Schweber Apr 11 '18 at 14:59
  • $\begingroup$ Not very deep, but nonetheless discovered quite lately in 1953... $\endgroup$ – StefanH Apr 11 '18 at 15:15
  • $\begingroup$ @StefanH: I'm not sure I would call that "lately". Robust general concepts of "recursively enumerable" and "decidable" have only been around since the mid-late 1930s, so it only took 15-20 years for someone to get around to writing this down. It has been close to four times as long since 1953. $\endgroup$ – hmakholm left over Monica Apr 11 '18 at 15:32
  • $\begingroup$ Yes, but in 1953 formal logic was already well developed, Gödels famous theorem where known, different characterisations of partial recursive (Kleene, Church, Turing...) and recursive, examples of decidable theories where known... so the theory was already quite mature. $\endgroup$ – StefanH Apr 11 '18 at 15:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.