4 ms·

That'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

by kmill 7y ago

That'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.)

lisper 7y ago
> this diagonalization argument is the core idea No, not really. I mean yes, it is, if you're a mathematician. But no, it's not, if you're someone who needs to have binary encoding explained to them, which the original article attempts to do. (And if you're a mathematician you don't need Godel's theorem explained to you at all.) Here's how I would go on with the exposition: A formal proof is a sequence of strings, each of which can be derived from the set of strings that precede it in the sequence according to a set of rules. There is a particular set of rules called Peano arithmetic (because they were invented by a guy named Peano) that are so far mankind's best attempt at encoding the fundamental properties of the natural numbers. Ideally, a string in a formal proof under the Peano rules should correspond to a true statement about numbers, and conversely, every true statement about numbers should have a corresponding proof. But it turns out that both of these cannot be simultaneously true. In particular, we can prove that if all strings in proofs correspond to true statements about numbers, then there must be true statements about numbers that cannot appear in proofs. Godel's original proof involved constructing a number N whose corresponding string essentially means "The string corresponding to N has no proof." Describing how N is constructed is tricky, but since we know about the halting problem we can prove this result in a much more straightforward way: suppose that we could prove any true statement about numbers. Consider an arbitrary program P. That program can be encoded as a number N. So the statement "The program corresponding to the number N halts" is a claim about numbers. It is either true or false. If it is true, then by our assumption we can prove it, and if it is false then its negation is true and we can prove that. So now all we have to do to solve the halting problem is to systematically search through the space of all possible proofs until we find a proof either of "the program corresponding to the number N halts" or its negation, at which point we will know whether or not P halts, and so we have solved the halting problem. But we already know that we can't solve the halting problem, so our assumption that all true statements about numbers can be proven must be false.
- kmill 7y ago
  I find computer scientists have a stronger grasp on encodings than mathematicians, who tend to get bogged down in these details due to lack of familiarity. With what I wrote up, the point I failed to make is that it comes down to some cleverness in how you mess around with read, eval(=provable), and print. That is, follow the Lisp way and think in s-expressions. I was responding specifically to > 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. The thing I'm taking issue with is calling parsing the core idea, with the rest "just"[1] being tedious details, where, as someone who has done some PL implementations, the parsing seems to me to be the tedious part. It's an important idea that's essential to the proof, but, again, that's like saying parsing is the core problem in writing a compiler (or that writing read is the core problem in implementing a Lisp interpreter). This is not exactly evidence of any kind, but notice your whole final paragraph is a diagonalization argument, and it is longer than the first paragraph of your exposition, which quickly explains how strings can represent logical statements and proofs. Maybe this is a synthesis: the core idea is that you can write an interpreter that takes an encoding of a logical statement and returns whether or not it is provable. Since the interpreter is itself a logical statement, you can apply a diagonalization argument to produce a true statement that refutes its own provability. (When I say the core idea is the diagonalization, I mean both the interpreter and the fixed point finding. When you say the core idea is encoding, I suspect you might mean more the interpreter than how your comment reads to me.) By the way, with the halting problem argument, it seems like if you're very careful you can write out an explicit Godel sentence, like what the Lawvere fixed point theorem would provide. I'm sort of curious what it would look like, rather than your recipe for how to construct it. (I also wonder what the shortest Godel sentence is. But only as much as I wonder what the shortest quines are.) > "The string corresponding to N has no proof" Small correction: it's that "N being true is equivalent to N having no proof." If N is false, then it is provable (bad), so if things are consistent it must be true, hence unprovable. It's interesting that N is a true statement. [1] I have a banned words list in my office; one entry is "just" because of just what it lets you sweep under the rug.

by kmill 7y ago

lisper 7y ago

> this diagonalization argument is the core idea No, not really. I mean yes, it is, if you're a mathematician. But no, it's not, if you're someone who needs to have binary encoding explained to them, which the original article attempts to do. (And if you're a mathematician you don't need Godel's theorem explained to you at all.) Here's how I would go on with the exposition: A formal proof is a sequence of strings, each of which can be derived from the set of strings that precede it in the sequence according to a set of rules. There is a particular set of rules called Peano arithmetic (because they were invented by a guy named Peano) that are so far mankind's best attempt at encoding the fundamental properties of the natural numbers. Ideally, a string in a formal proof under the Peano rules should correspond to a true statement about numbers, and conversely, every true statement about numbers should have a corresponding proof. But it turns out that both of these cannot be simultaneously true. In particular, we can prove that if all strings in proofs correspond to true statements about numbers, then there must be true statements about numbers that cannot appear in proofs. Godel's original proof involved constructing a number N whose corresponding string essentially means "The string corresponding to N has no proof." Describing how N is constructed is tricky, but since we know about the halting problem we can prove this result in a much more straightforward way: suppose that we could prove any true statement about numbers. Consider an arbitrary program P. That program can be encoded as a number N. So the statement "The program corresponding to the number N halts" is a claim about numbers. It is either true or false. If it is true, then by our assumption we can prove it, and if it is false then its negation is true and we can prove that. So now all we have to do to solve the halting problem is to systematically search through the space of all possible proofs until we find a proof either of "the program corresponding to the number N halts" or its negation, at which point we will know whether or not P halts, and so we have solved the halting problem. But we already know that we can't solve the halting problem, so our assumption that all true statements about numbers can be proven must be false.

kmill 7y ago
I find computer scientists have a stronger grasp on encodings than mathematicians, who tend to get bogged down in these details due to lack of familiarity. With what I wrote up, the point I failed to make is that it comes down to some cleverness in how you mess around with read, eval(=provable), and print. That is, follow the Lisp way and think in s-expressions. I was responding specifically to > 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. The thing I'm taking issue with is calling parsing the core idea, with the rest "just"[1] being tedious details, where, as someone who has done some PL implementations, the parsing seems to me to be the tedious part. It's an important idea that's essential to the proof, but, again, that's like saying parsing is the core problem in writing a compiler (or that writing read is the core problem in implementing a Lisp interpreter). This is not exactly evidence of any kind, but notice your whole final paragraph is a diagonalization argument, and it is longer than the first paragraph of your exposition, which quickly explains how strings can represent logical statements and proofs. Maybe this is a synthesis: the core idea is that you can write an interpreter that takes an encoding of a logical statement and returns whether or not it is provable. Since the interpreter is itself a logical statement, you can apply a diagonalization argument to produce a true statement that refutes its own provability. (When I say the core idea is the diagonalization, I mean both the interpreter and the fixed point finding. When you say the core idea is encoding, I suspect you might mean more the interpreter than how your comment reads to me.) By the way, with the halting problem argument, it seems like if you're very careful you can write out an explicit Godel sentence, like what the Lawvere fixed point theorem would provide. I'm sort of curious what it would look like, rather than your recipe for how to construct it. (I also wonder what the shortest Godel sentence is. But only as much as I wonder what the shortest quines are.) > "The string corresponding to N has no proof" Small correction: it's that "N being true is equivalent to N having no proof." If N is false, then it is provable (bad), so if things are consistent it must be true, hence unprovable. It's interesting that N is a true statement. [1] I have a banned words list in my office; one entry is "just" because of just what it lets you sweep under the rug.