Most proofs of undecidability for various theories (pure logic with binary relation, group theory, etc.) show that the natural numbers and Robinson's $Q$, in one form or another, can be encoded appropriately. Hence the decision problem for these theories is as hard as $K$, the halting set.

Are there are recursively axiomatized theories which are undecidable, but yet easier than $K$ (i.e. $K$ is not Turing reducible to deciding to the theory)?

  • 4
    $\begingroup$ Steve Simpson discusses the lack of natural examples of c.e. degrees between $0$ and $0'$ in this paper. $\endgroup$ Jul 6 '11 at 1:56

When I was looking around trying to find some inspiration to answer your question, I found the following result of Feferman from 1957:

For any set $X$ of natural numbers there is a theory $T(X)$ such that:

  • The set $X$ and the set of Gödel numbers of consequences of $T(X)$ have the same degree of unsolvability.

  • If $X$ is r.e. then $T(X)$ is effectively axiomatizable.

Because there are nonzero r.e. Turing degrees strictly weaker than $K$, I think this may answer the question.

The result is in the paper "Degrees of Unsolvability Associated with Classes of Formalized Theories", Solomon Feferman, The Journal of Symbolic Logic, Vol. 22, No. 2 (Jun., 1957), pp. 161-175. http://www.jstor.org/stable/2964178


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.