= 27d567bc2d48d9f40e9ccc20ea370b15)
AlephNeil comments on AI cooperation in practice - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (157)
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.
Aha - very cunning.