= 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)
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.