[jjcc]

May I suggest that "true" in "true-but-unprovable" means from God's eye or in a higher level system but not in current system because "unprovable"（in current system only) means it's not really true in current system? Correct me if I'm wrong in this context.

[hilbertseries]

You are wrong. Godel in fact showed precisely that there are unprovable statements in any consistent set of axioms. In fact it’s equivalent. The only systems in which every statement is provable are inconsistent. Consistent here meaning that statements cannot be proven to be both true and false from axioms.

[jfarmer]

There are two other conditions/premises that, arguably, play a bigger role in Gödel's theorems:

1. The theory must be strong enough to do a certain amount of arithmetic

2. The axioms of the theory must be computably enumerable

So, you can have relatively weak theories in which the incompleteness results don't hold. A major example here is comes from Gödel's _completeness_ theorem (notice "completeness" not "INcompleteness") which says: in first-order logic a statement is true if and only if its provable.

You can also have strong theories whose axioms are not computably enumerable. Start with something like the Peano axioms and consider the set of all true statements in that theory. We can take any set we want as axioms, so what if we take the set of all true statements in Peano arithmetic as our axioms?

Now every valid "proof" is one line long since what was previous a theorem is now an axiom, but we've kicked the can down the road. How do we figure out whether something is an axiom in this new system or not?

This latter system is called "true arithmetic" Gödel's incompleteness theorems don't apply there, either.

[dwohnitmok]

Godel's completeness theorem is not in opposition to his incompleteness theorems.

Godel's incompleteness theorems and completeness theorem can hold at the same time. They talk about two separate notions of completeness (the former about incompleteness in the sense of logical independence and the latter in the sense of the correspondence between semantics and syntax). Indeed Godel's incompleteness theorem is usually presented in the context of first-order Peano arithmetic.

This is again why I don't like talking about "truth." It is not completely inaccurate to say Godel's completeness theorem says "a statement is true if and only if it's provable." It is also not completely inaccurate to say Godel's incompleteness theorems say "some true statements are not provable." But the vagaries and philosophical baggage behind the two statements mean you have to tread _very_ carefully and without _extremely_ careful qualifications you can start making philosophical statements that are extrapolations of those theorems rather than the theorems themselves. That's why I strongly believe that it's much much much more productive to talk about incompleteness and consistency rather than truth.

[jfarmer]

You're right! I confused the deductive system/language w/ the theory. Oops.

Something like Presburger Arithmetic would've been a proper example.

[jjcc]

I'm not contradictory to your statement. Or your explanation hasn't touch my potential flaw if exists. Let me put in this way:

There is at least some "thing" that can not be proved without cause inconsistency. To avoid the inconsistency to prove the "thing" which become true we need to create a high order system in which then the "thing" is truth but also cause the same dilemma in the new bigger system that new "thing" will show up that need another high order system. So it's correct that no system can contain all truth while keeping consistent. This is the point you want to express in your statement, right? (Actually it's Godel theorem in plain English itself)

What I try to say is: if its not provable in current system so it can not be called true within current system. I could be wrong at this part but not what you tried to explain which I already agree.

[dpierce9]

This isn’t quite right, though perhaps a nit, plenty of formal systems are provably sound (only true things are provable) and complete (all true things are provable). For example, the predicate calculus you learn in Logic 101. Formal systems become provably incomplete when they are able to express arithmetic (e.g., Peano axioms).