I'm a little out of my depth here, so sorry if my comments don't make sense.
I'm not an expert either, so I'm probably just being unclear
That's supposed to be a r.e. set of axioms, not a single axiom, right? I can easily imagine the program that successively prints the axioms R(x) for all x in L, but how do you enumerate the axioms not R(x) for all x not in L, given that L is only r.e. and not recursive? Or am I missing some easy way to have the whole thing as a single axiom without pulling in the machinery for running arbitrary programs and such?
The axioms don't need to be r.e. If they were, the oracle would never be more helpful than a halting oracle, no?
I don't completely understand why there won't be an accidental smart thing among all the silly things...
I don't either. It's just a strong intuition which I'm not sure I can justify, and which might be wrong.
ETA: By silly, I don't necessarily mean as simple as the examples I gave. Basically if you have a formula phi(S(x), T, F), which holds for arbitrary sentences S(x), provably true T, and provably false S, then you can replace S(x) with R(x), T with R(x in L), and S with R(x not in L). Not sure if that was well explained, but yeah.
At least it looks like my answer is correct :). Also my proof should generalize, if it does work. So I would have guessed that Feferman's (stronger) result was true, and I wouldn't be surprised if the argument was along these lines, though maybe the details are harder.
If they were, the oracle would never be more helpful than a halting oracle, no?
But we want the oracle to be less helpful than the halting oracle...
Anyway, the question is settled now, thanks a lot :-)
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.