Hacker News Reader

It's very hard to believe Godel didn't face problems you faced. He probably did mistakes too, and went back periodically to make sure his proofs are sane. He was probably stuck too, many times even, and solved those problems as other mathematicians solve their problems. After all, it took him many years to complete his proof. And even more years until theorems stabilized to today's form (i.e. Rosser's trick etc). People have been practicing formal mathematics long before Godel, and this cycle of being stuck and solving problems is pretty common in mathematics. His coworkers would have had the same sort of issue. This seems to indicate me that GP comment is right that the inciting incident was understanding the correspondence between mathematics and its encoding. Which brings us to:

> 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.

Has anyone tried to find a transcript of the Gibbs Lecture? Any luck? It apparently appears in Vol III of Godel's Collected Works, and nowhere else I can see. Thanks!

Two things: if you can find this text by Fefermann, this is very helpful: Are There Absolutely Unsolvable Problems? Gödel's Dichotomy https://academic.oup.com/philmat/article-abstract/14/2/134/1... it's super simple and clarifies a lot of things about Godel.

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.

Could you send it to jacob at-sign solidangle.ca? I would greatly appreciate it.

I couldn't find your contact information. It might be good to add it to your profile for other people.

Sorry, my bad, I never realized HN doesn't have PMs (or does it? Couldn't find an inbox). Sending the pdf to your email.

Thanks for the pointer to Feferman's (very interesting) article. As for Godel, my university's library turns out to have a set of the Collected Works. So, I'll just check that out. Thanks!

The Gibbs lecture can indeed be found in Kurt Gödel, Collected Works, Volume III, Unpublished essays and lectures, edited by Feferman et al., 1995.

http://libgen.io/search.php?req=godel+collected+works+3&open...

https://ipfs.io/ipfs/QmfHv87H26WavgKxWs11Y2GuoHR62Ge32HvxhDo...

> People have been practicing formal mathematics long before Godel

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.

> 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 :)

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.

It's super easy to prove if you assume the Halting Problem is undecidable. Basically,

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.

> It's super easy to prove if you assume the Halting Problem is undecidable.

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.

It isn't, actually. The proof of the undecidability of the halting problem is rather straightforward. You just assume you have a program that determines whether or not its input halts or loops. Then you write a program that uses your assumption as a helper and does the opposite:

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.

Here's my favourite version of this proof, in the style of a poem by Dr. Seuss: http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html

The proof of the Halting Problem's undecidability is a lot less technically challenging. Here it is, off the top of my head:

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).

> Construct the program BOOM(n) that runs forever if HALT(n) returns 1 and returns 0 if HALT(n) returns 1.

I assume you mean "returns 0 if HALT(n) returns 0"?

That is correct. I did say this was on the fly ;-)

This proof using Turing machines is indeed very slick! Its elegance is balanced by its nonconstructiveness: Gödel's proof yields an explicit example for an unprovable statement (namely a formal rendering of "this statement is not provable"), while the Turing machine proof doesn't.

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.

As Wittgenstein correctly pointed out, Gödel's proposition "I'm unprovable" is not a proposition in Russell's system because it leads to inconsistency. Consequently, Gödel's incompleteness results are not valid for Russell's system. The proposition "I'm unprovable" cannot be constructed as a fixed point of P |-> ~|-P because ~|-P has order one greater than the order of P.

Could you give a reference for this claim of Wittgenstein’s, please?

A reference is:

Ludwig Wittgenstein. 1956. Remarks on the Foundations of Mathematics, Revised Edition Basil Blackwell. 1978.

There is a discussion here:

https://hal.archives-ouvertes.fr/hal-01566393

That seems entirely circular.

Gödel's proposition "I'mUnprovable" cannot be constructed as a fixed point of P |-> ~|-P because ~|-P has order one greater than the order of P.

The Turing machine proof does yield an explicit unprovable statement when you combine it with the (constructive) proof of the undecidability of the Halting problem. Let H be the Turing machine that, when given a Turing machine M, searches for a proof (in the formal system under consideration) that M halts or a proof that M doesn’t halt. Build the machine Q that quines itself to apply H to the code of Q itself, then either loops forever or halts according to the opposite of what H purportedly proved. Then the true statement “Q doesn’t halt” is unprovable in the formal system.

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.

Wow! Didn't notice that. I stand corrected. Your rendition of the proof even dispenses of the assumption that the formal system correctly judges the halting behaviour of Turing machines.

Thank you for this. Else I'd have perpetuated that myth further!

I’m personally a fan of using Chaitin’s constant (Ω). It’s easy to show that, for some finite n, the nth digit of n is uncomputable. It follows that statements of the form “the nth binary digit of Ω 0” can neither be proven nor disproven.

cough Hypercomputation cough

Hypercomputation is a fascinating concept; I particularly like infinite-time Turing machines, which can continue computing "at the end of time" (day ω), at the day after that (ω + 1), the day after that (ω + 2), at the second end of time (day ω ⋅ 2), the day after that (day ω ⋅ 2 + 1), and so on.

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...

If you actually want to make the proof above as rigorous as Goedel’s original proof, you’ll find that it will be exactly as technical as the original. The technical difficulty in the proof above is hidden in the step 2 — what you need to show is that every statement of a form “the Turing machine T = {..., ..., ...} halts on input ...” is expressible in the language of first order arithmetic. To do that, you need to do exactly the same work as Goedel did, with all the finite string encoding etc.

>Again, it seems unlikely that this was the sticking point.

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 proof - page after page of work showing how to encode and decode formal propositions using primitive recursive functions.

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.

You're missing my point.

Whether you have a thing memorized is fairly unrelated to how complex the thing is.