Godel's Incompleteness Theorem

Create a meta function $𝐠$ that bijects between natural numbers and formulas of a formal system $F$ that has first order logic and Peano arithmetic. Also create a meta function $𝐤$ that turns the meta natural numbers into the symbols for the formal systems Peano arithmetic numerals.

Diagonal Lemma

Make substitution function that applies to the Godel numeral of a function with a single free variable with a Peano arithmetic numeral.

Then define diagonalization function.

and a formula.

and Diag is a function satisfying

let

then let

Then prove that

and substituting

then

First incompleteness theorem

Use diagonal lemma to make

So if $G$ is provable it is true but that means it's not provable. If $\neg G$ is provable then it means that $G$ is provable so the formal system isn't consistent