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 =)
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 =)