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