I know this question has been investigated in other threads, but I would like to pose yet another question on Gödel's theorem incompleteness, and truth in 'the standard model' compared with provability in the 'formal model'.
I will use the language of Gensler's little book "Gödel's Theorem Simplified" (see here for a summary).
For what Gensler calls System C, he gives an outline for how to construct a wff in system C. The system C the symbols are /, (, ), - , n (for a variable), nn (another variable),...etc.).
The reference numbers for system C formulas (like Godel numbers) are defined too.
For example the ref # for / is 1, the reference # for the variable n is 8, etc.
Then Gensler gives instructions for how to create a formula called F which states
(F) "There is no system C proof for the son of the system C formula with reference # n ".
Here n is a variable. So the system C formula with reference # n exists, call that system C formula XX, and F is the statement that the system C son of XX, SonXX, is not a theorem in system C).
F is a string of symbols of system C.The son of F is obtained by taking the reference number (an actual whole number like 112278 etc) for F, writing that whole number as the system C string //.../ (with reference # of F many /'s appearing) and replacing each occurrence the variable n in (F) with that many ///.../.
The result is a new system C formula, the son of F, called G.
The 'standard model' interpretation of G is then
(G) "There is no system C proof for the son of the system C formula with reference # equal to the reference # of F."
In other words, there is no system C proof of G itself.
Then Gensler and other sources indicate this standard interpretation of G is true, so it is a true 'ordinary arithmetic' statement, for which the corresponding system C formula has no proof.
It seems to me that what you can really say is this:
If you assume that the standard interpretation of G is a true statement in the ordinary standard model, then the corresponding system C formula is an unprovable system C formula. So you have a 'true' ordinary arith statement which cannot be proved in system C, BECAUSE you have ASSUMED that the standard model version of G is true.
If you assume that the standard interpretation of G is a false statement in the ordinary standard model, then the corresponding system C formula is an provable system C formula.So you have a 'false' ordinary arith statement which can be proved in system C, BECAUSE you have ASSUMED that the standard model version of G is false.
But how do you know that one of the two statements " G is a true statement in the ordinary standard model" or " G is a false statement in the ordinary standard model" must be valid?
Isn't the best you can say that IF you could determine that G were a true statement in the ordinary standard model" or " G is a false statement in the ordinary standard model" THEN you can draw conclusions about non provability or provability of G as a system C formula?