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.
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.
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.
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.
> 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.
> 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.
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.
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.
[1] https://inference-review.com/article/loebs-theorem-and-curry...
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.
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.
Yeah. I'd say half of the work is Gödel numbering and the other half is the diagonal lemma.
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.
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.
> 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...
> 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.
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.