Edit: Wow, I really am an idiot. I assumed the second statement was true about every statement, but I just realized (by reading one extra comment after posting) that by Lob’s Theorem that’s not true. But my original idea, that the first statement is all that’s required to prove anything, still seems to hold.
Okay, I can follow the first proof when I assume statement 1, but I don’t quite understand how cousin_it got to 1. The Diagonal Lemma requires a free variable inside the formula, but I can’t seem to find it.
In fact, I think I totally misunderstand the Diagonal Lemma, because it seems to me that you could use it to prove anything. If you replace “outputs(1)” by “2==3″, the proof still seems to hold. Statement 2 would still be true with “2==3” (it is true about any statement, after all), and all the logic that follows from those two statements would be true. In fact, by an unclearly written chain of reasoning which I originally intended to post before realizing that it would be much simpler to just say this, all you seem to require is the first statement to be able to prove anything. If I am mistaken, which is probable, then I expect my error lies in the assumption that “outputs(1)” could be replaced by any string of code.
For my original unclear explanation of why the first statement in the proof seems to allow anything to be proven, in case anyone cares for it:
Also, I must be an idiot, but it seems to me that you can prove pretty much anything using 1. As far as I can tell, the “eval(outputs(1))” could be “2==3“ or any other statement, and the only reason “eval(outputs(1))” is used is because it’s useful in the proof. Given that statement 1 is proven, “eval(box)” must return true, because if it returns false, then “proves(box,n1)” cannot return true, and therefore “implies(proves(box, n1),eval(outputs(1)))” must return true, and false!=true. Assuming that my reasoning is correct (a very questionable assumption, I know), I have just proven that “eval(box)” is true, therefore “prove(box,n1)” is also true for some arbitrarily large n1. Therefore, the “implies” will return “eval(outputs(1))”, which must be true for “eval(box)” to equal it. So given my earlier assumption (which I suspect is my error) that “eval(outputs(1))” can be replaced by anything, then I can replace it by any statement, which must return true to equal “eval(box)”. So through this, I seem to have proven that “2==3”.
Anyone care to point me to my mistake (or, to satisfy my wildest of dreams, say that I appear to be right ;) )?
I don’t understand how the first statement can be used to prove anything...
The second statement might be true for every statement, but it’s not necessarily provable for every statement, which is required in the proof. In fact, the second statement is provable for “outputs(1)” by inspection of the program (because the program searches for proofs of “outputs(1)”), but not provable for “2==3” (because then “2==3″ would be true, by Lob’s theorem).
I’m sorry, my comment grew into a mess, I should have cleaned it up a bit before posting. Anyway, I agree fully about the second statement only applying to this program, that’s what I realized in the edit.
But for the first statement, I’ll try to be a bit more clear.
My first claim is that “eval(box) == implies(proves(box, n1), eval(‘2==3’))” is a true statement, proven by the Diagonal Lemma. I’ll refer to it as “statement 1″, or “the first statement”.
If “eval(box)” returns false, then for the first statement to be true, “implies(proves(box, n1), eval(‘2==3’))” must return false. “implies” only returns false if “proves(box, n1)” is true and “eval(‘2==3’)” is false. Therefore for statement 1 to be true when “eval(box)” is false, then “proves(box, n1)” has to be true, which is a contradiction: “eval(box)” can’t be false and also provably true. Therefore, “eval(box)” must be true.
So let’s say “eval(box)” is true, that means that “implies(proves(box, n1), eval(‘2==3’))” must also return true for statement 1 to be true. One way for the “implies” statement to return true is for “proves(box, n1)” to return false. Since I have proven above that “eval(box)” is true, any good definition of the “proves” function will also return true, because if it finds no other, it will at least find my proof. Therefore, “proves(box, n1)” will return true.
So there is only one other way for the “implies” statement to return true: “eval(‘2==3’)” must return true. Therefore, “eval(‘2==3’)” returns true, and it follows from this that 2=3.
Your proof of eval(box) relied on the fact that eval(box) can’t be false and also provably true. But that fact is equivalent to consistency of the formal theory, so it can’t be proven within the formal theory itself, by Godel’s theorem. Of course, since eval(box) is a terminating computation that returns true (your proof of that is correct), the formal theory can eventually prove that by step-by-step simulation. But that proof will be much longer than your proof above, and much longer than n1. In fact, proves(box,n1) will return false, and your comment serves as a nice proof of that by reductio.
Don’t get discouraged, it’s a very common mistake =)
Edit: Wow, I really am an idiot. I assumed the second statement was true about every statement, but I just realized (by reading one extra comment after posting) that by Lob’s Theorem that’s not true. But my original idea, that the first statement is all that’s required to prove anything, still seems to hold.
Okay, I can follow the first proof when I assume statement 1, but I don’t quite understand how cousin_it got to 1. The Diagonal Lemma requires a free variable inside the formula, but I can’t seem to find it.
In fact, I think I totally misunderstand the Diagonal Lemma, because it seems to me that you could use it to prove anything. If you replace “outputs(1)” by “2==3″, the proof still seems to hold. Statement 2 would still be true with “2==3” (it is true about any statement, after all), and all the logic that follows from those two statements would be true. In fact, by an unclearly written chain of reasoning which I originally intended to post before realizing that it would be much simpler to just say this, all you seem to require is the first statement to be able to prove anything. If I am mistaken, which is probable, then I expect my error lies in the assumption that “outputs(1)” could be replaced by any string of code.
For my original unclear explanation of why the first statement in the proof seems to allow anything to be proven, in case anyone cares for it:
Anyone care to point me to my mistake (or, to satisfy my wildest of dreams, say that I appear to be right ;) )?
I don’t understand how the first statement can be used to prove anything...
The second statement might be true for every statement, but it’s not necessarily provable for every statement, which is required in the proof. In fact, the second statement is provable for “outputs(1)” by inspection of the program (because the program searches for proofs of “outputs(1)”), but not provable for “2==3” (because then “2==3″ would be true, by Lob’s theorem).
I’m sorry, my comment grew into a mess, I should have cleaned it up a bit before posting. Anyway, I agree fully about the second statement only applying to this program, that’s what I realized in the edit.
But for the first statement, I’ll try to be a bit more clear.
My first claim is that “eval(box) == implies(proves(box, n1), eval(‘2==3’))” is a true statement, proven by the Diagonal Lemma. I’ll refer to it as “statement 1″, or “the first statement”.
If “eval(box)” returns false, then for the first statement to be true, “implies(proves(box, n1), eval(‘2==3’))” must return false. “implies” only returns false if “proves(box, n1)” is true and “eval(‘2==3’)” is false. Therefore for statement 1 to be true when “eval(box)” is false, then “proves(box, n1)” has to be true, which is a contradiction: “eval(box)” can’t be false and also provably true. Therefore, “eval(box)” must be true.
So let’s say “eval(box)” is true, that means that “implies(proves(box, n1), eval(‘2==3’))” must also return true for statement 1 to be true. One way for the “implies” statement to return true is for “proves(box, n1)” to return false. Since I have proven above that “eval(box)” is true, any good definition of the “proves” function will also return true, because if it finds no other, it will at least find my proof. Therefore, “proves(box, n1)” will return true.
So there is only one other way for the “implies” statement to return true: “eval(‘2==3’)” must return true. Therefore, “eval(‘2==3’)” returns true, and it follows from this that 2=3.
So, where did I go wrong?
Your proof of eval(box) relied on the fact that eval(box) can’t be false and also provably true. But that fact is equivalent to consistency of the formal theory, so it can’t be proven within the formal theory itself, by Godel’s theorem. Of course, since eval(box) is a terminating computation that returns true (your proof of that is correct), the formal theory can eventually prove that by step-by-step simulation. But that proof will be much longer than your proof above, and much longer than n1. In fact, proves(box,n1) will return false, and your comment serves as a nice proof of that by reductio.
Don’t get discouraged, it’s a very common mistake =)