What Gödel Discovered (2020)(stopa.io)
stopa.io
What Gödel Discovered (2020)
https://stopa.io/post/269
38 comments
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.
Or is this too reductive?
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?
The easiest way to think about it is like this:
We have these things called systems: a "system" is anything that follows rules: a board game, traffic, the English language, math, C++, etc. Some systems are smart and they can talk about themselves, but others can't. For example, Tic-Tac-Toe can't talk about Tic-Tac-Toe, but English can talk about English.
Gödel is interested in smart systems because dumb systems are boring.
Some systems are useful: they are "useful" if they always say true things. So math is more useful than English. I can lie in English, but I can't lie in math. (Formally, this is what we call consistency).
So here's a problem for you: suppose we have a smart-useful-system, call it SUS. SUS should be able to say "SUS is useful." It can talk about itself and it can't lie, so we should have no problem, right?
Gödel showed that if our system can actually say that about itself, it wasn't useful to begin with. For a few centuries, philosophers and mathematicians were trying to come up with the "one perfect system": useful, smart, and also complete (it can say all true things), and a few more properties. Turns out such a system is impossible.
NB: I use the words "say" or "talk about" in a very hand-wavy fashion, sometimes I mean Prove(), sometimes I mean Entail(). The details are very nuanced, and this isn't meant to be a deep dive.
We have these things called systems: a "system" is anything that follows rules: a board game, traffic, the English language, math, C++, etc. Some systems are smart and they can talk about themselves, but others can't. For example, Tic-Tac-Toe can't talk about Tic-Tac-Toe, but English can talk about English.
Gödel is interested in smart systems because dumb systems are boring.
Some systems are useful: they are "useful" if they always say true things. So math is more useful than English. I can lie in English, but I can't lie in math. (Formally, this is what we call consistency).
So here's a problem for you: suppose we have a smart-useful-system, call it SUS. SUS should be able to say "SUS is useful." It can talk about itself and it can't lie, so we should have no problem, right?
Gödel showed that if our system can actually say that about itself, it wasn't useful to begin with. For a few centuries, philosophers and mathematicians were trying to come up with the "one perfect system": useful, smart, and also complete (it can say all true things), and a few more properties. Turns out such a system is impossible.
NB: I use the words "say" or "talk about" in a very hand-wavy fashion, sometimes I mean Prove(), sometimes I mean Entail(). The details are very nuanced, and this isn't meant to be a deep dive.
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.
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.
You are suggesting Godel created the punctuation mark known as a period? Obviously not. But I'm not sure what you are trying to say..
That period was encoded in a symbol string, i.e. it is a bit string.
Today we encode everything in bi-symbol strings.
This was not common when Gödel crafted his incompleteness theorem. And at the time it was a novel approach for setting up a context for testing the limits of computing.
Some people can still be struck by it as novel when reading the proof, because in context it was, and still feels that way. But today "symbol string" representation is ordinary and pervasive.
Today we encode everything in bi-symbol strings.
This was not common when Gödel crafted his incompleteness theorem. And at the time it was a novel approach for setting up a context for testing the limits of computing.
Some people can still be struck by it as novel when reading the proof, because in context it was, and still feels that way. But today "symbol string" representation is ordinary and pervasive.
Do you recommend reading "Gödel, Escher, Bach: an Eternal Golden Braid"?
Gödel did not invent encoding. Morse was widely used before Gödel.
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.
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.
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.
Yeah, I think it would be better to first explain the liar's paradox to give the broad brush strokes, and then go into the details of Gôdel numbering.
It seems like most expositions of Gödel's incompleteness theorem go into a surprising amount of detail about Gödel numbering. In a way it's nice though, because you see that the proof is actually pretty elementary and doesn't require fancy math as a prerequisite.
It seems like most expositions of Gödel's incompleteness theorem go into a surprising amount of detail about Gödel numbering. In a way it's nice though, because you see that the proof is actually pretty elementary and doesn't require fancy math as a prerequisite.
Godel's 1st Incompleteness Theorem - Proof by Diagonalization
https://www.youtube.com/watch?v=PpSxqde0af4
This is another good exposition.
https://www.youtube.com/watch?v=PpSxqde0af4
This is another good exposition.
Yeah, I think that's the tradeoff.
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.
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.
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.
- 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.
You might say "but wait, haven't we just proven that it's true? So isn't that also a contradiction?" This would be a disaster, because it would prove that the axioms of arithmetic are inconsistent! Now 1+1=3 for all we know.
The catch is that when we proved that the sentence is not false, we used proof by contradiction, and for proof by contradiction to be a valid method of proof, we need to assume that the axioms we are working with are consistent (and therefore can't produce a contradiction). So really all we have proved is that either:
- the sentence is true
Or
- the axioms of arithmetic are inconsistent
We can't prove that the axioms of arithmetic are consistent, so we haven't actually proven that the sentence is true. Contradiction avoided.
This issue is actually a major part of Gödel's theorem; we can only avoid a paradox of the axioms of arithmetic can't prove their own consistency. These theorems apply to any system of axioms that are rich enough to state the liar's paradox.
The catch is that when we proved that the sentence is not false, we used proof by contradiction, and for proof by contradiction to be a valid method of proof, we need to assume that the axioms we are working with are consistent (and therefore can't produce a contradiction). So really all we have proved is that either:
- the sentence is true
Or
- the axioms of arithmetic are inconsistent
We can't prove that the axioms of arithmetic are consistent, so we haven't actually proven that the sentence is true. Contradiction avoided.
This issue is actually a major part of Gödel's theorem; we can only avoid a paradox of the axioms of arithmetic can't prove their own consistency. These theorems apply to any system of axioms that are rich enough to state the liar's paradox.
> We can't prove that the axioms of arithmetic are consistent [...]
Sure we can! [1] ... but it requires (logically) stronger axioms. Assessing the relative strength of axioms along these (Gentzen's) lines goes by the name "ordinal analysis". It's not clear to me that stronger axioms are always less plausible than weaker ones (as axioms).
An alternative is to abandon your insistence on consistency. Another thread points to an article by Graham Priest but not to one of his main research interests: paraconsistency. This line of work aims to route around these issues (paradox in general) by making inconsistencies less explosive. A quick google turned up some relevant discussion [2]. I have it on good authority that the wheels fall off at some point.
[1] https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof
[2] https://math.stackexchange.com/questions/1524715/how-do-inco...
Sure we can! [1] ... but it requires (logically) stronger axioms. Assessing the relative strength of axioms along these (Gentzen's) lines goes by the name "ordinal analysis". It's not clear to me that stronger axioms are always less plausible than weaker ones (as axioms).
An alternative is to abandon your insistence on consistency. Another thread points to an article by Graham Priest but not to one of his main research interests: paraconsistency. This line of work aims to route around these issues (paradox in general) by making inconsistencies less explosive. A quick google turned up some relevant discussion [2]. I have it on good authority that the wheels fall off at some point.
[1] https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof
[2] https://math.stackexchange.com/questions/1524715/how-do-inco...
> We can't prove that the axioms of arithmetic are consistent
using the axioms themselves. We can prove consistency using a stronger set of axioms, but those axioms have their own liar sentence, and so they can't prove their own consistency. And without knowing if the stronger set of axioms is consistent, we can't be sure that we have really proved the consistency of arithmetic.
using the axioms themselves. We can prove consistency using a stronger set of axioms, but those axioms have their own liar sentence, and so they can't prove their own consistency. And without knowing if the stronger set of axioms is consistent, we can't be sure that we have really proved the consistency of arithmetic.
> These theorems apply to any system of axioms that are rich enough to state the liar's paradox.
Isn't that circular reasoning or tautological though? Rephrased: any system that can state something that these theorems apply to, can have the theorems applied to.
I think the word "rich" is too inaccurate in this context. It is not clear why there can't be a more "rich" system which does not suffer from this issue and can't state the liars paradox.
Isn't that circular reasoning or tautological though? Rephrased: any system that can state something that these theorems apply to, can have the theorems applied to.
I think the word "rich" is too inaccurate in this context. It is not clear why there can't be a more "rich" system which does not suffer from this issue and can't state the liars paradox.
Yeah rich is a vague word here. Really we're trying to say 'if a set of axioms can express provability, and can get a sentence to refer to itself, then it can state the liar sentence. And once it can state the liar sentence, then the rest of Gödel's argument follows.' There's no circularity.
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.
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.
I’m confused by this jump to the natural world:
> 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.
> 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.
>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?
It explains this directly before that phrase:
"Their language was dense and the work laborious, but they kept on proving a whole bunch of different truths in mathematics, and so far as anyone could tell at the time, there were no contradictions. It was imagined that at least in theory you could take this foundation and eventually expand it past mathematics: could you encode in pure logic how a dog behaves, or how humans think?"
>Math have been used to model natural phenomena a long time before Principia.
Which means little in this context. The question posed wasn't if you can use some math to describe some natural phenomenon.
The question posed was whether one could model the whole thing (e.g. how a dog behaves) in a formal language - not just take some isolated equations and apply it to this or that aspect of phenomenon (especially if it's a mere approximation). That they already knew, e.g. the equations for planetary motion.
It explains this directly before that phrase:
"Their language was dense and the work laborious, but they kept on proving a whole bunch of different truths in mathematics, and so far as anyone could tell at the time, there were no contradictions. It was imagined that at least in theory you could take this foundation and eventually expand it past mathematics: could you encode in pure logic how a dog behaves, or how humans think?"
>Math have been used to model natural phenomena a long time before Principia.
Which means little in this context. The question posed wasn't if you can use some math to describe some natural phenomenon.
The question posed was whether one could model the whole thing (e.g. how a dog behaves) in a formal language - not just take some isolated equations and apply it to this or that aspect of phenomenon (especially if it's a mere approximation). That they already knew, e.g. the equations for planetary motion.
So would it be just as correct to use an electrical circuit as example, i.e. before Principia it was not believed possible to model an electrical circuit in a formal language?
> I would assume this could be described in a formal language
The assumption is the first problem, no? If the formal language is complete, it must be inconsistent. If it is consistent, it must be incomplete. If the language is incomplete or inconsistent, you may be unable to encode dog behavior in it.
The assumption is the first problem, no? If the formal language is complete, it must be inconsistent. If it is consistent, it must be incomplete. If the language is incomplete or inconsistent, you may be unable to encode dog behavior in it.
The article use “describing the behavior of a dog” as something people began to think was possible because of Principia. This is what I don’t get. Was this thought impossible before Principia? On what grounds?
What about describing an electrical circuit formally? Surely this was thought possible before Principia was published.
What about describing an electrical circuit formally? Surely this was thought possible before Principia was published.
The assumption made by many in the early 20th century, spurred on by the recent successes of unification and formalization, was essentially that we could formally describe the entire universe. Godel’s proof shows that if you attempt to formally describe something there’s either an inconsistency or it’s incomplete. That doesn’t mean you cannot describe the behavior of a dog formally but it does mean the same formula which encodes the behavior will either be inconsistent or incomplete. It might only be inconsistent or incomplete when applied outside of defining the behavior of a dog though. That’s why the little preamble about unification exists in this post but it’s not very well tied into the rest of the post.
> Godel’s proof shows that if you attempt to formally describe something there’s either an inconsistency or it’s incomplete.
The “something” Gödels proof talks about is axiomatic systems. It doesn’t talk about physical objects.
The “something” Gödels proof talks about is axiomatic systems. It doesn’t talk about physical objects.
>This is what I don’t get. Was this thought impossible before Principia? On what grounds?
Even the full formalization of mathematics wasn't considered certain (*) before Hilbert/Principia and those 20th century attempts. Much less the formalization being applied everything in the physical world or even animal behavior.
* in retrospect rightly so, because it wasn't, at least not without inconsistency/incompleteness.
Even the full formalization of mathematics wasn't considered certain (*) before Hilbert/Principia and those 20th century attempts. Much less the formalization being applied everything in the physical world or even animal behavior.
* in retrospect rightly so, because it wasn't, at least not without inconsistency/incompleteness.
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.
Saying his name like “girdle”, is the closest English pronunciation I’ve seen.
The actual German ö is hard for me to figure out without having a native speaker around to practice with.
The actual German ö is hard for me to figure out without having a native speaker around to practice with.
The “l” is just as hard to pronounce correctly. English has a very nasal “l” compared to german.
Try saying English “hell” but dragging out the “l” (“helllllllll”); very nasal. Compare audio here: https://en.wiktionary.org/wiki/hell#German
Try saying English “hell” but dragging out the “l” (“helllllllll”); very nasal. Compare audio here: https://en.wiktionary.org/wiki/hell#German
I try to explain it as trying to shape your mouth as if you were saying e but say o instead.
I'd say it's like the 'u' in 'hurt'.
[1] https://inference-review.com/article/loebs-theorem-and-curry...