So far everyone in the whole world is not up to the challenge of removing the extraneous complexity from the 1931 Incompleteness Theorem.

This complexity comes from the fact that the GIT must construct the equivalent of a HOL provability predicate within the language of arithmetic.

Doing this apparently requires 46 definitions, Gödel numbers and the Diagonal lemma. If we were dealing with HOL that has its own provability predicate none of this extraneous complexity would be required.

**Stanford Encyclopedia of Philosophy Gödel’s Incompleteness Theorems **

**2.5 The First Incompleteness Theorem—Proof Completed**

**(G) F ⊢ G**_{F}** ↔ ¬Prov**_{F}**(⌈G**_{F}**⌉).
**

**My adaptation:**

**G ↔ ~∃Γ ⊆ WFF(F) Provable(Γ, G)**** // No Gödel numbers required
**