I watched the video and the video does not in any way attempt to debunk Godel's proof.
I think moreso it just shows that Godel's proof is not as significant or as relevant as many people make it out to be, and on the whole I'd say I agree with that.
I didn't watch the video, but FWIW I have personally formally verified the First Incompleteness Theorem (Goedel-Rosser variant) within the Coq proof assistant.
My biggest mistake was following the traditional single variable definition of substitution. I now understand that modern CS definitions of substitution typically substitute all (free) variables simultaneously. For variables that you don't want to substitute, you are required to explicitly map them back to themselves.
Chapter 7 of my thesis <https://r6.ca/thesis.pdf> has some more comments. With a bit more care using Prop/Set maybe one could compute explicitly what these Goedel sentences are (similar to <https://web.archive.org/web/20160528092209/http://tachyos.or...>). Maybe using Robinson Q instead of Hodel's obscure NN system would have been better, or maybe with a bit more abstraction it would be easier to apply the proof to other axioms systems, such as ZF, which don't use the same language that PA does. And maybe making sure the Second Incompleteness could follow more easily would be good (which has since been formalized elsewhere).
The strengthened liar paradox discussed in the video is "This statement is not true", whereas Gödel constructed a mathematical statement that says something along the lines of "This statement is not provable". Proving something is a different process than stating something.
What doubt does it spread?
What’s the key take away?
Is it just a crank video?
A famous proof published in 1931 that has had much discussion and testing is debunked and disproved on YouTube!
No way of telling except to click through and watch a 15 minute video that isn’t even vouched for or elaborated on by the commenter posting it.