In Godel's first incompleteness theorem the Godel sentence G is true otherwise it contradicts itself, however its truth implies it is not provable .

Question

How can this be? I understand there are two basic definitions of truth in mathematics, one being the formalist definition which includes excluded middle and the second form being the intuitionist in which truth is based only on deductive provability. it just seems that informally if a theory is unprovable yet true, being able to explicitly state such a theory would constitute non trivial knowledge of a higher level of provability or computation?

Answer 1

Also if we stay with your awkward simplification, G's Incompleteness Th is no problem for intuitionism.

You are right in saying that for "the intuitionist [...] truth is based only on [...] provability", but this must not be read as "provability into a formal system".

G's proof is perfectly "sound" for an intuitionist : it shows "constructively" how to build up a formula of the formal system which is not provable in the system itself.

Thus, the proof of the existence of formulae unprovable in the formal system is intuitionistically "correct".

Answer 2

You need to be very careful when you talk about truth. Usually it means true in the standard model. There will be nonstandard models where it is false. It is best to think about the incompletness theorems purely in terms of provability.

Answer 3

When we say "true" about statements in the language of arithmetic, we often mean "true in the standard model". In general, "true" is a semantic property and a statement is true in a particular interpretation or it is false there. Without talking about a model, or a structure, the term "true" is utterly meaningless.

In the incompleteness theorem we construct a statement which is true in the standard model of the natural numbers, but does not have to be true in other models. And recall that as a first-order theory, Peano axioms have a myriad of different models.