1931 Incompleteness Theorem Refutation Strategy

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: SentenceF(G) ∧ ~ProvableF(G) ∧ ~RefutableF(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