# 1931 Incompleteness Theorem is only undecidable because it is not a sentence expressing Boolean

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.

https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
In mathematical logic, a sentence of a predicate logic is a boolean-valued well-formed formula with no free variables. A sentence can be viewed as expressing a proposition, something that must be true or false.

G @ ∃X ~Provable(X, G) // Minimal Type Theory
(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).

Expression 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

Cycles in directed graphs of logical expressions are erroneous:
https://en.wikipedia.org/wiki/Occurs_check
A naive omission of the occurs check leads to the creation of cyclic structures and may cause unification to loop forever.

Programming in Prolog (2003) by Clocksin and Mellish page 254
equal(X, X).
?- equal(foo(Y), Y).
match a term against an uninstantiated subterm of itself. In this example, foo(Y) is matched against Y, which appears within it. As a result, Y will stand for foo(Y), which is foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))), and so on. So Y ends up standing for some kind of infinite structure.

https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
(G) F ⊢ GF ↔ ¬ProvF(⌈GF⌉)

Match a term against an uninstantiated subterm of itself:
Equivalent( GF, ¬ProvF( Godel_Number(GF) )
Equivalent( GF, ¬ProvF(GF) )
Equivalent( ¬ProvF(GF), GF )

Equivalent( ProvF(GF), GF )
?- equal(foo(Y), Y).
Can you see how the above two are the same?