Are you confusing soundness with consistency? omega-consistency is much weaker than soundness.
Consistency: a syntactic claim that it's impossible to derive a contradiction. Doesn't require a notion of truth to be useful.
Omega-consistency: a syntactic claim that it's impossible to prove certain statements together. Doesn't need a notion of truth, but is motivated by the standard model of natural numbers.
Soundness: a semantic claim that given a specific notion of "true" as applies to a statement, e.g. truth in the model N of natural numbers, all the axioms of the theory are true. Automatically implies both consistency and omega-consistency. Requires a notion of the "intended model" or a "standard model" for the theory in which we consider the truth of propositions. For example, soundness is meaningless to talk about in the case of ZFC, which doesn't have an intended model.
I think this argument holds as long as the other formal system is recursively enumerable, and if PA is omega-consistent.
Look at this sentence from the argument:
"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."
If the oracle for a formal system S says "yes" on a given statement S that encodes the proposition "a Turing machine T will halt on this input", this means that S proves this proposition. It does not mean that the proposition is true and T will in fact halt! For that to be true, you need the formal system S to be sound. S could easily be omega-consistent and not sound, in which case it'll lie to you (example, assuming you believe PA to be consistent: the formal system.
Soundness: a semantic claim that given a specific notion of "true" as applies to a statement, e.g. truth in the model N of natural numbers, all the axioms of the theory are true. Automatically implies both consistency and omega-consistency. Requires a notion of the "intended model" or a "standard model" for the theory in which we consider the truth of propositions. For example, soundness is meaningless to talk about in the case of ZFC, which doesn't have an intended model.
I looked it up, and it seems like what you're referr...
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.