I believe the answer to your question is yes. I’m going to just interpret “formal system” as “first order theory”, and then try to do the most straightforward thing.
Take a language L of intermediate degree, as constructed via the priority method. I’d like to just take the strings (or numbers) in this language to be the theory’s axioms. So let the theory have some 1-ary relation, call it R, as well as +, and constants 0 and 1. Assert that everything has a successor, just to get the “natural numbers” (without having multiplication though). Then just include the axiom that says R(x) for all x in L, and not R(x) for all x not in L.
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 has the same degree as an oracle for L.
Don’t feel like thinking about how to say/prove this part formally, but maybe someone can help (or correct) me. Also, for reference, Presburger arithmetic is basically arithmetic without multiplication, and is decidable.
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 believe the answer to your question is yes. I’m going to just interpret “formal system” as “first order theory”, and then try to do the most straightforward thing.
Take a language L of intermediate degree, as constructed via the priority method. I’d like to just take the strings (or numbers) in this language to be the theory’s axioms. So let the theory have some 1-ary relation, call it R, as well as +, and constants 0 and 1. Assert that everything has a successor, just to get the “natural numbers” (without having multiplication though). Then just include the axiom that says R(x) for all x in L, and not R(x) for all x not in L.
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 has the same degree as an oracle for L.
Don’t feel like thinking about how to say/prove this part formally, but maybe someone can help (or correct) me. Also, for reference, Presburger arithmetic is basically arithmetic without multiplication, and is decidable.
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.