This blog post gets way too caught up in Gödel numbers, which are merely a technical detail (specifically how the encoding is done is irrelevant). A clever detail, but a detail nonetheless. Author gets lost in the sauce and kind of misses the forest for the trees. In class, we used Löb's Theorem[1] to prove Gödel, which is much more grokkable (and arguably even more clever). If you truly get Löb, it'll kind of blow your mind.
Other names for Gödel encoding: Digital. Binary. Zorros and Unos.
Today Gödel encoding is so pervasive, it’s easy to miss that everything is trivially Gödel encladed. Because like most everything invisible, it’s right in front of us.
We Gödel our memes and gift cards, and (pick your poison) pr0ns. Colors and AI’s, lax ASMR’s and our (sneaky don’t read me) terms of service. Even this very small humble .
Gödel isn’t eating the world. Gödel already pööped it.
Morse didn't conceptually extend encoding to self-referential symbolic systems. Morse's insight was pure communication of symbols devoid of meaning.
Important but nowhere near the same.
Today, general symbolic encoding is viewed as trivial. Every symbol we have is pervasively encoded as bits, so of course entire expressions are. So Morse's code might seem comparable.
But what Gödel invented went well beyond Morse. We are just jaded with regard to his insight now.
Of course you can encode self-references in morse code, how could morse prevent that? Just use the same lisp syntax as in the article and then encode using morse code instead of Gödel numbering.
The purpose of Gödel numbering is to represent an arbitrary-length string of symbols as a single integer which allows you to manipulate it using Peano arithmetic.
But it is not like Gödel invented binary as you seem to suggest. Baudot code (a 5-bit character encoding) was in use in 1870’s.
In any case, Gödel-numbering is the least interesting part of the the theorem. The groundbreaking idea is creating statements about theorems.
As a non-mathematician I always wondered about one thing. Because the way I interpret the Incompleteness Theory is that "you cannot have a universal system of infinite expressiveness, because you will need a more expressive one to prove it".
In other words, you can't have a top-down universal system. But you very well can have well described ones perfectly describe observable behaviour without defects.
The proof will be more friendly to nowadays programmers if we treat all "Gödel numbers" as bytecode of a programming language.
It's trivial that functions like "prove" and "subst" can be implemented based on abilities like bytecode parsing and expression tree manipulation.
I feel like it's nice to get the gist before diving into the gory details. The proof works by showing that just within the axioms of arithmetic, you can formally state the sentence "this sentence is unprovable." This has some very strange consequences:
- It can't be false, because if it's false then it is provable, and 'provable' means ' can be proven to be true.' That would be a contraction.
- So therefore it must be true, implying that it can't be proven. Consequently there are statements that are true but unprovable, even just within the axioms of arithmetic.
This is Gödel's incompleteness theorem in a nutshell. Most of the proof is spent developing machinery for doing logic, talking about provability, and ultimately getting a statement to refer to itself all using integers and their properties. It's quite satisfying because it doesn't require any super-advanced math, and yet the result is very deep.
> could you encode in pure logic how a dog behaves
Assuming we knew enough about how a dog behaves (or less ambitiously, a more primitive organism) I would assume this could be described in a formal language. But why would Principia be needed for this? Math have been used to model natural phenomena a long time before Principia.
What Gödel showed is that (in any sufficiently powerful formal axiomatic system) the set of provable statements isn’t the same as the set of true statements. This means that either there are true statements that aren’t provable (incompleteness), or that there are provable statements that aren’t true (inconsistency), or both.
One way to see this is via the halting problem. For any program (with a fixed input), there is a truth of the matter of whether it will eventually halt or not. In the formal system, for every (Turing-machine) program P we can define a function s_P(n) that gives us the state of the program after n steps (by recursive definition). Then we can write for any program P the statement H(P) = “there exists a natural number n such that s_P(n) is a halting state”. Furthermore, we can write a program R that, given any program P as input, enumerates all proofs of the formal system (this is possible because proofs are strings, and we can write a program that enumerates all strings) and that for each proof checks if it is a proof of H(P) or of not H(P), and if it finds such a proof, stops and outputs the result (P halts or doesn’t halt). If such a proof exists, then R will eventually find it. And if R would find a proof for any P, then this would solve the halting problem.
But we know that the halting problem is undecidable, which means that there must be programs P for which there is neither a proof of H(P) nor of not H(P). This shows that there are truths (the program will halt or won’t halt) for which there is no proof in the formal system; or alternatively, that the formal system is inconsistent and proves falsities.
14 comments
[ 4.6 ms ] story [ 44.4 ms ] thread[1] https://inference-review.com/article/loebs-theorem-and-curry...
Löb gets you to the main idea faster, but Gödel numbering is the part that makes it feel like the system is actually doing it itself.
Without that step, it can start to feel a bit too close to the liar paradox.
Today Gödel encoding is so pervasive, it’s easy to miss that everything is trivially Gödel encladed. Because like most everything invisible, it’s right in front of us.
We Gödel our memes and gift cards, and (pick your poison) pr0ns. Colors and AI’s, lax ASMR’s and our (sneaky don’t read me) terms of service. Even this very small humble .
Gödel isn’t eating the world. Gödel already pööped it.
Important but nowhere near the same.
Today, general symbolic encoding is viewed as trivial. Every symbol we have is pervasively encoded as bits, so of course entire expressions are. So Morse's code might seem comparable.
But what Gödel invented went well beyond Morse. We are just jaded with regard to his insight now.
The purpose of Gödel numbering is to represent an arbitrary-length string of symbols as a single integer which allows you to manipulate it using Peano arithmetic.
But it is not like Gödel invented binary as you seem to suggest. Baudot code (a 5-bit character encoding) was in use in 1870’s.
In any case, Gödel-numbering is the least interesting part of the the theorem. The groundbreaking idea is creating statements about theorems.
In other words, you can't have a top-down universal system. But you very well can have well described ones perfectly describe observable behaviour without defects.
Or is this too reductive?
https://www.youtube.com/watch?v=PpSxqde0af4
This is another good exposition.
- It can't be false, because if it's false then it is provable, and 'provable' means ' can be proven to be true.' That would be a contraction.
- So therefore it must be true, implying that it can't be proven. Consequently there are statements that are true but unprovable, even just within the axioms of arithmetic.
This is Gödel's incompleteness theorem in a nutshell. Most of the proof is spent developing machinery for doing logic, talking about provability, and ultimately getting a statement to refer to itself all using integers and their properties. It's quite satisfying because it doesn't require any super-advanced math, and yet the result is very deep.
> could you encode in pure logic how a dog behaves
Assuming we knew enough about how a dog behaves (or less ambitiously, a more primitive organism) I would assume this could be described in a formal language. But why would Principia be needed for this? Math have been used to model natural phenomena a long time before Principia.
The actual German ö is hard for me to figure out without having a native speaker around to practice with.
One way to see this is via the halting problem. For any program (with a fixed input), there is a truth of the matter of whether it will eventually halt or not. In the formal system, for every (Turing-machine) program P we can define a function s_P(n) that gives us the state of the program after n steps (by recursive definition). Then we can write for any program P the statement H(P) = “there exists a natural number n such that s_P(n) is a halting state”. Furthermore, we can write a program R that, given any program P as input, enumerates all proofs of the formal system (this is possible because proofs are strings, and we can write a program that enumerates all strings) and that for each proof checks if it is a proof of H(P) or of not H(P), and if it finds such a proof, stops and outputs the result (P halts or doesn’t halt). If such a proof exists, then R will eventually find it. And if R would find a proof for any P, then this would solve the halting problem.
But we know that the halting problem is undecidable, which means that there must be programs P for which there is neither a proof of H(P) nor of not H(P). This shows that there are truths (the program will halt or won’t halt) for which there is no proof in the formal system; or alternatively, that the formal system is inconsistent and proves falsities.