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.

> 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