There is an objective definition of truth in any particular model. For any particular model M of, say, Peano arithmetic, there is an objective, unambiguous, perfectly well-defined notion of truth in that model (of course, the definition of truth cannot itself be formalized within the model).
> There is an objective definition of truth in any particular model.
"in any particular model" - this is exactly parent's point.
From Wikipedia, a restatement of the 1st incompleteness theorem:
> there are statements of the language of F which can neither be proved nor disproved in F
The truth of a proposition P, within F, means "P is an axiom of F, or can be proved in F".
Saying "there are statements of the language of F which can neither be proved nor disproved in F... but the statements are true nevertheless" is appealing to some 'objective notion' of truth that transcends F.
>The truth of a proposition P, within F, means "P is an axiom of F, or can be proved in F".
No, truth and proof are NOT the same thing. The system F needn't have any notion of truth. For example, Peano arithmetic has no notion of truth. Peano arithmetic has notions of zero, successor, addition, and multiplication--none of truth.
Almost all competent mathematicians would agree that there exist theorems in the language of PA which are neither provable nor disprovable in PA but which are nevertheless true. Here, "true" means "true in the standard model of PA", not "true according to PA"---the latter isn't even meaningful because there is no such thing as "truth according to PA".
1. The original example would be Goedel's own example, namely, the statement (formulated in the language of PA) that PA is consistent, i.e., that PA does not prove 1=0.
