In Godel's first incompleteness theorem the Godel sentence G is true otherwise it contradicts itself, however its truth implies it is not provable . 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?

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".