I’m a little out of my depth here, so sorry if my comments don’t make sense.
Then just include the axiom that says R(x) for all x in L, and not R(x) for all x not in L.
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?
On second thought, maybe we don’t need the second part. Just having R(x) for all x in L could be enough.
It seems pretty clear that the only things this theory proves are things that FOL proves, silly things about the successor function, and silly things about R, like “forall x, R(x) → R(x)” and “(R(14) and R(12)) → R(17)” where R(14) is false. So an oracle for the logical implications of this theory is basically the same as an oracle for L.
I don’t completely understand why there won’t be an accidental smart thing among all the silly things...
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.
I’m a little out of my depth here, so sorry if my comments don’t make sense.
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?
On second thought, maybe we don’t need the second part. Just having R(x) for all x in L could be enough.
I don’t completely understand why there won’t be an accidental smart thing among all the silly things...
I’m not an expert either, so I’m probably just being unclear
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 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.
But we want the oracle to be less helpful than the halting oracle...
Anyway, the question is settled now, thanks a lot :-)
Oops sorry! Ignore what I said there. Anyways, the axioms aren’t necessarily r.e., but as far as I can tell, they don’t need to be.