The current problem is that even though it can prove that DefectBot defects
How can it do that in the general case?
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.
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?
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.
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.
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.
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.