I'm always fascinated by how Gödel's incompleteness theorems, Cantor's diagonalization proof, Turing's halting problem, and Russel's paradox all seem to graze the boundaries of logic. There's something almost terrifying about how everything we know seems to "bottom out" and what we're left with is an embarrassingly small infinite set of truths to grapple with.<p>It really feels to me as if the distinctions between countable vs uncountable; rational vs irrational; discrete vs continuous; all represent the boundary between physics and mathematics – an idea I wish I could elaborate more precisely, but for me stands only on a shred of intuition.<p>I've been interested lately in Stephen Wolfram's and Scott Aaronson's writings on related ideas.<p>Aaronson on Gödel, Turing, and Friends: <a href="https://www.scottaaronson.com/democritus/lec3.html" rel="nofollow noreferrer">https://www.scottaaronson.com/democritus/lec3.html</a><p>Wolfram on computational irreducibility and equivalence:
<a href="https://www.wolframscience.com/nks/chap-12--the-principle-of-computational-equivalence/" rel="nofollow noreferrer">https://www.wolframscience.com/nks/chap-12--the-principle-of...</a>
Everyone has their own way of stumbling through to a breakthrough, where suddenly things that had been confusing and complex suddenly seem clear, beautiful, and intuitive.<p>Here are a couple of thoughts on Godel's incompleteness theorem that helped me get there.<p>First, a description of the idea; consider the following two statements:<p>"There exists a formula with Godel number M that has the property that neither the formula nor its negation has a proof."<p>"Oh, by the way. The Godel number of the above formula is M."<p>"M" in the above is an actual number. In the first statement, one has an arithmetic expression (i.e., "3 + 4*5 + 12^100000 + ...") that is short but that evaluates to a really large number.<p>After developing the idea of mapping formulas and proofs of first-order logic to integers, Godel needed to use his new tool to come up with some way to express self reference. (The formula above has to have an embedded arithmetic expression "M" that unwraps and and evaluates to the Godel number of the entire formula.)<p>Godel devised what we would today recognize as exactly the Y combinator, expressed in first order arithmetic.<p>This was a shocking realization when it dawned on me, and it enabled me to gain an insight to the magnificent subtlety of Godel's mind.<p>I am personally comfortable with lisp, functions as first-class objects, lambda calculus, etc., as is certainly the case for many Hacker News readers.<p>So, at least for me, the above connection helped an awful lot to really understand the heart of Godel's insight.
Has anyone done work on finding undecidable math beyond self-referential statements? Meaning: beyond variations of "who shaves the barber," do we have a sense that the undecidable statements are all pathologically long, or are there (we think) undecidable statements a human can comprehend that are undecidable that don't rely on self-reference?
I have a blog post that does a somewhat deeper dive into how to build a self-referential sentence @ <a href="https://r6.ca/blog/20190223T161625Z.html" rel="nofollow noreferrer">https://r6.ca/blog/20190223T161625Z.html</a> where I attempt to answer the question:<p>> I never understood the step about how a system that can do basic arithmetic can express the "I am not provable in F" sentence. Does anyone have an ELI30 version of that?
Veritasium has an excellent video explaining the proof and the historical context.<p><a href="https://youtu.be/HeQX2HjkcNo" rel="nofollow noreferrer">https://youtu.be/HeQX2HjkcNo</a>
I've only had one math prof be able to articulate Gödel's Incompleteness Theorem for me in a way that I could really understand (on a superficial level of course).<p>She was such a great math prof. Weird how one person can make you love a subject even after years of not so great teachers.
Nagel & Newman's <i>Gödel's Proof</i> is an excellent book on how the proof works. It doesn't have all the tie-ins and fun asides that GEB has, but it's stronger for it.
From a newbie here, Aside from the one (and sufficient) self referential formula, have we come up with other examples of non decidable propositions that are meaningful?
Does anyone know of any material linking Godel, Turing, and John McCarthy's work, beyond their individual publications?<p>It's also my understanding that Godel did not like publishing. Has his unpublished work ever been combed through and published in some form? Did he primarily write in English or German? Who has his personal papers?
I thought this writeup was quite good. Anyway, anyone interested in this is also likely interested in Rosser's theorem: <a href="https://scottaaronson.blog/?p=710" rel="nofollow noreferrer">https://scottaaronson.blog/?p=710</a>
I have known about Godel's work and the incompleteness theorem but never understood it much until I read this article. Can anyone recommend a book relating to Godel's work written is a similarly accessible style?
John Conway’s lectures are quite good.<p><a href="https://www.youtube.com/watch?v=bSx63Uy-gn0" rel="nofollow noreferrer">https://www.youtube.com/watch?v=bSx63Uy-gn0</a>
I find the section about substitution too quick and consequently confusing. For example, the author didn't clearly explain the meaning of sub(x,y,z).
<a href="https://youtu.be/5LWQPGjAs3M?si=WBu6C6mWCZ88pH-K" rel="nofollow noreferrer">https://youtu.be/5LWQPGjAs3M?si=WBu6C6mWCZ88pH-K</a><p>Any takes on this ? Spreads doubts over godels proofs