And then couldn’t you patch up the proof somehow to show that program has to output 2? Specifically, to get the analogue of step 2, can’t you prove that proves(outputs(2), n) implies the negation of proves(outputs(1), n), and hence prove that proves(outputs(2), n) implies outputs(2)?
Even if this is correct, it only applies to the program you use in your proof, where if proves(outputs(2), n) then 2 is returned; whereas the puzzle above doesn’t allow for 2 to be returned at all. However, if I’m right then presumably something must be going wrong in the proof?
can’t you prove that proves(outputs(2), n) implies the negation of proves(outputs(1), n)
To prove that, the proof system would need to know its own consistency, because an inconsistent proof system could prove both of these statements and indeed any statement at all. But a proof system cannot know its own consistency without actually being inconsistent (Goedel’s second theorem).
Technically true. You could always just evaluate the two statements and there you have your proof, with length exponential in n. I very much doubt the proof could be made shorter than n though, because the statement is equivalent to “you can’t find a contradiction in these axioms using less than n steps”, the difficulty of which should grow way faster than linearly in n.
Good catch! Yes, my argument only shows that there’s no short easy proof. You can always just evaluate the two statements and there you have your proof. But that has length exponential in nmax. I’d be amazed if “1=2 is unprovable with length < nmax” were provable with length < nmax, which is pretty much the same statement. This is a very very strong statement. It can also be reformulated as “you cannot find a contradiction in the theory using less than nmax steps”.
This is awesome—great post!
I’ve scanned briefly through the comments, and didn’t see anyone ask this, but apologies if I missed it:
You use the diagonal lemma to establish that there is a piece of code called “box” such that the following is provable:
eval(box) == implies( proves(box, n1), eval(outputs(1)))
But couldn’t there likewise be a “box2” such that:
eval(box2) == implies( proves(box2, n1), eval(outputs(2)))
And then couldn’t you patch up the proof somehow to show that program has to output 2? Specifically, to get the analogue of step 2, can’t you prove that proves(outputs(2), n) implies the negation of proves(outputs(1), n), and hence prove that proves(outputs(2), n) implies outputs(2)?
Even if this is correct, it only applies to the program you use in your proof, where if proves(outputs(2), n) then 2 is returned; whereas the puzzle above doesn’t allow for 2 to be returned at all. However, if I’m right then presumably something must be going wrong in the proof?
To prove that, the proof system would need to know its own consistency, because an inconsistent proof system could prove both of these statements and indeed any statement at all. But a proof system cannot know its own consistency without actually being inconsistent (Goedel’s second theorem).
For a finite set of proofs, that a given statement is not provable by a proof from that set, is provable, possibly by a proof from that set.
Technically true. You could always just evaluate the two statements and there you have your proof, with length exponential in n. I very much doubt the proof could be made shorter than n though, because the statement is equivalent to “you can’t find a contradiction in these axioms using less than n steps”, the difficulty of which should grow way faster than linearly in n.
Good catch! Yes, my argument only shows that there’s no short easy proof. You can always just evaluate the two statements and there you have your proof. But that has length exponential in nmax. I’d be amazed if “1=2 is unprovable with length < nmax” were provable with length < nmax, which is pretty much the same statement. This is a very very strong statement. It can also be reformulated as “you cannot find a contradiction in the theory using less than nmax steps”.
Aha—very cunning.