[wsxcde]

Godel's incompleteness is not that complicated. The main insight Godel had was that proofs as well as provable statements can be encoded in numbers. This is obvious to everyone reading HN -- all computing works by encoding things into numbers. And it's easy to see how you'd encode proofs, proof rules etc. into numbers. (hint: as flattened ASTs!)

The thing is, Godel didn't live in an era of pervasive computing so he came up with a wonky encoding based on products of powers of primes. This makes the proof technically challenging, but the fundamental idea is not that complex. What he was able to eventually do was encode a recursive statement of the form "this statement is not provable" where the "this" is kind of like a pointer back to the full statement. The rest is straightforward.

[gnulinux]

This is true, obviously, but I can reassure you that the actual proof is very technical and long. Back in college I took a logic class that spent almost the entire semester going over this proof, in its shortened form i.e. using Rosser's trick. By using Rosser's trick one can prove a more general Incompleteness theorem (based on Q) and more elegantly. It ends up stating very concisely that a theory cannot be all 3 of (any 2 or 1 or 0 is fine):

* axiomatizable extension of Q

* consistent

* complete

(where Q is a minimalistic arithmetical theory that can do addition and multiplication: https://en.wikipedia.org/wiki/Robinson_arithmetic)

It's true that the "main idea" of the proof is "everything is a natural number", which is obvious to us programmers (it possibly wasn't obvious to anyone in Godel's time). However, this is by no means the only trick that's used in the proof.

[stepbeek]

> This is true, obviously,

Is this a dig at Hilbert?

[ProfHewitt]

[Gödel 1931] tried to formally prove the proposition that there are true but unprovable propositions, which had been previously intuited by others.

Unfortunately, the [Gödel 1931] proof fails for the claimed Russell's system for the foundations of mathematics.

The following has an explanation of what went wrong in this and many other cases in foundations of mathematics for computer science:

    Vanquishing ‘Monsters’ in Foundations of Computer Science: Euclid, Dedekind, Russell, Gödel, Wittgenstein, Church, and Turing didn't get them all ...

https://papers.ssrn.com/abstract=3603021

[sukilot]

Computers use a much more complicated encoding, if you specify them in as much detail as Gödel did.