3 ms·

https://youtu.be/5LWQPGjAs3M?si=WBu6C6mWCZ88pH-K https://youtu.be/5LWQPGjAs3M?si=WBu6C6mWCZ88pH-K Any takes on this ? Spreads doubts over godels proofs

jamiek88 3y ago
What a lazy comment. 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.
- Kranar 3y ago
  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.
rssoconnor 3y ago
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.
- abrenuntio 3y ago
  Hey I know your proof, the 2005 paper is on my desk :-) If you were to code this in Coq again today, would you do things different in some way?
  - rssoconnor 3y ago
    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 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.org/godel/Godel_number.html 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).
smokel 3y ago
This does not cast doubt on Gödel's proofs. 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.

jamiek88 3y ago

What a lazy comment. 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.

Kranar 3y ago
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.

rssoconnor 3y ago

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.

abrenuntio 3y ago
Hey I know your proof, the 2005 paper is on my desk :-) If you were to code this in Coq again today, would you do things different in some way?
- rssoconnor 3y ago
  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 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.org/godel/Godel_number.html 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).

smokel 3y ago

This does not cast doubt on Gödel's proofs. 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.