The division you see has to do with the level of conservativity of the theories in question. On the one hand, the theory ZFC + Con(ZFC) is not $\Pi^0_1$-conservative over ZFC since Con(ZFC) is a $\Pi^0_1$ sentence which is not provable from ZFC. On the other hand, CH is $\Pi^0_1$-conservative over ZFC since ZFC + CH and ZFC prove exactly the same arithmetical facts. Indeed, by the Shoenfield Absoluteness Theorem, ZFC and ZFC + CH prove exactly the same $\Sigma^1_2$ facts. In general, forcing arguments will not affect $\Sigma^1_2$ facts and so any statement whose independence is proved by means of forcing will be $\Sigma^1_2$-conservative over ZFC. By contrast, large cardinal hypotheses are not $\Pi^0_1$-conservative over ZFC.
An example of a natural statement that is independent of PA but nevertheless true is the Paris–Harrington Theorem, which is equivalent to the 1-consistency of PA. In other words, the statement is equivalent to the statement that every PA-provable $\Sigma^0_1$ sentence is true.
Yes, this line of thought is perfectly fine.
A set is decidable if and only if it has complexity
$\Delta_1$ in the arithmetic
hiearchy,
which provides a way to measure the complexity of a
definable set in terms of the complexity of its defining
formulas. In particular, a set is decidable when both it
and its complement can be characterized by an existential
statement $\exists n\ \varphi(x,n)$, where $\varphi$ has
only bounded quantifiers.
Thus, if you have a mathematical structure whose set of
truths exceeds this level of complexity, then the theory
cannot be decidable.
To show that the true theory of arithmetic has this level
of complexity amounts to showing that the arithmetic
hierarchy does not collapse. For every $n$, there are sets
of complexity $\Sigma_n$ not arising earlier in the
hierarchy. This follows inductively, starting with a
universal $\Sigma_1$ set.
Tarski's theorem on the non-definability of
truth
goes somewhat beyond the statement you quote, since he
shows that the collection of true statements of arithmetic
is not only undecidable, but is not even definable---it
does not appear at any finite level of the arithmetic
hiearchy.
Finally, it may be worth remarking on the fact that there
are two distinct uses of the word undecidable in this
context. On the one hand, an assertion $\sigma$ is not
decided by a theory $T$, if $T$ neither proves nor refutes
$\sigma$. On the other hand, a set of numbers (or strings,
or statements, etc.) is undecidable, if there is no Turing
machine program that correctly computes membership in the
set. The connection between the two notions is that if a
(computably axiomatizable) theory $T$ is complete, then its
set of theorems is decidable, since given any statement
$\sigma$, we can search for a proof of $\sigma$ or a proof
of $\neg\sigma$, and eventually we will find one or the
other. Another way to say this is that every computably
axiomatization of arithmetic must have an undecidable
sentence, for otherwise arithmetic truth would be
decidable, which is impossible by the halting problem (or
because the arithmetic hierarchy does not collapse, or any
number of other ways).
Best Answer
When we say the Gödel sentence is true, we mean exactly the same thing as when we say the Fundamental Theorem of Arithmetic is true, or Fermat’s Last Theorem, or any other theorem in mathematics. We mean that we’ve proven it, using our standard consensus principles for reasoning about mathematical objects. And when we talk about natural numbers — as in FTA, FLT, or the Gödel sentence — we mean the actual natural numbers, not arbitrary models of PA.
With FTA or FLT, we don’t usually even question that. The reason we look at Gödel’s sentence in other models of PA isn’t because of any difference or subtlety in what the statement means — it’s just a difference in why we’re interested in it. That difference comes back to the question of what principles we’re using in our proofs.
Most of the time, we just take those “standard principles” as an implicit background consensus, and don’t mention them explicitly. But with our logicians’ hats on, we may want to be more explicit about them. Most of the time, they’re assumed to be ZFC set theory or something closely equivalent. So we can refine our statement that “the FTA is true” (or FTA, the Gödel sentence, etc) to “in ZFC, we have shown the FTA is true”, or more formally “ZFC proves FTA”.
And then to further refine it, we can ask: did we really need the whole power of ZFC, or does some weaker logical system suffice? So we can ask whether these theorems are provable in PA, or any other logical theory T that has a way of talking about natural numbers. And only then can we start asking about whether these statements may hold in some models of T and fail in others. Which is an interesting question — and especially because in the case of the Gödel sentence, we can show it holds in some models and fails in others — but it’s very much a secondary one, and doesn’t affect the original primary meaning of the statement. And it depends entirely on what theory T is under consideration.
The one subtlety to note here is that if we’re talking about “PA proves FTA” and “ZFC proves FTA”, these can’t quite be formally the same statement “FTA”, since one must be written in the formal language of arithmetic, the other in the language of set theory. What’s happening here is that the ZFC-version of “FTA” is an translation of the PA-version of FTA in ZFC, using ZFC’s set of natural numbers. This translation is what “the standard model” means. But it’s just part of giving a more refined analysis of the logical status of these statements — it doesn’t mean that every time we do any elementary number theory in ZFC, we should feel obliged to add “in the standard model”. The whole point of a standard model is that it’s standard — it’s just giving the language of arithmetic its usual meaning within ZFC (or other ambient foundation). You can equally well take “FTA” to be the PA-statement and view the ZFC-version as its interpretation under the standard mode, or take “FTA” to be the ZFC-statement and view the PA-version as a transcription of it into the language of arithmetic. The former is more common in logic, but the latter is arguably closer to mathematical practice.
So overall: It’s completely accurate to just say “The Gödel sentence is true”, in the same sense that we mean when we say any other mathematical statement is true or false. But if we want to refine that statement to a sharper one, then what we should say is “ZFC proves the Gödel statement [in the standard model of arithmetic].” — the part that really sharpens the statement is specifying “ZFC”, not the mention of the standard model. Similarly, when we say that it is unprovable (or fails in some models), we need to be clear which theory we’re talking about provability in, or models of.
Edit. I’ve assumed we’re talking of the Gödel sentence for PA, or some similar theory of arithmetic; but the same applies with the Gödel sentence for ZFC, or any other theory $T$. In Gödel’s theorem, we assume $T$ comes equipped with an interpretation of the language of arithmetic, and its Gödel sentence $G_T$ is a priori a sentence of arithmetic, that then gets (in the proof of Gödel’s theorem) interpreted into $T$. So again what it means when we say $G_T$ holds is no different in principle from what it means when we say FTA or FLT holds — it means “reasoning in the normal mathematical way, we can prove $G_T$ holds (in the natural numbers)”. So there’s no difference from before what it means for $G_T$ to hold. And there’s a difference, but a straightforward one, in whether we can show $G_T$ holds: If $T$ is a theory that we can prove consistent (so e.g. PA would be such a theory, if we’re working ambiently in something like ZFC), then using that, we can prove unconditionally that $G_T$ holds. If we can’t prove $T$ is consistent (e.g. if $T$ is ZFC itself, or something stronger), then all we can prove is: If $T$ is consistent, then $G_T$ holds.