cousin_it comments on Decision Theories, Part 3.5: Halt, Melt and Catch Fire - Less Wrong

31 Post author: orthonormal 26 August 2012 10:40PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (34)

You are viewing a single comment's thread. Show more comments above.

Comment author: cousin_it 28 August 2012 12:41:27PM *  2 points [-]

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.

Comment author: V_V 28 August 2012 01:06:26PM 0 points [-]

proof of mutual defection against itself (emphasis mine)

Hence he's assuming that A = B, if I understand correctly.

Comment author: cousin_it 28 August 2012 01:19:12PM *  2 points [-]

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.

Comment author: orthonormal 28 August 2012 04:12:05PM 0 points [-]

Yes, this is what I meant. Thanks!

Comment author: V_V 28 August 2012 02:54:48PM 0 points [-]

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.