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.
Right! More generally, I claim that if a modal agent provably cooperates (in PA) against some other agent, then it cannot provably defect (in PA) against any other agent: roughly speaking, PA can never prove that any proof search in PA or higher fails, so a modal agent can only provably (in PA) do the action that it would do if PA were inconsistent.
hm. I’m still a bit shaky on the definition of modal agent...does the following qualify?
IF(opponentcooperates with me AND I defect is a possible outcome){defect}
else{ if (opponent cooperates IFF i cooperate) (cooperate){else defect}
(edit: my comment about perfect unfair bots may have been based on the wrong generalizations from an infinite-case).
addendum: if what I’ve got doesn’t qualify as a model agent I’ll shut up until I understand enough to inspect the proof directly.
What do you even mean by “is a possible outcome” here? Do you mean that there is no proof in PA of the negation of the proposition?
The formula of a modal agent must be fully modalized, which means that all propositions containing references to actions of agents within the formula must be within the scope of a provability operator.
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
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
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
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.
Right! More generally, I claim that if a modal agent provably cooperates (in PA) against some other agent, then it cannot provably defect (in PA) against any other agent: roughly speaking, PA can never prove that any proof search in PA or higher fails, so a modal agent can only provably (in PA) do the action that it would do if PA were inconsistent.
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.
TrollDetector is not a modal agent.
hm. I’m still a bit shaky on the definition of modal agent...does the following qualify?
IF(opponentcooperates with me AND I defect is a possible outcome){defect} else{ if (opponent cooperates IFF i cooperate) (cooperate){else defect}
(edit: my comment about perfect unfair bots may have been based on the wrong generalizations from an infinite-case). addendum: if what I’ve got doesn’t qualify as a model agent I’ll shut up until I understand enough to inspect the proof directly.
addendum 2: well. alright then I’ll shut up.
What do you even mean by “is a possible outcome” here? Do you mean that there is no proof in PA of the negation of the proposition?
The formula of a modal agent must be fully modalized, which means that all propositions containing references to actions of agents within the formula must be within the scope of a provability operator.
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
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
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
Oh, I see. Thanks.