[dvt]

Just going to echo @dwohnitmok here in saying that this is a pretty 'meh' article. Understanding Godel's First Incompleteness Theorem is actually very accessible, I wrote about it a few years ago[1]. His second is much more involved and laymen won't have the required tools to grasp it. In my opinion, the easiest way to understand it is probably using Löb's Theorem, but that's neither here nor there. Either way, I'm of the opinion that arithmetic coding is very confusing and shouldn't be used to introduce people to Godel.

[1] https://dvt.name/2018/03/12/godels-first-incompleteness-theo...

[krick]

I'm not sure this is equivalent to Gödel's theorem. Actually, I'm not sure this is a correct proof of anything at all, merely a sort-of demonstration of Richard's paradox.

First, for reference, let me quote First Incompleteness Theorem: "Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F." (from Wikipedia)

Now back to your post.

Obviously, f' is not in T and it is not computable. But neither is T. It is incomputable merely by being the list of computable functions, which we cannot construct because of halting problem and stuff like that.

And your definition of f' relies on having T. So we don't in fact have seen "statement f'". So, the direct connection between Gödel's theorem and your construct is not obvious to me, because first is about constructable, but unprovable statements, and second seems to be a faulty (i.e. mathematically uninterpretable) construct itself.

[dvt]

> I'm not sure this is equivalent to Gödel's theorem.

It is. In fact, I've seen it proven this way several times (mostly in CS-y papers), but it's definitely not common. My post is in fact based (almost beat-by-beat) on this UC Davis lecture: https://www.youtube.com/watch?v=9JeIG_CsgvI

[krick]

Your plain and confident statement "it is" doesn't really address any of my concerns, and I just explained why, as it seems, it actually isn't.

P.S.

I did some random googling, and while I'm not sure, all this story seems to be based off of Paul Finsler's work, which he himself thought to be the priority for an incompleteness theorem (Collected Works Vol. IV., p. 9), but didn't seem so to Gödel (and, seemingly, the majority of those who had to say something about it).

If this indeed is the same thing, it would explain to me why this "proof", which doesn't seem to me like a proof at all is so widespread. But, again, I'm not sure I'm reading into it correctly, and operating under assumption that if somebody could provide something more weighty than "it is" statement, I could be persuaded otherwise.

[dvt]

> Your plain and confident statement "it is" doesn't really address any of my concerns...

Your concerns aren't really valid (for example, the computability of T is irrelevant). These are questions I already answered before on both HN and in the Disqus comments. Further, metalogic was my area of focus in school, so I'm quite familiar with intricacies here, and don't really feel it's useful to get too deep into the weeds. But don't take my word for it; Dr. Gusfield's paper (that the lecture is based on) can be found here: https://csiflabs.cs.ucdavis.edu/~gusfield/godelproofreviseda...

The ideas in this proof have been well-tread by Scott Aaronson, Peter Smith, and Michael Sipser. My curt "it is" is also meant to nip in the bud -- correct -- claims that it's not exactly what Godel proved (the OG variant is actually slightly stronger). Why I'd want to nip these in the bud is that in school, you technically learn the weaker variant (albeit starting with a Henkin construction of Godel's Completeness Theorem). Sort of like this[1]. But the difference between the two is so nuanced, it's not even really worth bringing up unless we're in a graduate seminar.

[1] https://hal.archives-ouvertes.fr/hal-00274564/document

[irontinkerer]

Per the end of your article, have you started writing about the 2nd theorem yet?

[dvt]

I did (https://dvt.name/2018/04/11/godels-second-incompleteness-the...) -- but like I mentioned, it's not very accessible and I don't think it's a particularly good explanation, either (although I've yet to find one I really like, to be honest).