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.”

**Formalized as: Sentence _{F}(G) ∧ ~Provable_{F}(G) ∧ ~Refutable_{F}(G)**

**Any expression G of language F is not a sentence of ****language F **

**if this expression G of language F is not ****provable or refutable in F. **

**(see definitions below)**

∀FS ∈ Formal_Systems:

… Provable(FS, X) ↔ ∃Γ ⊆ Rules(FS) (Γ ⊢ X)

… Refutable(FS, X) ↔ ∃Γ ⊆ Rules(FS) (Γ ⊢ ~X)

… True(FS, X) ↔ ∃Γ ⊆ Axioms(FS) (Γ ⊢ X)

… False(FS, X) ↔ ∃Γ ⊆ Axioms(FS) (Γ ⊢ ~X)

… Sentence(FS, X) ↔ ( True(FS, X) ∨ False(FS, X) )

Axioms ⊆ Rules ⊆ WFF ∴

True(FS, X) ⊢ Provable(FS, X)

False(FS, X) ⊢ Refutable(FS, X)

**∴ ( ~Provable(F, G) ∧ ~Refutable(F, G) ) → ~Sentence(F, G)**

**copyright 2017, 2018 Pete Olcott**