I highly recommend getting Godel's proof[1] and reading it. It's an amazing journey and quite understandable from the start (the first half of the book is introduction), and I've never been able to read proofs very well. It takes concentration, but once you get it (at '17 GenR') it's almost like a symphony going off. The crystalline brilliance of the "System P" decomposition is worth it just to see how math as a process could be reduced to a such simple, clear and concise set of symbol manipulations...and then the rest shows how that could be used topple itself. Incredibly philosophically insightful.<p>[1] <a href="https://www.amazon.ca/Undecidable-Propositions-Principia-Mathematica-Mathematics-ebook/dp/B00A44R3E8/ref=sr_1_1?ie=UTF8&qid=1489447527&sr=8-1&keywords=on+formally+undecidable+systems+godel" rel="nofollow">https://www.amazon.ca/Undecidable-Propositions-Principia-Mat...</a>
A light take on the subject can be found in Logicomix: <a href="https://en.wikipedia.org/wiki/Logicomix" rel="nofollow">https://en.wikipedia.org/wiki/Logicomix</a> - a cool blend between the dry topic and comics.
This reminds me of the Berry Paradox: <a href="https://en.wikipedia.org/wiki/Berry_paradox" rel="nofollow">https://en.wikipedia.org/wiki/Berry_paradox</a>
I like very much the program x virus example/citation.. but I would put it in the other way around:
"A program can find all virus, unless the operating system is a virus itself."
"Digital Physics" (the movie) is now free on Amazon Prime. It is also available for rent/purchase on iTunes and Vimeo, in case you are kind enough to support an independent filmmaker:) Come explore the world of self-reference, infinity, complexity, Gödel & Turing, and psychedelics with Khatchig!!
Isn't Gödel's incompleteness a consequence of overly ambitious material implication properties? When you look at the truth table:<p>A | B | A -> B<p>0 | 0 | 1<p>0 | 1 | 1<p>1 | 0 | 0<p>1 | 1 | 1<p>I fail to see why all except for 1 -> 0 = 0 aren't undefined. I understand reasoning behind why this was done, but mixing unrelated predicates seems like a generally bad idea, even if it allows mechanical proofs.<p>Aren't there already "complete" systems like relevance logic? Now with computers we can perhaps make proofs we need "relevant" instead of being based on fundamentally incomplete though "simpler" logic?