While I applaud the effort to recast Godel's proof in computational terms, I think this author makes a horrible mess of it. The core idea is extremely simple, particularly in today's world: strings of symbols can be re-cast as numbers (and vice-versa), and rules for manipulating those symbols can therefore be re-cast as arithmetic. The mapping between strings of symbols and numbers is called an encoding. Godel's original encoding relied on exponentiation of prime numbers, and that produced one particular set of mathematical operations that mapped onto the formal rules of Peano arithmetic. Nowadays we can simply encode symbols as ascii or unicode with the obvious translation into numbers and arithmetic, and that produces a different set of mathematical operations that map onto the formal rules of Peano arithmetic. All the rest, all the heavy lifting, is just cranking out the tedious details of what those mathematical operations actually are, but none of that is necessary in order to understand the core idea of the proof.
Gödel’s Proof, by Nagel & Newman gives a good explanation for the semi-layman or undergrad coming across this for the first time.<p>Before picking up this book as an undergrad in pure maths, I still had romantic ideas about a separate platonic universe and the divine authority of mathematics to explain all human thought.<p>This book, along with studying the various geometries, each with a different choice of axioms not necessarily based in ‘reality’, destroyed the majority of that romance.
For me the easiest way to prove Gödel first's with perfect rigor, without bothering with numberings (but using computational undecidability) is here <a href="http://users.utu.fi/jkari/automata/fullnotes.pdf" rel="nofollow">http://users.utu.fi/jkari/automata/fullnotes.pdf</a> (Section 4.10)
My favourite proof of the (Second) Incompleteness Theorem is the semantic proof due to Jech/Woodin: <a href="https://andrescaicedo.files.wordpress.com/2010/11/2ndincompleteness1.pdf" rel="nofollow">https://andrescaicedo.files.wordpress.com/2010/11/2ndincompl...</a><p>It is easiest to think about in terms of set theory, but it is possible to formalize it in a fragment of second-order arithmetic that is conservative over PA (and this conservativity is provable in PA itself). The beauty of this proof is that it first establishes semantic incompleteness without formalizing a proof system; the connection to syntactic incompleteness only uses the Completeness Theorem, which is of independent interest.
Is this a correct (over)simplification of the theory: there’s not enough information in a system that on its own can describe it’s correctness?
I know this is a very naive and maybe incorrect interpretation of it, but I think this theorem is so important in so many ways, it should be used more in layman’s discussions, even though I understand that it’s easy to misuse it etc.
The result in the Medium article applies only to a theory whose theorems are computationally enumerable. In computer science, we need theories that axiomatize subject matter such as natural numbers and computation up to a unique isomorphism so that the objects being axiomatized are characterized precisely. Such theories have induction axioms with <i>uncountable</i> instances. Consequently, the theories have <i>uncountable</i> axiom instances and their theorems <i>cannot</i> possibly be computationally enumerated although each proof can be computationally checked for correctness.<p>Therefore, a <i>more general proof</i> is needed to prove incompleteness. Such a proof can be found here:<p><a href="https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3459566" rel="nofollow">https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3459566</a>
There's another paper called "Incompleteness Ex Machina" with several proofs of both the first and second incompleteness theorems.<p><a href="https://arxiv.org/abs/1909.04569" rel="nofollow">https://arxiv.org/abs/1909.04569</a>
The article claims, "Given that some sets of strings are decidable, it stands to reason that other sets of strings are not. "<p>How can a string not be decidable?! Just search for the string in the set. It is either there, or not there.<p>What an I missing?