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
then the degrees of subtheories of T are exactly the complete degrees.
ETA: Is this what you were ref...
WARNING: this post requires some knowledge of mathematical logic and computability theory.
I was just talking with Wei Dai and something came up that seems at once obvious and counterintuitive. Though if the argument is correct, I guess it will be old news to about 50% of the people who read my posts :-)
Imagine you have an oracle that can determine if an arbitrary statement is provable in Peano arithmetic. Then you can try using it as a halting oracle: for an arbitrary Turing machine T, ask "can PA prove that there's an integer N such that T makes N steps and then halts?". If the oracle says yes, you know that the statement is true for standard integers because they're one of the models of PA, therefore N is a standard integer, therefore T halts. And if the oracle says no, you know that there's no such standard integer N because otherwise the oracle would've found a long and boring proof involving the encoding of N as SSS...S0, therefore T doesn't halt. So your oracle can indeed serve as a halting oracle.
On the other hand, if you had a halting oracle to begin with, you could use it as a provability oracle for PA: "if a program successively enumerates all proofs in PA, will it ever find a proof for such-and-such statement?"
So having a provability oracle for PA or any other consistent formal system that proves some valid arithmetic truths (like ZFC) is equivalent to having a halting oracle, and thus leads to a provability oracle for any other formal system. In other words, if you knew all about the logical implications of PA, then you would also know all about the logical implications of ZFC and all other formal systems. Hee hee.
ETA: this line leads to a nontrivial question. 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?
ETA 2: the question seems to be resolved, see Zetetic's comment and my reply.