= 27d567bc2d48d9f40e9ccc20ea370b15)
orthonormal 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)
You could make f(1) large enough for Loebian cooperation to happen immediately. Then you could make f(2) large enough to simulate what happened in the first f(1)+1 steps, and so on. I still don't completely understand how you're going to use this thing, though.
Lemma 1: There's a proof that M'(DefectBot)=D, and that there does not exist a shorter proof of M'(DefectBot)=C.
Proof: There's a short proof that DefectBot(DefectBot)=D, and a proof of length (waiting time + short) that FB'(DefectBot)=DefectBot(FB')=D. (It needs to wait until FB' stops looking for only cooperative proofs.) Clearly there are no shorter proofs of contrary statements.
So there's a proof that M' skips to its default defection (since there's nothing strictly better), and this proof has length less than (g(short) + g(wait + short) + short), where g is the function that bounds how long it takes to verify that something is the shortest proof of a certain type, in terms of the proof length. (I think g is just bounded by an exponential, but it doesn't matter).
Thus, of course, Lemma 1 has a proof of length at most g(g(short) + g(wait + short) + short).
Lemma 2: There's a proof that M'(FB')=FB'(M')=C, and that there does not exist a shorter proof of any alternative outcome.
Proof: Similar to Lemma 1. The initial proofs are a bit longer because we need the Löbian proof of length less than (waiting time) that FB'(FB')=C, instead of the short proof that DefectBot(DefectBot)=D.
And so there's a proof of length (g(wait+short) + g(wait) + short) that M' goes to the sanity-check trying to prove that FB'(M')=FB'(FB'). Now a proof of length L that FB'(M')=C would imply a proof of length L + (g(wait+short) + g(wait) + 2*short) that M'(FB')=C...
Oh, and here's the impasse again, because the existence of a proof that M'(FB')=C is no longer enough to prove that FB'(M')=C, you also need that there's no shorter proof that M'(FB')=D. Unless there's a clever way to finesse that (within something provable by the same system), it looks like that's where this last-ditch fix fails.
Drat.