How can you add 'not G' to a formal system without introducing omega inconsistency?

In any formal system S that is susceptible to Godel's proof, we can make a formula G which is undecidable. That should mean that we can add either $G$ or $\neg G$ as an axiom to S and still end up with a consistent system, but I'm not sure exactly how $S + \neg G$ can be consistent.

So, $G$ says: "There does not exist a number $n$, which is the Godel number for a proof of $G$." If G were provable, it would be false, and the system would be inconsistent (because $G$ implies $\neg G$). If $\neg G$ were provable, however, the system does not have to be blatantly inconsistent, but only omega-inconsistent. $\neg G$ says "There does exist a number $n$, which is the Godel number for a proof of $G$." But it doesn't specify what that number is. So S can still have theorems: "1 does not prove $G$", "2 does not prove $G$", "3 does not prove $G$" and so on, and it would only be omega-inconsistent (since there is no provable statement that is blatantly the negation of another). But we assume that $S$ is omega-consistent, so we are forced to conclude that $G$ is undecidable. Okay. (as a side-note, I thought that Godel's proof didn't need the assumption of omega-consistency, but it seems required here ... ?)

Now, I understand what happens when you add $G$ to S. In this new $S+G$ system, $G$ says, "There is no number which is the Godel number of a proof for $G$ in S", which is, of course, true (and presumably consistent).

But in $S + \neg G$, $\neg G$ says "There is a number which is the Godel number of a proof for $G$ in S"; yet, since every provable statement of $G$ is also provable in $S + \neg G$, this new system will also say "1 does not prove $G$ in S", "2 does not prove $G$ in S", ... and so on. So isn't $S + \neg G$ omega-inconsistent? And doesn't that go against the idea that we should be able to add either $G$ or $\neg G$ to S and still end up with a consistent system? Does that "consistency promise" not extend to omega-consistency? If not, isn't there a "logically better" way to extend S, even though both extensions are possible?

-
The notion of "number" in $S+\neg G$ is not the same. In fact, you want to understand $G$ as saying "there does not exist an '$S$-number' that is the number of a proof of $G$.", however, there well can be an "$S+\neg G$"-number that is a proof (and indeed there is), because you have new axioms, so your function "is a proof in $S$ of" is different from the function "is a proof in $S+\neg G$ of". Also, note that there are versions of Goedel's proof that avoid the issue of $\omega$-inconsistent. –  Arturo Magidin Apr 16 '12 at 20:55
In addition to Arturo's previous comment, your first paragraph is slightly wrong. No one guarantees that $S+G$ and $S+\lnot G$ are consistent. However if $S$ is consistent then so are $S+G$ and $S+\lnot G$. We simply did not introduce contradictions to the system, but we might not be able to prove the consistency of $S$. –  Asaf Karagila Apr 16 '12 at 21:02
@ArturoMagidin I understand that $\neg G$ in $S + \neg G$ talks about provability in $G$, but why would it talk about S numbers and not $S + \neg G$ numbers? I understand that the function "is provable in S" is different from the function "is provable in $S + \neg G$". But when I prove, in $S + \neg G$, that "there is a number that proves G in S" and "1 is not that number", "2 is not that number", etc., am I not talking about the same type of numbers in each case? –  Ord Apr 16 '12 at 21:03
@AsafKaragila But we assume the consistency of S, don't we? We assume it, and then go ahead and show that $S + \neg G$ must be omega-inconsistent! How does that work? Surely, Godel's proof does not say that a consistent formal system cannot exist? –  Ord Apr 16 '12 at 21:05
@Ord: The notion of "number" depends on the model; what you call a "number" in the model $M$ of $S$ need not be the same things that you call a "number" in the model $M'$ of $S+\neg G$. In particular, there can be "numbers" other than the ones that were already identified as "numbers" in $M$. Note that Goedel uses $\omega$-inconsistency in order to show that $\neg G$ cannot be a theorem; as I said, there are refinements of Geodel's argument that completely avoid the issue of $\omega$-inconsistency. –  Arturo Magidin Apr 16 '12 at 21:07

Your conclusion that $S+\neg G$ is not $\omega$-consistent is right. It is (assuming that $S$ is consistent) consistent, but fails to be $\omega$-consistent. Being $\omega$-consistent is a stronger condition than consistency, satisfied by fewer systems.

Would it be "logically better" to extend $S$ in an $\omega$-consistent way than in one that isn't? I don't think so. As a sometimes Platonist, I would certainly favor the extension $S+G$ over $S+\neg G$, perhaps even claiming that the former is true whereas the latter isn't, but that preference is not based on logical properties (being true is not a logical property).

Part of the confusion is that "$\omega$-consistency" is something of a misnormer -- because the name contains "consistency" one is tempted to think that like ordinary consistency it is an intrinsic property of the theory. But really it isn't; saying that a theory is $\omega$-consistent is a statement between the relation between what the theory proves and arithmetic at the meta-level. Being $\omega$-consistent is a necessary criterion for the theorems of the theory to be truths about the intuitive naturals, but failure to express arithmetic truth is not a logical problem for the theory -- it is innocent of our ambitions about what we might like it to model or not.

One might consider modifications of the concept of $\omega$-consistency such that it looks more intrinsic to the theory. For example we could define that a theory $T$ is $\omega'$-consistent iff, whenever $T\vdash \exists x. \phi(x)$ there is some closed term $t$ such that $T\vdash \phi(t)$. (The difference is that in ordinary $\omega$-consistency we require $t$ to be a "numeral"; the generalized definition allows arbitrary closed terms). However, under this generalization it is still not clear why one would consider $\omega'$-consistency to be a desirable property of theories in general, even if we don't intend the theory to model arithmetic.

-
Excuse my ignorance, but what exactly is a "closed term", and why would omega-prime-consistency be undesirable? –  Ord Apr 16 '12 at 23:25
A closed term is one that contains no variables -- such as $S(S(S(0)))+S(0)$ in the language of arithmetic opposed to $S(S(S(x)))+y$. -- I'm not saying that $\omega'$-consitency would be actively undesirable, just that I don't see why one would explicitly desire it. For example, ZFC is not $\omega'$-consistent, but I don't think one should count that as a disadvantage. –  Henning Makholm Apr 16 '12 at 23:31
Okay, thank you very much for your response! I think I have a much better handle on the situation now. –  Ord Apr 16 '12 at 23:40