Gödel’s 1931 Incompleteness Theorem summed as a single line of Minimal Type Theory

https://plato.stanford.edu/entries/goedel-incompleteness/
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.

https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
(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:
[01] G                                (02)(04)
[02] THERE_EXISTS (03)
[03] X
[04] NOT                         (05)
[05] Provable                (03)(01)   // cycle indicate infinite evaluation loop

G_Not_Provable.png