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

**from the set**

*A***Γ**.

**Γ ⊢**≡

_{𝓕𝓢}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:** **Sentence _{F}(G) ∧ ~Provable_{F}(G) ∧ ~Refutable_{F}(G)**

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

*is not a*

**expression***(see graph below).*

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