= 27d567bc2d48d9f40e9ccc20ea370b15)
Oops, you're right. But how do you prove that every modal agent is defected against by at least one of FairBot and UnfairBot?
Proof: Let X be a modal agent, Phi(...) it's associated fully modalized formula, (K, R) a GL Kripke model and w minimal in K. Then, for all statement of the form ◻(...) we have w |- ◻(...) so Phi(...) reduce in w to a truth value which is independent of X opponent. As a result, we can't have both w |- X(FairBot) = C and w |- X(UnfairBot) = D and so we can't have both ◻(X(FairBot) = C) and ◻(X(UnfairBot) = D) and so we can't both have FairBot(X) = C and UnfairBot(X) = C. QED
trollDetector-a fundamental part of psychbot-gets both of these to cooperate.
TrollDetector tests opponents against DefectBot. If opponent defects, it cooperates. if opponent cooperates, TrollDetector defects.
So both UnfairBot and Fairbot cooperate with it, though it doesn't do so well against itself or DefectBot.
no modal agent can get both FairBot and UnfairBot to cooperate with it.
TrollDetector is not a modal agent.
As you have defined UnfairBot, both FairBot and UnfairBot cooperate with PrudentBot.
UnfairBot defect against PrudentBot.
Proof: For UnfairBot to cooperate with PrudentBot, PA would have to prove that PrudentBot defect against UnfairBot which would require PA to prove that "PA does not prove that UnfairBot cooperate with PrudentBot or PA+1 does not prove that UnfairBot defect against DefectBot" but that would require PA to prove it's own consistency which it cannot do. QED
In response to
Robust Cooperation in the Prisoner's Dilemma
Here is another obstacle to an optimality result: define UnfairBot as the agent which cooperate with X if and only if PA prove that X defect against UnfairBot, then no modal agent can get both FairBot and UnfairBot to cooperate with it.
In response to
Robust Cooperation in the Prisoner's Dilemma
I have two proposed alternatives to PrudentBot.
If you can prove a contradiction, defect. Otherwise, if you can prove that your choice will be the same as the opponent's, cooperate. Otherwise, defect.
If you can prove that, if you cooperate, the other agent will cooperate, and you can't prove that if you defect, the other agent will cooperate, then cooperate. Otherwise, defect.
Both of these are unexploitable, cooperate with themselves, and defect against CooperateBot, if my calculations are correct. The first one is a simple way of "sanitizing" NaiveBot.
The second one is exactly cousin_it's proposal here.
Both of those agents are modal agents of rank 0 and so the fact that they defect against CooperateBot imply that FairBot defects against them by theorem 4.1.
JusticeBot cooperates with anyone who cooperates with FairBot, and is exploitable by any agent which comprehends source code well enough to cooperate with FairBot and defect against JusticeBot. Though I'm going here off the remembered workshop rather than rechecking the paper.
You're right, and wubbles's agent can easily be exploited by a modal agent A defined by A(X)=C <-> [] (X(PB)=C) (where PB is PrudentBot).
Hm. I think X within the test could be introduced as a new constant and solved, but I'm not sure.
The agent defined by wubbles is actually the agent called JustBot in the robust cooperation paper and which is proven to be non-exploitable by modal agents.
In response to
comment
by
on
A problem with "playing chicken with the universe" as an approach to UDT
You're right, and I don't know how to fix the problem without adding the equivalent of "playing chicken". But now I wonder why the "playing chicken" step needs to consider the possible actions one at a time. Instead suppose that using an appropriate oracle, the agent looks through all theorems of PA, and returns action a as soon as it sees a theorem of the form A()≠a, for any a. This was my original interpretation of cousin_it's post. Does this have the same problem, if two otherwise identical agents look through the theorems of PA in different orders?
In response to
comment
by
on
A problem with "playing chicken with the universe" as an approach to UDT
Well, depend how different the order is...
If there are theorem in PA of the form "If there are theorems of the form A()≠a and of the form A'()≠a' then the a and the a' such that the corresponding theorem come first in the appropriate ordering must be identical." then you should be okay in the prisoner dilemma setting but otherwise there will be a model of PA in which the two players end up playing different actions and we end up in the same situation as in the post.
More generally, no matter how you try to cut it, there will always be a model of PA in which all theorems are provable and your agent behavior will always depend on what happen in that model because PA will never be able to prove anything which is false in that model.
Interesting. I think the other approach that cousin_it and Karl wrote about is more elegant (*) anyway, but cousin_it was dissatisfied with it because it involved an arbitrary time limit. Here's an idea for making it less arbitrary. Suppose instead of a halting oracle, we had an oracle for General Turing Machines that (in one cycle) outputs the final output of a given GTM if it converges. Then we can use it to look through all theorems of the form A()=a => U()>=u, and return the action with the highest u, or an error ("break down and cry") if no such action exists.
(*) More elegant because 1) it doesn't require the "play chicken" step and 2) it doesn't require that the set of possible actions be finite.
In response to
comment
by
on
A problem with "playing chicken with the universe" as an approach to UDT
If I understand what you're proposing correctly then that doesn't work either.
Suppose it is a theorem of PA that this algorithm return an error, then all theorems of the form A()=a => U()>=u are demonstrable in PA and so there is no action with the highest u and the algorithm return an error, because that is demonstrable in PA the algorithm must return an error by Löb's theorem.
= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
= f037147d6e6c911a85753b9abdedda8d){kind=logo}
I don't know what that means. Can you prove it without using Kripke semantics? (if that would complicate things enough to make it unpleasant to do so, don't worry about it; I believe you that you probably know what you're doing)
Proof without using Kripke semantic: Let X be a modal agent and Phi(...) it's associated fully modalized formula. Then if PA was inconsistent Phi(...) would reduce to a truth value independent of X opponent and so X would play the same move against both FairBot and UnfairBot (and this is provable in PA). But PA cannot prove it's own consistency so PA cannot both prove X(FairBot) = C and X(UnfairBot) = D and so we can't both have FairBot(X) = C and UnfairBot(X) = C. QED