Hmm, that’s pretty cool, thanks! But it’s still not obvious to me that it solves the same problem as the algorithm in the post. There are probably many mutually incompatible implementations of ChecksOut, because there are many ways to diagonalize that differ only syntactically. Do you have an argument why they will end up cooperating with each other? It seems to me that they won’t, just like different implementations of quining cooperation.
Hmm, yes, you’re right, it’s quining cooperation all over again—as defined, the programs would only cooperate with opponents that are sufficiently similar syntactically. And they need compatible proof systems in any case. So it’s not a solution to the same problem, only a possible optimization.
Hmm, that’s pretty cool, thanks! But it’s still not obvious to me that it solves the same problem as the algorithm in the post. There are probably many mutually incompatible implementations of ChecksOut, because there are many ways to diagonalize that differ only syntactically. Do you have an argument why they will end up cooperating with each other? It seems to me that they won’t, just like different implementations of quining cooperation.
Hmm, yes, you’re right, it’s quining cooperation all over again—as defined, the programs would only cooperate with opponents that are sufficiently similar syntactically. And they need compatible proof systems in any case. So it’s not a solution to the same problem, only a possible optimization.