12 ms·
A Computability Proof of Gödel’s First Incompleteness Theorem
- pfortuny 7y ago“semi” rigurously is what spooked me. The thing with Gödel’s proof is that it is very hard to do rigurously...
- QuesnayJr 7y agoIt's not that hard. There are several computer-checked proofs of it. It's hard to explain, because the idea of encoding statements about a system in terms of the system itself is weird if you haven't seen it before.
- thethirdone 7y agoThere are a lot of details that are needed in the proof. You need to define a first order logic and prove arithmetic theorems on top of PA to even start a rigorous proof. That said it can be fully covered in a single semester of undergraduate study, so its not that hard. There are many theorems that couldn't be fully proved in a semester.
- mensetmanusman 7y agoThere are many true theorems that couldn’t be fully proved ;)
- caleb-allen 7y agoProve it!
- cellular 7y agoOk: "this sentence is unprovably true".
- mensetmanusman 7y agoOr Pinocchio saying: “My nose will get longer”
- adz_6891 7y agoI went through it the first time by reading over Computability & Logic (5th edition) [1]. I'd love to go over it again, and would recommend it to anyone interested who has a few weekends to invest. [1] https://www.goodreads.com/book/show/1556746.Computability_and_Logic https://www.goodreads.com/book/show/1556746.Computability_an...
- michelmichel 7y agoFor me the easiest way to prove Gödel first's with perfect rigor, without bothering with numberings (but using computational undecidability) is here http://users.utu.fi/jkari/automata/fullnotes.pdf http://users.utu.fi/jkari/automata/fullnotes.pdf (Section 4.10)
- noname120 7y agoYou can access directly the relevant section[1] using the `#page=` directive. See here[2] for a full list of parameters you can use. [1] http://users.utu.fi/jkari/automata/fullnotes.pdf#page=134 http://users.utu.fi/jkari/automata/fullnotes.pdf#page=134 [2] https://www.adobe.com/content/dam/acom/en/devnet/acrobat/pdfs/pdf_open_parameters.pdf#page=5 https://www.adobe.com/content/dam/acom/en/devnet/acrobat/pdf...
- 0db532a0 7y agoGödel’s Proof, by Nagel & Newman gives a good explanation for the semi-layman or undergrad coming across this for the first time. 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. 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.
- dasmithii 7y agoReading it now and enjoying it a lot. It's destroying one romance in favor of another!
- chongli 7y agoExactly! The beauty of life is in its flaws and limitations. Perfection is boring. Gödel opened the door to a multiverse of mathematics, all flawed in some way, yet not unworthy of study. Mathematicians of the past sought perfection for the glory of God. Now we have the opportunity to give credit where it’s due: to our fellow human beings, many of whom devoted their lives to the craft of mathematics.
- xamuel 7y agoGödel's work actually echoes Christianity quite deeply. A key theme of Christianity is that humans are incapable of being good (much less of achieving perfection) on their own strength--no more than Hilbert could axiomatize all of mathematics with a consistent, computable set of axioms. "Do not be overly righteous, and do not make yourself too wise." (Ecclesiastes 7:16) "There is no distinction, for all have sinned and fall short of the glory of God, and are justified freely by His grace through the redemption that is in Christ Jesus." (Romans 3:22-23)
- 0db532a0 7y agoIt would be interesting to see an analysis where the most fundamental results in mathematics are looked at under the light of their discoverers' ideological beliefs and psychologies. I wonder whether Gödel would have pursued the Proof if he did not believe in an omnipotent god.
- cwzwarich 7y agoMy favourite proof of the (Second) Incompleteness Theorem is the semantic proof due to Jech/Woodin: https://andrescaicedo.files.wordpress.com/2010/11/2ndincompleteness1.pdf https://andrescaicedo.files.wordpress.com/2010/11/2ndincompl... 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.
- gre 7y agoThere's another paper called "Incompleteness Ex Machina" with several proofs of both the first and second incompleteness theorems. https://arxiv.org/abs/1909.04569 https://arxiv.org/abs/1909.04569
- lisper 7y agoWhile 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.
- kmill 7y agoThat's the core idea of the proof inasmuch as parsing is the core idea of writing a compiler. Once you get that part out of the way, the incompleteness theorem is a clever diagonalization argument (and is a consequence of the Lawvere fixed point theorem). The way it all sort of works is: 1. A mathematical theory is called consistent if there is some model of it, a self-consistent set M of all mathematical objects for that theory. For example, a model of the natural numbers would be {0,1,2,...}, but there are other models too. 2. By some parsing method, we can encode every "first-order definable" (akin to "computable") statement and function as an element of M itself. Let (M -> M) denote the set of definable functions; by picking out an element nil from M, we can think of such a function as being a boolean-valued function, where like Lisp we say nil is the unique false value, everything else is truthy. 3. Since everything is encodable, there is a function print : (M -> M) -> M and a left inverse read : M -> (M -> M). (I imagine parse errors just return the constant-nil function.) 4. We can define lots of useful functions, like not, where not(nil) = 1 and not(x) = nil for all x != nil, where 1 is anything that's not nil. Another is iff(x,y) = (not(x) == not(y)), that is, whether both inputs are truthy in the same way. 5. An interesting function you can define is provable : (M -> M) -> M, which takes a function f and returns whether or not M contains a proof that f is non-nil for all inputs. This takes a bit of implementation, but it's not too hard. 6. Now to set up diagonalization. Define f : M -> M by f(x) = print(lambda _ -> not(provable(read(x))) iff (forall z -> read(x)(z))). 7. Lawvere's fixed point theorem (with respect to the read function) implies there is some element phi of M such that f(phi) = phi; this should be compared to the problem of quine construction, and you can in principle write phi down. Let g = read(phi). Then to both sides, feed in phi, apply read, then feed in any input (doesn't matter what; might as well use nil): g(nil) = not(provable(g)) iff (forall z -> g(z)). 8. This g(nil) is the "Godel statement." If provable(g) were true, then there would be some input x such that g(x) == nil, which contradicts the fact g is supposedly provable. On the other hand, if provable(g) were false, then (forall z -> g(z)) would be true, so provable is not able to prove all true things (it is incomplete). The way this is summarized is: either the theory is inconsistent (there is no model) or it is incomplete (the provable function can't prove all true things). The way this ends up working in the mathematical landscape is that, if there is any model at all, there is more than one. (Something is provable if and only if it is true in all models -- Godel.)
- he0001 7y agoIs 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.
- cellular 7y agoThe article claims, "Given that some sets of strings are decidable, it stands to reason that other sets of strings are not. " How can a string not be decidable?! Just search for the string in the set. It is either there, or not there. What an I missing?
- gus_massa 7y agoYou can have a infinite set of finite strings, for example {“1”, “11”, “111”, “1111”, “11111”, “111111”, “1111111”, “11111111”, ...}
- cellular 7y agoIs having an infinite amount of strings the only reason for the claim? Infinity breaks a lot of things. Infinity isn't even real. So I'm not sure this counts. It seems like the article would have mentioned infinity if that were the reason for the claim. It seems like Enumeration fails for an infinite set too.
- Hercuros 7y agoInfinity is the only reason: all finite sets of strings are decidable, simply because you can just keep a list and see if a string is in there. Important to mention that there are decidable infinite sets of strings. For instance, deciding whether a string contains only ones is easy, even though there are infinitely many such strings and you couldn’t write all of them down. A lot of these ideas don’t require any actual “realized” infinity, however. For instance, there are infinitely many natural numbers, but natural numbers themselves are still finite. You can write a program that prints every number at some time in the nearby future (ignoring physical constraints), even though there is no point in time where it will have printed all numbers. If you want to take away infinity, you have to draw an arbitrary upper bound somewhere, since unbounded things are infinite. Drawing that line is fairly arbitrary since there is no reason why things should no longer work if you add just one more.
- cellular 7y ago
- kanibal 7y agokek
- ProfHewitt 7y agoThe 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 uncountable instances. Consequently, the theories have uncountable axiom instances and their theorems cannot possibly be computationally enumerated although each proof can be computationally checked for correctness. Therefore, a more general proof is needed to prove incompleteness. Such a proof can be found here: https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3459566 https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3459566