Edit: The following is not obviously possible, see this comment.
This can be generalized to provide even better algorithms for more general games. Let the following be a simplified outline of the algorithm for cooperation problem, with bounds omitted (players are A and B, our player is A):
function main1() {
if (proves("A()==B()"))
return "Cooperate";
return "Defect";
}
The proof that the outcome is “Cooperate” basically hinges on the provability of Löb statement
proves("A()==B()") => (A()==B())
from which we conclude that A()==B() and so A()==”Cooperate”. The statement can be constructed from
Now, we can get basically the same proof if we use a simpler algorithm for the players:
function main2() {
if (proves("A()=="Cooperate" && B()=="Cooperate""))
return "Cooperate";
return "Defect";
}
This gets rid of the more general relation, but achieves basically the same result. We can improve on this by defecting against cooperating rocks:
function main3() {
if (proves("A()=="Defect" && B()=="Cooperate""))
return "Defect";
if (proves("A()=="Cooperate" && B()=="Cooperate""))
return "Cooperate";
return "Defect";
}
This suggests a general scheme for construction of decision-making algorithms: for all possible actions a and b of players A and B, sort the pairs by utility for A, starting from highest, and implement the Löb algorithm for each possibility in turn:
function main4() {
for(action pairs <a,b> in order of descending utility for A) {
if (proves("A()==a && B()==b"))
return a;
}
return something;
}
This plays against arbitrary opponents quite well.
function main3() {
if (proves("A()=="Defect" && B()=="Cooperate""))
return "Defect";
if (proves("A()=="Cooperate" && B()=="Cooperate""))
return "Cooperate";
return "Defect";
}
Sorry if I’m being naive, but if we amend the program that way then doesn’t it lose the ability to prove the Löb statement implies(proves(P), P) where P = “A()==‘Cooperate’ && B()==‘Cooperate’”? (Due to the unprovability of unprovability.)
Can this problem be solved by adjusting maximal length of checked proofs such that unprovability of proves(“A()==”Defect” && B()=”Cooperate”″, maxDC) is provable by proves(..., maxsteps)?
Yes, that occurred to me too, and I think it does the job.
I wonder if there are theorems of the form “There’s no significantly better way to show that P isn’t provable in N steps than by listing all proofs of length N and observing that P isn’t proved”. Then of course maxsteps would need to be exponential in maxDC.
On the other hand the fact that proves(“A()==”Cooperate” && B()==”Cooperate”″) was called means that A()==”Defect” && B()==”Cooperate” is unprovable under maxDC proof length. The question is can this fact be used in proof. The proof checker can be programmed to add such self-evident propositions into set of axioms, but I can’t clearly see consequences of this. And I have a bad feeling of mixing meta- and object levels.
I’m not sure if your idea will work, but have some notation to help you avoid mixing the levels. Here’s how you say “try to prove this fact conditional on some other fact”:
function main()
{
if (proves(outputs(1), n1))
return 1;
else if (proves("implies(!proves(outputs(1), n1), eval(outputs(2)))", n2))
return 2;
else
return 0;
}
OK, so first we try to prove P1 = “A()==”Defect” && B()==”Cooperate”“ using some theory T, then on failing that, we try to prove P2 = “A()==”Cooperate” && B()==”Cooperate”” using the augmented theory T’ = T + “T cannot prove P1 in maxDC steps”.
And then T’ can prove that “If T’ proves P2 then P2 is true”.
And note that the number of steps doesn’t matter any more.
“P isn’t provable in N steps” is in Co-NP. Since in general it’s an open question whether P=Co-NP, there might be a polynomial time algorithm to solve it, or their might not, respectively.
On the other hand, if you
1) Showed some large class of particular problems (ones that can reduced to from [no typo there] nonequivalent SAT instances, which I suspect is most of them) weren’t provable in N=cP steps IF it’s unprovable, then
2) You would have shown a sufficiently large class of SAT problems weren’t easily solvable in N=kP steps,
3) which would imply P!=NP (and also P!=Co-NP).
If on the other hand your whole class of problems is unprovable, then you can prove P isn’t provable by your theorem, which is presumably smaller than N in this context.
So, in summary my guess interesting classes of P, your question is equivalent to “Does P=NP?”, which we know is a tough nut to crack.
This is true, and it’s a bit disturbing that it took so long for someone to point that out. I feel that there should be a way out, but don’t see what it is (and finding it might suggest interesting limitations).
According to my experience, the study of game-playing programs has two independent components: fairness/bargaining and enforcement. If you have a good method of enforcement (quining, löbbing, Wei Dai’s joint construction), you can implement almost any concept of fairness. Even though Freaky Fairness relied on quining, I feel you can port it to löbbing easily enough. But fairness in games with non-transferable utility is so difficult that it should really be studied separately, without thinking of a specific enforcement mechanism.
Suppose we have two possible actions X,Y and A prefers to to to and B prefers to to to . What will be the outcome if both of them use main4() with their respective orderings and the same proves() function?
Edit: The following is not obviously possible, see this comment.
This can be generalized to provide even better algorithms for more general games. Let the following be a simplified outline of the algorithm for cooperation problem, with bounds omitted (players are A and B, our player is A):
The proof that the outcome is “Cooperate” basically hinges on the provability of Löb statement
from which we conclude that A()==B() and so A()==”Cooperate”. The statement can be constructed from
and so
Now, we can get basically the same proof if we use a simpler algorithm for the players:
This gets rid of the more general relation, but achieves basically the same result. We can improve on this by defecting against cooperating rocks:
This suggests a general scheme for construction of decision-making algorithms: for all possible actions a and b of players A and B, sort the pairs by utility for A, starting from highest, and implement the Löb algorithm for each possibility in turn:
This plays against arbitrary opponents quite well.
Sorry if I’m being naive, but if we amend the program that way then doesn’t it lose the ability to prove the Löb statement implies(proves(P), P) where P = “A()==‘Cooperate’ && B()==‘Cooperate’”? (Due to the unprovability of unprovability.)
Can this problem be solved by adjusting maximal length of checked proofs such that unprovability of proves(“A()==”Defect” && B()=”Cooperate”″, maxDC) is provable by proves(..., maxsteps)?
Yes, that occurred to me too, and I think it does the job.
I wonder if there are theorems of the form “There’s no significantly better way to show that P isn’t provable in N steps than by listing all proofs of length N and observing that P isn’t proved”. Then of course maxsteps would need to be exponential in maxDC.
On the other hand the fact that proves(“A()==”Cooperate” && B()==”Cooperate”″) was called means that A()==”Defect” && B()==”Cooperate” is unprovable under maxDC proof length. The question is can this fact be used in proof. The proof checker can be programmed to add such self-evident propositions into set of axioms, but I can’t clearly see consequences of this. And I have a bad feeling of mixing meta- and object levels.
I’m not sure if your idea will work, but have some notation to help you avoid mixing the levels. Here’s how you say “try to prove this fact conditional on some other fact”:
OK, so first we try to prove P1 = “A()==”Defect” && B()==”Cooperate”“ using some theory T, then on failing that, we try to prove P2 = “A()==”Cooperate” && B()==”Cooperate”” using the augmented theory T’ = T + “T cannot prove P1 in maxDC steps”.
And then T’ can prove that “If T’ proves P2 then P2 is true”.
And note that the number of steps doesn’t matter any more.
So perhaps Nesov’s idea was OK all along?
“P isn’t provable in N steps” is in Co-NP. Since in general it’s an open question whether P=Co-NP, there might be a polynomial time algorithm to solve it, or their might not, respectively.
On the other hand, if you 1) Showed some large class of particular problems (ones that can reduced to from [no typo there] nonequivalent SAT instances, which I suspect is most of them) weren’t provable in N=cP steps IF it’s unprovable, then 2) You would have shown a sufficiently large class of SAT problems weren’t easily solvable in N=kP steps, 3) which would imply P!=NP (and also P!=Co-NP).
If on the other hand your whole class of problems is unprovable, then you can prove P isn’t provable by your theorem, which is presumably smaller than N in this context.
So, in summary my guess interesting classes of P, your question is equivalent to “Does P=NP?”, which we know is a tough nut to crack.
This is true, and it’s a bit disturbing that it took so long for someone to point that out. I feel that there should be a way out, but don’t see what it is (and finding it might suggest interesting limitations).
According to my experience, the study of game-playing programs has two independent components: fairness/bargaining and enforcement. If you have a good method of enforcement (quining, löbbing, Wei Dai’s joint construction), you can implement almost any concept of fairness. Even though Freaky Fairness relied on quining, I feel you can port it to löbbing easily enough. But fairness in games with non-transferable utility is so difficult that it should really be studied separately, without thinking of a specific enforcement mechanism.
Bargaining is about logical uncertainty, something we avoid using sufficiently high upper bounds in this post.
Suppose we have two possible actions X,Y and A prefers to to to and B prefers to to to . What will be the outcome if both of them use main4() with their respective orderings and the same proves() function?
Probably , which is not quite optimal. This doesn’t solve the bargaining problem, which is exactly what your example is.
Most likely , but possibly or if one of the agents manages to “trick” the other.
Your idea is similar to preferential voting.