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

*is indeed not*

**expression***.*

**provable**(3) However the above

*(see graph below).*

*expression is not a sentence***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 ⊢ G**_{F}** ↔ ¬Prov**_{F}**(⌈G**_{F}**⌉)**

**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?**