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)
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.
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:
 G (02)(07)
 NOT (03)
 THERE_EXISTS (04)
 SUBSET_OF (05)(06)
 Provable (05)(01) // cycle indicates infinite evaluation loop