# Refuting the conclusion of Gödel’s 1931 Incompleteness Theorem

Syntactic Consequence (Provability)
A formula A is a syntactic consequence within some formal system 𝓕𝓢
of a set Γ of formulas if there is a formal proof in 𝓕𝓢 of A from the set Γ.
Γ ⊢𝓕𝓢 A   ≡   ∃Γ ⊆ FS Provable(Γ, A)

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.

https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
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:       SentenceF(G) ∧ ~ProvableF(G) ∧ ~RefutableF(G)

G @ ~∃Γ ⊆ F Provable(Γ, 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).

Sentence translated into a Directed Acyclic Graph by the MTT compiler:
[01] G                                (02)(07)
[02] NOT                          (03)
[03] THERE_EXISTS (04)
[04] SUBSET_OF         (05)(06)
[05] Γ
[06] F
[07] Provable                 (05)(01) // cycle indicates infinite evaluation loop