The situation with Goedel sentence (let's call it G) is actually not very different. As neither G nor negation of G is provable, you could also say that it cont

The situation with Goedel sentence (let's call it G) is actually not very different. As neither G nor negation of G is provable, you could also say that it contains extra information, and add negation of G as a new axiom to PA, just like you could add CH to ZF. If you do that, you could wonder what your new arithmetic looks like. This is actually very interesting question. Since "not G" says basically "it's not true that there's no proof of me", or, more specifically, "it's not true that there's no number that represents the proof of me", it's clear that "not G" asserts the existence of a certain "natural" number being the proof of G, which is not one of the natural numbers we know (since no "regular" natural number represents the proof of G). In our new universe there are "natural" numbers that you cannot reach by counting. Because of that, one can construct many different nonequivalent "implementations" (models) of PA + not G, which are necessarily different than the standard implementation of artihmetic we know (1, 2 = S(1), 3 = S(S(1)), ..., n = S(S(...S(1)...)), with + and *). What is interesting about incompleteness theorem is that no matter if we add arbitrarily large number of axioms to PA, or even infinite number of axioms generated by computer program we write, the resulting system will still be incomplete, and each will have its own (many of them, actually) Goedel sentence.