For you final question, I find it hard to imagine a notion of “formal system” that does not just mean “language.” Then an RE formal system is the same as an RE language. If you insist on the terminology of proofs, you can take the words of the language as axioms and not have any rules of inference.
For you final question, I find it hard to imagine a notion of “formal system” that does not just mean “language.” Then an RE formal system is the same as an RE language. If you insist on the terminology of proofs, you can take the words of the language as axioms and not have any rules of inference.
How about http://en.wikipedia.org/wiki/First-order_logic#Syntax ?
So you agree that “provability oracle for an RE formal system” is the same as “membership oracle for an RE language” and your question is trivial?
ETA: No, first order languages does restrict the set of languages. But I object to this usage. “Formal systems” should include more general systems.