Is there a formal system (not talking about the standard integers, I guess) whose provability oracle is strictly weaker than the halting oracle, but still uncomputable?
I did some reading and it looks like while there are some proofs of the existence of a dense set of intermediate Turing degrees, it’s a bit difficult to pin down definite problems of intermediate degree. I found one paper that postulates a couple of possibly intermediate degree problems.
This article (same author) talks about some of the surrounding issues and some the difficulties with proving the existence of an intermediate computational process.
Given those difficulties, it isn’t clear to me that intermediate proof oracles for formal systems exist and if they do it seems like that might be non-trivial, but I’m definitely not the best person to ask.
In a similar vein, it was shown by Feferman that derivability in a formal theory fully reflects the structure of the r.e. degrees: for every r.e. degree d there is an axiomatizable theory whose collection of theorems has degree exactly d, see [10].
And [10] resolves to:
[10] S. Feferman. Degrees of unsolvability associated with classes of formalized theories. J. Symbolic Logic, 22:161–175, 1957.
I guess that’s enough information to answer my question. Thanks a lot!
I found another paper with an interesting result (unfortunately behind a pay wall). It asks what range of degrees occur for subtheories of arithmetic and concludes that a degree a is associated with these theories iff it’s a complete degree. What does that mean?
Definition 10 A degree of recursive unsolvability a is said to be complete if there exists a degree b such that b’ = a (According to Freiberg’s theorem [6, p.265] a degree a is complete iff 0′<= a).
That makes sense because b’ is basically a Turing jump from b, but it’s bad because 0′ is the degree of the halting problem. The first Turing jump from deciable theories is of degree equal to the halting problem. So it looks like any undecidable (in distinction from Presberger and other decidable theories) first order subsystems of arithmetic, which to me would be the most intuitive theories, are going to be at least as strong as the halting problem. That is, if I’m reading this right—proof theory is sort of a hobby and I’m mostly self-taught.
A more specific statement of the result from the paper is:
Lemma 1 Suppose that the theory T is omega consistent with repsect to some formula P(y) and that T has a finitely axiomatizable subtheory S satisfying
(i) Each recursive relation is definable in S
(ii) For every m = 0, 1, ….,
)
Then each subtheory of T is of complete degree
Also:
Corallary 6 Let T be the theory ZF or any extension of ZF. If T is omega consistent with respect to the formula yinomega then the degrees of subtheories of T are exactly the complete degrees.
ETA: Is this what you were referring to in:
Is there a formal system (not talking about the standard integers, I guess)
I’m not sure, I don’t see a related reply/comment. Either way, I’m not 100% sure I’m following all of the arguments in the papers, but it appears that the theories that are of intermediate degree are necessarily very unusual and complicated, and I’m not sure how feasible it would be to construct one explicitly.
ETA2: I found yet another interesting paper that seems to state that finding a natural example of a problem of intermediate degree is a long standing open problem.
I did some reading and it looks like while there are some proofs of the existence of a dense set of intermediate Turing degrees, it’s a bit difficult to pin down definite problems of intermediate degree. I found one paper that postulates a couple of possibly intermediate degree problems.
This article (same author) talks about some of the surrounding issues and some the difficulties with proving the existence of an intermediate computational process.
Given those difficulties, it isn’t clear to me that intermediate proof oracles for formal systems exist and if they do it seems like that might be non-trivial, but I’m definitely not the best person to ask.
A quote from your last link:
And [10] resolves to:
I guess that’s enough information to answer my question. Thanks a lot!
Something is going on with my comment, the middle section keeps disappearing.
I found another paper with an interesting result (unfortunately behind a pay wall). It asks what range of degrees occur for subtheories of arithmetic and concludes that a degree a is associated with these theories iff it’s a complete degree. What does that mean?
That makes sense because b’ is basically a Turing jump from b, but it’s bad because 0′ is the degree of the halting problem. The first Turing jump from deciable theories is of degree equal to the halting problem. So it looks like any undecidable (in distinction from Presberger and other decidable theories) first order subsystems of arithmetic, which to me would be the most intuitive theories, are going to be at least as strong as the halting problem. That is, if I’m reading this right—proof theory is sort of a hobby and I’m mostly self-taught.
A more specific statement of the result from the paper is:
Also:
ETA: Is this what you were referring to in:
I’m not sure, I don’t see a related reply/comment. Either way, I’m not 100% sure I’m following all of the arguments in the papers, but it appears that the theories that are of intermediate degree are necessarily very unusual and complicated, and I’m not sure how feasible it would be to construct one explicitly.
ETA2: I found yet another interesting paper that seems to state that finding a natural example of a problem of intermediate degree is a long standing open problem.
Thanks again for taking the time to parse all that!
Yeah, kind of. I didn’t know the results but for some reason felt that subtheories of arithmetic shouldn’t lead to intermediate degrees.
No problem! It’s an interesting topic with lots of surrounding results that are somewhat surprising (at least to me).