The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F.
When Godel said that he found a sentence G of language F such that:
~(ProvableF(G) ∨ RefutableF(G) ) he was wrong.
(G) F ⊢ GF ↔ ¬ProvF(⌈GF⌉)
1931 GIT entirely summed up as a single line of Minimal Type Theory:
G @ ∃X ~Provable(X, G)
(1) The above expression says that it is not provable.
(2) The above expression is indeed not provable.
(3) However the above expression is not a sentence (see graph below).
Sentence translated into a Directed Acyclic Graph by the MTT compiler:
 G (02)(04)
 THERE_EXISTS (03)
 NOT (05)
 Provable (03)(01) // cycle indicate infinite evaluation loop