Yes, there is a problem there. In a nonstandard model it would say that G is provable, while it isn't. — alcontali

But we're discussing non-standard models where ~G is true. Since ~G says that G is provable then, if ~G is true, G is provable.

However since G isn't derivable from the axioms of the theory, G is not provable. Therefore there can be no models where ~G is true.

Which would seem to render discussion of models with ~G as true as moot.

Therefore there can be no models where ~G is true. — Andrew M

There are, and they are arithmetically unsound: Arithmetic unsoundness for models with ~G true.

Going back to this again.

Yes, there is a problem there. In a nonstandard model it would say that G is provable, while it isn't. — alcontali

Consider a non-standard model where ~G is true.

Since ~G says that G is provable then, if ~G is true, G is provable. Now ~G is true (in that model) therefore G is provable (in that model).

It seems you disagree with this. Which part and why?

Since ~G says that G is provable then, if ~G is true, G is provable. Now ~G is true (in that model) therefore G is provable (in that model). It seems you disagree with this. Which part and why? — Andrew M

Concerning "G is provable (in that model)", it should be phrased as "G is provable (in the theory of which M is a model)". Sentences are true or false in a model. Sentences are provable or unprovable in a theory.

Concerning "Arithmetic unsoundness for models with ~G true", the very first remark to make is that the model is unsound. The model contains a sentence ~G as true, while it is false. That is unsound.

Inconsistency, however, means that both ~G and G would be provable from the theory. This is not the case, because neither are provable. Hence, the theory is consistent but one of its models is unsound.

The nonstandard model is indeed unsound but that does not make the theory inconsistent.

• Unsound model: it has true sentences that are actually false.
• Inconsistent theory: it is possible to prove a sentence as well as its negation.

Concerning "Since ~G says that G is provable then, if ~G is true, G is provable", no. The model says this, but it simply says something wrong.

G is not provable. ~G is also not provable. Therefore, ~G being true, is simply wrong in the model.

It just means that the model is unsound, meaning, that it contains a statement that of which it says that it is true, while it is actually false.

Thanks for your detailed reply - definitely helpful for working through this.

However that Wikipedia link doesn't provide an external reference and a search on "arithmetic unsoundness" doesn't return anything useful. From my own investigation, it seems instead that ~G being true is understood as correct for non-standard models. See the quotes below.

Any model in which the Gödel sentence is false must contain some element which satisfies the property within that model. Such a model must be "nonstandard" – it must contain elements that do not correspond to any standard natural number (Raatikainen 2015, Franzén 2005, p. 135). — Truth of the Gödel sentence - Wikipedia (italics mine)

Namely, if there are independent statements such as GF, F must have both models which satisfy GF and models which rather satisfy ¬GF. As ¬GF is equivalent to ∃xPrfF(x, ⌈GF⌉), the latter models must possess entities which satisfy the formula PrfF(x, ⌈GF⌉). And yet we know (because PrfF(x, y) strongly represents the proof relation) that for any numeral n, F can prove ¬PrfF(n, ⌈GF⌉). Therefore, no natural number n can witness the formula. It follows that any such non-standard model must contain, in addition to natural numbers (denotations of the numerals n), “infinite” non-natural numbers after the natural numbers. — 2.6 Incompleteness and Non-standard Models - SEP (italics mine)

On the other hand, I completely agree that in the model M, the sentence G loses its intuitive meaning. That’s the key to this business.

G is a statement that’s all about natural numbers. It’s supposed to encode the English language statement “I am unprovable”. But what it actually says is a bit more like this:

“There is no natural number n that is the number of a proof of this statement”.

(The idea, remember, is that Gödel figured out a way to assign numbers to proofs.)

However, the model M contains nonstandard natural numbers as well as the usual ones. In the model M, one of these nonstandard numbers is the number of a proof of G. So, G does not hold in the model M.

So, G doesn’t hold in M, but that’s because M has nonstandard numbers. We can loosely say that there’s a nonstandard number which is the number of an “infinitely long proof” of G. — John Baez - professor of mathematics at the University of California, Riverside

“There is no natural number n that is the number of a proof of this statement”. So, G doesn’t hold in M, but that’s because M has nonstandard numbers. We can loosely say that there’s a nonstandard number which is the number of an “infinitely long proof” of G. — John Baez - professor of mathematics at the University of California, Riverside

That sounds intriguing and intuitively correct, but unfortunately, also difficult to verify, because these nonstandard numbers are infinite cardinalities. So, yes, if there is a proof it will be encoded in one of these infinite cardinalities, which is indeed not a natural number n.

That sounds intriguing and intuitively correct, but unfortunately, also difficult to verify, because these nonstandard numbers are infinite cardinalities. So, yes, if there is a proof it will be encoded in one of these infinite cardinalities, which is indeed not a natural number n. — alcontali

Yes.

So I think there's a lot of baggage that comes along with accepting the Gödel sentence in one's logic system. I suggest that the sentence is not truth-apt.