= 27d567bc2d48d9f40e9ccc20ea370b15)
V_V comments on Decision Theories, Part 3.5: Halt, Melt and Catch Fire - 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 (34)
So there's one last fix that occurred to me overnight, but I can't see whether it could possibly work.
The impasse is that we need a version of FairBot which acts as usual (given enough deductive capacity) AND is able to deduce that it defects mutually against DefectBot. The current problem is that even though it can prove that DefectBot defects, this isn't enough to prove that FairBot won't find a proof of DefectBot's cooperation anyway. (FairBot can't deduce that FairBot's deduction procedure is consistent, unless it's inconsistent!)
A failed fix is a FairBot that simultaneously looks for proofs of the opponent's cooperation and defection, and acts symmetrically as soon as it finds one (and defects if it doesn't). The problem is that this algorithm may as easily find a proof of mutual defection against itself as a proof of mutual cooperation; it depends on the proof ordering.
So the last-ditch fix is for FairBot to search for both proofs simultaneously, but somehow search more effectively in the cooperative direction, so that we can guarantee it finds a cooperative proof against itself rather than a defective one. This could be done either by giving it exponentially more search time in the cooperative direction than in the defective direction, or by preparing it with a Löbian constructive approach in the cooperative direction.
Do either of these seem feasible?
How can it do that in the general case?
Maybe I'm missing something, but wouldn't that imply that the formal system is inconsistent, and hence useless due to the principle of explosion?
If program A which uses a specific proof ordering can find a proof of some theorem about program A, and program B which uses a different proof ordering can find a proof of the opposite theorem about program B, that doesn't imply inconsistency.
Hence he's assuming that A = B, if I understand correctly.
He's saying that program A can find a proof that it cooperates with program A, but if we slightly change the proof ordering in program A and obtain program B, then program B can find a proof that it defects against program B. I still don't see the inconsistency.
Yes, this is what I meant. Thanks!
Ok, so the proof ordering is considered part of the program, I assumed it was an external input to be universally quantified. Thanks for the clarification.