What Made Gödel’s Incompleteness Theorem Hard to Prove
algorithmsoup.wordpress.com
algorithmsoup.wordpress.com
> Here’s another example (known as the Berry paradox):
> Define {x} to be the smallest positive integer that cannot be defined in under {100} words.
> This might look like a valid mathematical definition. But again it’s nonsensical. And, importantly for the sanity of mathematics, no analogous statement can be made mathematically formal.
I thought it was worth mentioning that the Berry Paradox does show up in a mathematically formal way, and it was fascinating to me. It can be used to prove that a general algorithm to compute the Kolmogorov complexity of a string is uncomputable.
https://en.wikipedia.org/wiki/Berry_paradox#Formal_analogues
The second incompleteness theorem gives an example of something undecidable that's probably more interesting that the uselessly paradoxical statement in the first: it says that no system can consistently prove its own consistency.
But the grander point, that Hofstadter pushes a lot in GEB, is that any sufficiently powerful symbolic system will be able to self-reference. For example, consider a programming language that is not Turing complete. You will basically need to disallow loops, because with those you can implement a virtual machine to break all your self-reference-banning rules.
Lock yourself away in a room with nothing but pen and paper (no internet, not books) and try to reproduce Goedel's original proof. Then post the attempt here :)
When I tried this a few years ago I made a mistake in the definition of numbering, got through half the proof, ran into trouble, and gave up before I figured out exactly where the mistake was. And I had already committed the overall outline and the tactical steps for each part to memory...
Even if you remember the entire outline, it'll be really hard to get the details right....
And, more importantly, the outline itself is actually not obvious.
>... much easier for us than for mathematicians of Godel's time because we are familiar with programs and computers
Again, it seems unlikely that this was the sticking point.
E.g. Hilbert understood mathematics as a symbolic game, thought about this exactly question, and didn't come up with Goedel's proof. And Hilbert was definitely no dullard.
> E.g. Hilbert understood mathematics as a symbolic game
Hilbert had a radically different understanding of the nature of mathematics compared to Godel. Moreover, Hilbert was radical enough that he tried to use his fame to silence people with differing views than him (e.g. Brouwer). Hilbert hardly believed Godel when he published his results, because it was easy to see that it would shake the foundations of "Hilbert's Program" something Hilbert spent half his life on (and logicians still publish papers about the relationship between Godel's Incompleteness theorems and Hilbert's Program). This makes Hilbert orders of magnitude less motivated to think about this issue, probably. On the other hand, Godel had various non-mathematical reasons to prove incompleteness, one being his desire to block materialism; check for Godel's Gibbs Lectures.
Second, I took a philosophy of mathematics course when I was an undergrad studying computer science. And I have a copy of Godel (1951) (I think it's transcripted from his Gibbs Lecture) given to me as a class material. I tried search engines and couldn't find it anywhere, for the love of god. It's such a shame because it's a very important text imho. Since it's probably copyrighted or something, I don't know where to put it. If you're interested PM me and I can send you a pdf. Its title is "Some basic theorems on the foundation of mathematics and their implications". It's mostly about Godel explaining philosophical implications of his theorems and why he thinks they're important. If someone can find pdf, it'd be very helpful.
I couldn't find your contact information. It might be good to add it to your profile for other people.
http://libgen.io/search.php?req=godel+collected+works+3&open...
Right, this was pretty much my original point.
> This seems to indicate me that GP comment is right that the inciting incident was understanding the correspondence between mathematics and its encoding.
Doesn't this sentence contradict the previously quoted one? Or, at the very least, the point is far more subtle than the GP's "...it's the conceptual leap to thinking about mathematical statements as mathematical objects..."
I don't see anything in Hilbert's mathematics that indicates he did not "think about mathematical statements as mathematical objects". Very much the opposite, actually.
I'll agree that the key insight was basically about mathematics and its encoding. And that this insight was extremely non-obvious.
But Hilbert's program really was literally all about GP's "[thinking of] mathematical statements as mathematical objects".
Or, to restate this contentious agreement we're having another away: things like the idea to do numbering in the first place are the details, and do not obviously follow from treating mathematical objects as objects of mathematics itself.
1. Assume every either T or ~T is provable for all theorems T, and that our logic is consistent. (The opposite of the incompleteness theorem.)
2. For every Turing machine, there is a proof that it halts or a proof that it doesn't halt.
3. A machine that enumerates and validates proofs will find one of those proofs, so the Halting Problem is decidable -- a contradiction.
Easy peasy. (The proof of the Halting Problem undecidability from the Incompleteness Theorem is similarly straightforward.)
Godel did his work first though, so he didn't have that machinery (hmm) available.
Well, sure, because proving the Halting Problem is undecidable is about as hard as proving Godel's Theorem without having the undecidability of the Halting Problem to start from.
If the input halts, then loop
If the input loops, then halt
You then pass the program itself as input to itself and you get a contradiction.
Assume you have a program HALT(n) that will return 1 if the Turing machine described by string n halts when fed itself as input and returns 0 otherwise. Construct the program BOOM(n) that runs forever if HALT(n) returns 1 and returns 0 if HALT(n) returns 1. Now consider HALT(BOOM). If HALT(BOOM) is 1, then BOOM(BOOM) halts by definition of HALT, but BOOM runs forever in that case. If it returned 0, then it runs forever, but BOOM(BOOM) in fact halted. Something must give, and the only thing that has room to give is that HALT itself can be constructed (since the encoding of Turing machines to numbers is well-defined, and the construction of BOOM is well-defined and possible iff HALT is well-defined and possible).
I assume you mean "returns 0 if HALT(n) returns 0"?
Also let me add a remark on a certain subtlety: Step 3 only works if we assume that, if a claim about the halting behaviour of Turing machines has a proof in the studied formal system, then it's actually true.
This assumption is believed to be warranted for the standard formal systems of mathematics such as Peano Arithmetic (PA) or Zermelo–Fraenkel set theory (ZF), but Gödel's proof also applies to formal systems for which this assumption doesn't hold, or for which the assumption does hold but cannot be proven in a weak metatheory.
These systems are typically not very useful as vehicles to carry out formalized mathematics, but they are nevertheless very interesting and fundamental to the study of logic. An example for such an anti-real formal system is PA adjoined by an axiom expressing that PA is inconsistent.
Ludwig Wittgenstein. 1956. Remarks on the Foundations of Mathematics, Revised Edition Basil Blackwell. 1978.
There is a discussion here:
It’s more work to formalize all the details here than in Gödel’s proof, because now you have to explain how the formal system can reason about Turing machines reasoning about Turing machines rather than just how the formal system can reason about itself, but it works just as well.
Thank you for this. Else I'd have perpetuated that myth further!
Infinite-time Turing machines can readily solve the halting problem for ordinary Turing machines, but (by the same proof) not for themselves.
The theory of infinite-time Turing machines is in some regards parallel to the theory of ordinary Turing machines and in others quite different.
I particularly enjoy the Lost Melody Theorem: There is a specific infinitely long 0/1 sequence for which
(a) it's possible to devise an infinite-time Turing machine which will correctly detect whether that 0/1 sequence is written on the input tape, but
(b) there is no infinite-time Turing machine which will, starting on an empty tape, write out that 0/1 sequence to the output tape.
It's like when you would recognize a song but cannot sing it. Some details are here: https://rawgit.com/iblech/mathezirkel-kurs/master/superturin...
We can all agree that would be hard, but your claim that the details are the central thing that makes GP hard is much, much stronger than that.
The relevant question would be: How many people alive right now could succeed at your challenge? My guess would be thousands, maybe tens of thousands.
And compare that to:
The number of people alive who, without any knowledge of GP, could come up with the key insight you describe in your 1 paragraph summary of the proof, and the insight of using godel numbers to label mathematical statements to make that argument rigorous.
The answer to that is "somewhere around 0."
I get that you're impressed by the proof's details -- they're impressive -- but it seems like an odd take to rate those as more difficult than the incredible creative leaps that produced the high-level ideas behind the proof.
Look at the proof - page after page of work showing how to encode and decode formal propositions using primitive recursive functions.
>E.g. Hilbert understood mathematics as a symbolic game, thought about this exactly question, and didn't come up with Goedel's proof. And Hilbert was definitely no dullard.
Goedel's theorem is exactly that mathematics is not a symbolic game - that Hilbert's program is not possible. The proof relies on reducing logical deduction to arithmetic.
Look at the game. Move after move of rooks moving in columns and rows and of bishops moving on the diagonals. :)
> Goedel's theorem is exactly that mathematics is not a symbolic game - that Hilbert's program is not possible. The proof relies on reducing logical deduction to arithmetic.
The point was that thinking of mathematics as a game in the first place requires "...the conceptual leap to thinking about mathematical statements as mathematical objects..."
Goedel's proof didn't come out of nowhere, and he was NOT the one to first propose thinking of mathematical statements as mathematical objects. In many ways, Goedel's proof was actually a response to/rejection of "mathematical statements as mathematical objects"
Goedel's big leap was... the proof itself. Was it the numberings? Well, I guess, but really it was what he did with the numberings. And then how he related that to arithmetic. It's hard to pick out a single piece of the derivation and say "ah ha! That's the key insight!". So I think "the point is in the details" is pretty accurate.
Scott Aaranson "popularizes" Kleene's textbook proof of Godel's theorems using Turing machines in his blog:
The role of Peano arithmetic is somewhat analogous to the role of the particular definition of a Turing machine in the proof of the halting problem: you can easily swap it out with something commensurate and get the same result.
(Stop pretending to explain things to me that I already know.)
Also when talking about a formal theory distinguishing the definition (i.e. the axioms) and the theorems is pretty important.
EDIT: I realize now that a specific example would be helpful. Goedel's theorem can be applied to primitive recursive arithmetic[1], which is neither weaker nor stronger than Peano arithmetic. Interestingly enough PRA with a small addition (of broader transfinite induction) can actually prove Peano arithmetic[2].
[1]: https://en.wikipedia.org/wiki/Primitive_recursive_arithmetic
[2]: https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof
>represent addition and multiplication
It's the simplest possible explanation. Stop being a pretentious jerk. Yes, I know about primitive recursive arithmetic. I first learned about it about ten years ago.
EDIT: Wait a second. Look, I said this:
>depends heavily on the properties of Peano arithmetic, as defined by addition and multiplication
I said it right there. How could you not know this? When I said "the properties of Peano arithmetic", I meant the presence of addition and multiplication.
Let me explain it another way: Goedel's theorem is a theorem about math. Math as it was understood in the 18th century. That's what makes it interesting. The halting problem is proven with an abstract machine that was invented, mostly, to use as a basis to form analogies with other machines. So it's general by construction. (If the integers were not already interesting, Goedel's theorem would be like proving a variant of the halting problem for some weird computational structure that has no relevance to anything and is absurdly cumbersome to prove equivalent to other systems. But for the integers, the analogy is why it's interesting. Nobody expected the Goedel numbering.)
Yes, Goedel's theorem applies to all interesting versions of the integers, but it does not apply to all interesting mathematical systems. IIRC people usually cite the theory of "real closed fields" or something like that.
> I said it right there. How could you not know this? When I said "the properties of Peano arithmetic", I meant the presence of addition and multiplication.
That's a curious definition of "heavily dependent" on the properties of Peano arithmetic (when the condition is in fact "any integer arithmetic with addition and multiplication"), and I'd argue it would be hazardously confusing to the uninitiated, but that's just semantics. Back to the original point (that the analogy is poor) I don't see how that breaks the analogy at all. Just like there are weaker arithmetics that escape Goedel's theorems (I will not mention their names since that seems to just cause issues), there are weaker models of computation that dodge the halting problem (again I'm sure you know of them, the one I'm thinking of off the top of my head rhymes with schmimative shmecursive shmunctions).
> Let me explain it another way: Goedel's theorem is a theorem about math. Math as it was understood in the 18th century. That's what makes it interesting.
I think what makes it interesting has nothing to do with the particulars of what people thought math was in the 18th century. I doubt there are any mathematicians from ancient Greece to a thousand years from now that would seriously consider using a logical system incapable of modeling addition and multiplication as a ground-level theory for the majority of mathematics. They probably would be fine with one that only killed off Peano arithmetic, just like we'd be fine with a form of computation that wasn't as limiting as PRFs but didn't happen to be susceptible to Turing's reasoning. It seems just as general by construction, and I doubt it is an accident that Goedel using something so basic.
Basically what I'm saying is just like the fact that the Church-Turing thesis has held up and all interesting forms of computation and equivalent to Turing machines, there is an implicit Addition-And-Multiplication-Are-Basic thesis that claims that systems unable to model addition and multiplication in some form are fun to visit but not to live in when you're doing mathematics.
(Stop pretending people can read your mind.)
There's also a version of Russell's paradox lurking in the standard proof of Cantor's theorem (https://en.wikipedia.org/wiki/Cantor%27s_theorem).
(GEB has other philosophical discourses that are interesting, if only as an example of how people can very reasonably mispredict the future. In Hofstader’s case, he posited that chess would only be played at a human level by an AGI.)
I read Godel's Proof after though, and I agree that it is a far clearer introduction to Godel's theorems.
Also, the book is about 98% Gödel and 2% Escher and Bach. Any time it steps outside its wheelhouse of math and into the realm of philosophy or art, you get the distinct sense that it has no idea what it's talking about.
Do yourself a favor and just take discrete math 1 and read a few Wikipedia articles instead.
+100, exactly. I have some familiarity with mathematical logic, and with Bach (though admittedly I'm less familiar with Escher) and I found GEB to be unintuitive at best, and misleading at worst.
To be honest, there may not be anything really magic about Goedel's incompleteness theorem once you grasp the core concept, which is: If you encode all proofs into a formal language, you can make a statement that is true but unprovable. (Which is, effectively: "This statement has no proof"). Most of Goedel's work on the incompleteness theorem was on the systematization of proofs, which can be tedious to work through.
I found at the time Godel's completeness theorem to be more interesting. Though I never got into model theory or more advanced mathematical logic so, grain of salt.
Godel's proof of inferential undecidability [incompleteness] was too superficial. It didn't get at the real heart of what was going on. It was more tantalizing than anything else. It was not a good reason for something so devastating and fundamental. It was too clever by half. It was too superficial. [It was based on the clever construction] I'm unprovable. So what? This doesn't give any insight how serious the problem is.
And GEB's explanation of it is more complete/exact than the one in the article.
It is also amazingly mind-twisting. Not the explanation per se, but the theorem.
And I think its consequences are under appreciated: no (sufficiently complex) logical system is free from self-contradictions.
Incompleteness: there exist true statements that lack proofs
Unsoundness: there exist false statements with proofs
If I understand all this correctly, what Goedel demonstrated was that a sufficiently complex logical system could self-reference, and from self-reference unprovable (not contradictory) true statements fall out.
By reductio ad absurdum any self-contradictory logical system is useless as a logic because everything is provable in it, so one wonders if such systems should even be considered "logical systems".
You don't RAA it because you can't prove the system is consistent (because you can't prove the counterexample)
I believe your position is that "sufficiently complex" == "able to formulate and prove its own consistency"; my position is that such a system would be worthless as a logic, because in such a system you can prove anything.
Your second paragraph is inscrutable to me. Are you trying to claim that you can't prove everything with a known inconsistent logic? Are you referring to paraconsistent logics?
[1] http://mathworld.wolfram.com/GoedelsSecondIncompletenessTheo...
Meaning, not "trivially simple". The description in your link is good enough, the description in the Wikipedia is more detailed
> any formal system that is interesting enough to formulate its own consistency can prove its own consistency iff it is inconsistent.
That's what "sufficiently complex" means and why you can't Reduction Ad Absurdum it.
That doesn't seem right? Any logical system that has a self-contradiction (which I take to mean can prove a statement and its inverse) will be able to prove everything, which is obviously a pretty big flaw.
What Godel's 2nd incompleteness theorem says is that if a system can prove its own consistency, then it follows that it is unsound.
In this theory, proof checking is computationally decidable even though the theorems are not computationally enumerable by a total procedure.
No it doesn't - that would contradict Goedel's well-established theorem. The formal consistency of Peano arithmetic has been proven, but not by Peano arithmetic:
> Gentzen's theory obtained by adding quantifier-free transfinite induction to primitive recursive arithmetic proves the consistency of first-order Peano arithmetic (PA) but does not contain PA [...] Gentzen's theory is not contained in PA, either, however, since it can prove a number-theoretical fact—the consistency of PA—that PA cannot. [1]
[1] https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof#...
Also, Godel's proposition "I'mUnprovable" does not exist in the higher order theory because it doesn't type check.
I also don't understand how proof checking can be decidable if the axioms are not recursively enumerable. If proof checking is decidable, there must be a way of determining if a use of an axiom refers to a valid axiom. But if you can do that, as long as you can put the syntactic formulas of the system in bijection with the natural numbers (which I presume is the case if this is aimed at computing, and would hope in general that you can write them on paper using a finite string of symbols) you can produce an enumerating program by just running the decision procedure on every syntactic formula and only emitting ones that pass. More succinctly, all recursive sets are recursively enumerable.
But proof checking is still computationally decidable by a provably total higher order procedure. See the following: https://hal.archives-ouvertes.fr/hal-01566393
See the following: https://cacm.acm.org/blogs/blog-cacm/231495-what-turing-and-...
It also depends what the context is. A paper is not meant to prove things sufficiently for a layperson but for the author’s peers and so an omitted proof means one of “proven elsewhere;” “follows in a straightforward way from the definitions;” “follows in a straightforward way from an earlier proposition;” or “follows from a well-known pattern in the subfield.” And here “follows in a straightforward way” typically means something between “just look at;” “at each step there is only one reasonable thing to do so just do that;” and “apply all the standard tricks from the subfield and see what sticks.”
It is not true that advanced mathematics is less rigorous than more elementary maths, it’s just that materials for advanced topics require more domain knowledge, and provide less hand-holding.
On the other hand, I do feel like there should be websites where papers can be annotated by readers, who can provide missing details etc. Though this does require a lot more papers to be open access.
Primary problem is interest, really. No one's going to annotate "The Last Ditch Journal Of Applied Theorem"'s non-headliner papers.
So, hyperlinking is not what is needed for outsiders. What's needed is lots of extra exposition and explicit connection-building/hand-holding/narration.
The result of the hard work of doing so is typically called "a book". Which, hopefully, makes it clear why no author does this exposition and connection-building work for everything they write...