Wei Dai comments on Decision Theories, Part 3.75: Hang On, I Think This Works After All

[Wei Dai]

given a payoff matrix in general, Masquerade enumerates all of the constant strategies and all of the “mutually beneficial deals” of the FairBot form

But here, you didn’t enumerates all of the constant strategies. To do that, we would change “for Y in [DefectBot, FairBot]” to “for Y in [DefectBot, CooperateBot, FairBot]”. Then Masquerade(CB)=D and Masquerade(Masquerade)=D because when it gets to “if utility > U(D,D)” it will be the case that my_move=D and their_move=C. Correct?

[orthonormal]

It’s the other way around: if we include CooperateBot among the options, Masquerade looks at playing CooperateBot against the other Masquerade, and sees that this would be the worst of its options. It sticks with FairBot.

The only reason I didn’t include CooperateBot in the proofs above is that it would make me write several more easy lemmas (and make everyone read them).

[Wei Dai]

Ah, ok. Another question: what happens if the other Masquerade is using a different proof system, like ZFC for example?

[orthonormal]

That’s a really interesting question; I don’t know. At the very least, what’s needed is for both agents to be using hierarchies of proof attempts such that the later attempts of one can answer questions about the early attempts of the other, and vice versa. Maybe some Löbian cycle still works if this is the case, or maybe they really do need to be using equivalent deductive systems at some point.

[Wei Dai]

Let me ask a simpler question. Does the following FB1 cooperate with FB2?

def FB1(X):
- if "X(FB1)=C" is provable in PA+1:
- - return C
- else return D

where FB2 is FB1 with “PA+2” in place of “PA+1″. I think the answer is yes, because PA+1 can prove

1. “FB1(FB2)=C” is provable in PA+1 implies “FB1(FB2)=C” is provable in PA+2

2. “FB1(FB2)=C” is provable in PA+1 implies FB2(FB1)=C (using 1 and looking at FB2)

3. “FB2(FB1)=C” is provable in PA+1 implies FB1(FB2)=C (looking at FB1)

4. FB2(FB1)=C (Löbian cycle)

Does this look right? And I think FB1 would also cooperate with FB-ZFC (FB1 with ZFC in place of PA+1), because PA+1 can prove that ZFC proves a superset of theorems of PA+1?

[orthonormal]

I think that’s right, yes. If one proof system encompasses the other, it looks like it works.

Another question is, what if we had two proof systems, neither of which encompasses the other? (Most horrifyingly, what if one were PA plus the Gödel sentence of PA, and the other were PA plus the negation of the Gödel sentence?)

[Wei Dai]

Another question is, what if we had two proof systems, neither of which encompasses the other? (Most horrifyingly, what if one were PA plus the Gödel sentence of PA, and the other were PA plus the negation of the Gödel sentence?)

I think that works too. Call these proof systems PA+ and PA- and the FairBots using them FB+ and FB-. PA can prove that any theorem of PA is also a theorem of PA+ and PA-. So PA can prove:

1. “FB+(FB-)=C” is provable in PA implies “FB+(FB-)=C” is provable in PA-

2. “FB+(FB-)=C” is provable in PA implies FB-(FB+)=C (using 1 and looking at FB-)

and similarly for the other half of the Löbian circle. So FB+(FB-)=C and FB-(FB+)=C are theorems of PA and hence theorems of PA- and PA+.