I looked it up, and it seems like what you’re referring to as soundness is called “arithmetic soundness.” The soundness I know doesn’t require a notion of standard model. It simply says that anything provable syntactically is also true in every model/interpretation. This is automatically true for any theory in first order logic. (Note that my version of soundness is the correct analogue of completeness, which is also true for any FOL theory, as Godel showed, less trivially.)
It’s just a different meaning of the word “soundness”. The soundness you’re talking about is really a property of a deductive system in first-order logic, as you point out. The soundness I’m talking about is a property of a theory w.r.t. a particular notion of truth defined for first-order formulas (and it’s usually defined by fixing a structure and an interpretation, in that structure, of the logic’s constant/function/relation symbols; in other words, a model). You’re right that sometimes, when talking about the model N, it’s referred to as “arithmetic soundness”, but the modifier is not at all required. E.g. search for “a theory T is sound” on Google as a phrase, with quotation marks, to see usage examples. Or search for “sound” in this post:
http://rjlipton.wordpress.com/2011/03/30/random-axioms-and-gdel-incompleteness/
Compare with the word “completeness”, which, I’m sure you’re aware, is also notoriously ambiguous: in “Godel’s completeness theorem” and “Godel’s incompleteness theorems” it refers to two totally different kinds of completeness. The difference between them is similar, though not identical, to the one between soundness as a property of a first-order logic and soundness as a property of a theory.
So here, the oracle says something of the form “exists x such that T halts after x steps”. Omega-consistency guarantees that there is some actual standard number N so that “T halts after N steps” is provable/true.
Well, not quite. Why do you think that omega-consistency guarantees that? What is it about omega-consistency that guarantees anything to be true? It only speaks of things that are provable/nonprovable.
Let me try to be a bit more detailed. You actually need your theory S (the one you have an oracle for, be it PA or something else) to uphold two separate requirements:
When S proves a sentence of the form “Exists x such that T halts after x steps”, you need that sentence to be true. This sentence is a Sigma1 sentence (let me know if I need to detail that further).
When there is a true sentence of the form “this is a run of T that ends after N steps” (which is a Sigma0 sentence), you need S to be able to prove it. This is what the original post means when it says “the oracle would have found a long and boring proof...”—you need this proof to actually exist! If S is too weak, it might not exist.
If you have both conditions, then the argument in the original post—the one that says an oracle for S can service as an oracle for the halting problem—goes through. In detail: if S proves T halts, by 1. T in fact halts. If S does not prove T halts, S cannot possibly prove “This is a run of T that ends after N steps” for any particular N, because if it could, it would also prove “T halts” by straightforward generalization. Therefore by 2. this cannot be true for any particular N, therefore T doesn’t halt.
So far, omega-consistency is not even in the picture. How does it come in? The easiest way to ensure 1. and 2. is simply to require that
(i) S is Sigma1-sound, that is, every Sigma1 sentence it proves must be true.
(ii) S is Sigma0-complete, that is, every true Sigma0 sentence is provable in S.
It turns out that (ii) is a fairly weak requirement, and every S that is strong enough to prove some basic statements about +, * and < satisfies it. The exact statement is that S must be stronger than Robinson’s theory R. And, given (ii), (i) is in fact implied by omega-consistency. By itself, omega-consistency of S doesn’t imply (i), but combined with Sigma0-completeness of S, it does. And here’s why:
Let P be a Sigma1 sentence of the form “There exist x such that R(x)” provable in S, where R is Sigma0. Suppose P is actually false, and then R(N) is false for every specific N, then not-R(N) is true for
every specific N, and it is provable in S for every specific N, by Sigma0-completeness. This directly contradicts the omega-consistency of S. Therefore P is true, and S is Sigma1-sound.
To sum up, it is enough to demand that S be omega-consistent if also it is strong enough to ensure that it is Sigma0-complete, and that requirement works two duties: both to translate omega-consistency into Sigma1-soundness which is what the argument really needs, and directly for the second half of the argument itself.
Phew. Hope I didn’t make any stupid mistake there. Let me know if anything’s unclear or disagreeable to you.
P.S. Note that the argument above depends crucially on the notion of what is “true”, which is defined in the model N of natural numbers. You cannot apply it to some theory S which isn’t able to speak of natural numbers at all (in fact, omega-consistency cannot be defined for such an S) or doesn’t have the basic machinery of arithmetic functions and relations (because it’s used to translate assertions about Turing machines into arithmetical statements). Thus my original remark that the argument depends on soundness of S. It was too broad in the sense that if you analyze the matter closely, you see that only Sigma1-soundness and not general soundness is required, as explained above, and that can be satisfied with omega-consistency and some modest strength. But the semantic requirements of having to talk about N and true statements doesn’t go away (because you can’t define Sigma0-completeness without that, and you do crucially need that for the argument to go through).
It’s just a different meaning of the word “soundness”. The soundness you’re talking about is really a property of a deductive system in first-order logic, as you point out. The soundness I’m talking about is a property of a theory w.r.t. a particular notion of truth defined for first-order formulas (and it’s usually defined by fixing a structure and an interpretation, in that structure, of the logic’s constant/function/relation symbols; in other words, a model). You’re right that sometimes, when talking about the model N, it’s referred to as “arithmetic soundness”, but the modifier is not at all required. E.g. search for “a theory T is sound” on Google as a phrase, with quotation marks, to see usage examples. Or search for “sound” in this post: http://rjlipton.wordpress.com/2011/03/30/random-axioms-and-gdel-incompleteness/
Compare with the word “completeness”, which, I’m sure you’re aware, is also notoriously ambiguous: in “Godel’s completeness theorem” and “Godel’s incompleteness theorems” it refers to two totally different kinds of completeness. The difference between them is similar, though not identical, to the one between soundness as a property of a first-order logic and soundness as a property of a theory.
Well, not quite. Why do you think that omega-consistency guarantees that? What is it about omega-consistency that guarantees anything to be true? It only speaks of things that are provable/nonprovable.
Let me try to be a bit more detailed. You actually need your theory S (the one you have an oracle for, be it PA or something else) to uphold two separate requirements:
When S proves a sentence of the form “Exists x such that T halts after x steps”, you need that sentence to be true. This sentence is a Sigma1 sentence (let me know if I need to detail that further).
When there is a true sentence of the form “this is a run of T that ends after N steps” (which is a Sigma0 sentence), you need S to be able to prove it. This is what the original post means when it says “the oracle would have found a long and boring proof...”—you need this proof to actually exist! If S is too weak, it might not exist.
If you have both conditions, then the argument in the original post—the one that says an oracle for S can service as an oracle for the halting problem—goes through. In detail: if S proves T halts, by 1. T in fact halts. If S does not prove T halts, S cannot possibly prove “This is a run of T that ends after N steps” for any particular N, because if it could, it would also prove “T halts” by straightforward generalization. Therefore by 2. this cannot be true for any particular N, therefore T doesn’t halt.
So far, omega-consistency is not even in the picture. How does it come in? The easiest way to ensure 1. and 2. is simply to require that
(i) S is Sigma1-sound, that is, every Sigma1 sentence it proves must be true. (ii) S is Sigma0-complete, that is, every true Sigma0 sentence is provable in S.
It turns out that (ii) is a fairly weak requirement, and every S that is strong enough to prove some basic statements about +, * and < satisfies it. The exact statement is that S must be stronger than Robinson’s theory R. And, given (ii), (i) is in fact implied by omega-consistency. By itself, omega-consistency of S doesn’t imply (i), but combined with Sigma0-completeness of S, it does. And here’s why:
Let P be a Sigma1 sentence of the form “There exist x such that R(x)” provable in S, where R is Sigma0. Suppose P is actually false, and then R(N) is false for every specific N, then not-R(N) is true for every specific N, and it is provable in S for every specific N, by Sigma0-completeness. This directly contradicts the omega-consistency of S. Therefore P is true, and S is Sigma1-sound.
To sum up, it is enough to demand that S be omega-consistent if also it is strong enough to ensure that it is Sigma0-complete, and that requirement works two duties: both to translate omega-consistency into Sigma1-soundness which is what the argument really needs, and directly for the second half of the argument itself.
Phew. Hope I didn’t make any stupid mistake there. Let me know if anything’s unclear or disagreeable to you.
P.S. Note that the argument above depends crucially on the notion of what is “true”, which is defined in the model N of natural numbers. You cannot apply it to some theory S which isn’t able to speak of natural numbers at all (in fact, omega-consistency cannot be defined for such an S) or doesn’t have the basic machinery of arithmetic functions and relations (because it’s used to translate assertions about Turing machines into arithmetical statements). Thus my original remark that the argument depends on soundness of S. It was too broad in the sense that if you analyze the matter closely, you see that only Sigma1-soundness and not general soundness is required, as explained above, and that can be satisfied with omega-consistency and some modest strength. But the semantic requirements of having to talk about N and true statements doesn’t go away (because you can’t define Sigma0-completeness without that, and you do crucially need that for the argument to go through).