It turns out that, even within the class of modal agents, it’s hard to formulate a definition of optimality that’s actually true of something, and which meaningfully corresponds to our intuitions about the “right” decisions on decision-theoretic problems. (This intuition is not formally defined, so I’m using scare quotes.)
This seems too simple, but why can’t PrudentBot search for a proof that (X(PrudentBot) = C and PrudentBot(X) = D) and defect if a proof is found. If no proof is found, search for the proof of (X(PrudentBot) = C) as before.
That agent gets (mutual) defection from FairBot, since it can never be proven in PA that it cooperates. (In order to do so, you’d need to show that the search for your first statement fails; it’s not enough to show there is a proof in PA of an incompatible statement, because PA doesn’t know that PA is consistent.)
Variants on that could end up cooperating with versions of FairBot that use PA+Con(PA) instead of just PA, of course. But this is a good illustration of just what’s so tricky about modal agents.
That agent gets (mutual) defection from FairBot, since it can never be proven in PA that it cooperates. (In order to do so, you’d need to show that the search for your first statement fails; it’s not enough to show there is a proof in PA of an incompatible statement, because PA doesn’t know that PA is consistent.)
What if PrudentBot searches for sufficiently short proofs of (PrudentBot(X) = D and X(PrudentBot) = C)? There may be a constructive proof in PA that (there does not exist a proof in PA of length N or shorter that (PrudentBot(X) = D) and X(PrudentBot) = C). If so, as long as FairBot searches for long-enough proofs in PA of (X(PrudentBot) = C) it can first prove that (there does not exist a proof in PA of length N or shorter that (PrudentBot(X) = D) and X(PrudentBot) = C) and subsequently that (PrudentBot(X) = C) and so decide to cooperate. If N is also large enough that PrudentBot can find a proof in PA that (PrudentBot(CooperateBot) = D and CooperateBot(PrudentBot) = C) then I think it can do everything the original PrudentBot did in PA+Con(PA) in a generic way.
There’s a hierarchy for existence of short proofs similar to the hierarchy for existence of proofs in this tower of formal systems. (If there weren’t, then these agents wouldn’t be much discussing! As it is, though, there are bounded algorithmic analogues of all these modal agents.) However, proving properties of such algorithms gets a lot trickier there, as you need to keep track of how long it takes to make all the trivial deductions in addition to Lobian ones.
Essentially, what you’re suggesting is something like an algorithmic analogue of the modal agent you considered before: searching for short proofs of exploitability, then longer proofs of mutual cooperation, is akin to searching for exploitability in a lower formal system and then mutual cooperation in a higher one. Not a bad idea! But when we transfer it to the easier-to-work-with context, it’s clear that waiting for a proof search to terminate must cost you against anything cooperative but impatient/low-powered. (Explicitly, the algorithm you suggested can never cooperate with an agent that only looks for proofs of cooperation up to length N.)
One last thing: all proofs in PA of the form “there does not exist a proof in PA of X with length less than N” must have length at least N, for analogous reasons to the fact that PA cannot prove its own consistency.
Essentially, what you’re suggesting is something like an algorithmic analogue of the modal agent you considered before: searching for short proofs of exploitability, then longer proofs of mutual cooperation, is akin to searching for exploitability in a lower formal system and then mutual cooperation in a higher one. Not a bad idea! But when we transfer it to the easier-to-work-with context, it’s clear that waiting for a proof search to terminate must cost you against anything cooperative but impatient/low-powered. (Explicitly, the algorithm you suggested can never cooperate with an agent that only looks for proofs of cooperation up to length N.)
What about optimizing proof search order? An extreme example would just be an agent with a lookup table indexed by the Goedel number of each possible agent up to a maximum value of some N, with either Defect or Cooperate in the lookup table which is the action the agent will take. If impatient agents came first in the lookup table they could quickly prove cooperation. The agent could append its quine to the end of the lookup table before searching in order to cooperate with itself. There should be an optimal lookup table for any length N and set S of games against other agents, defined as the lookup table that generates the highest score when playing all the games in set S.
Instead of including the lookup table the agent could perform the same sort of proof search necessary to generate the lookup table at runtime. If it searched for proofs in roughly the same order as the corresponding entries in the lookup table then impatient opposing agents would conveniently find a cooperation proof early in the simulation of the agent. In this case there would be an optimal list of rules for proof search order (perhaps including direct proofs for the most likely impatient opposing agents) that would approach the optimality of the lookup table, or perhaps exceed it if enough opposing agents give up when they see the size of the lookup-table-agent.
I have no idea if any of this is theoretically interesting or just a hack to potentially play PD slightly better.
One last thing: all proofs in PA of the form “there does not exist a proof in PA of X with length less than N” must have length at least N, for analogous reasons to the fact that PA cannot prove its own consistency.
And presumably more like O(2^N) in practice? I don’t know what percentage of bit strings are well formed formulas in an average formal language, but I would imagine it’s a significant fraction. The proof searcher would have to check every wff to completion because it doesn’t have Con(PA) to rule out contradictions, and I assumed that most of the proofs would be of the form “First the agent writes a 0 and moves the read-head right and goes to state 5, … , then the agent halts in a Cooperating state”, so N would probably be very large.
This seems too simple, but why can’t PrudentBot search for a proof that (X(PrudentBot) = C and PrudentBot(X) = D) and defect if a proof is found. If no proof is found, search for the proof of (X(PrudentBot) = C) as before.
That agent gets (mutual) defection from FairBot, since it can never be proven in PA that it cooperates. (In order to do so, you’d need to show that the search for your first statement fails; it’s not enough to show there is a proof in PA of an incompatible statement, because PA doesn’t know that PA is consistent.)
Variants on that could end up cooperating with versions of FairBot that use PA+Con(PA) instead of just PA, of course. But this is a good illustration of just what’s so tricky about modal agents.
What if PrudentBot searches for sufficiently short proofs of (PrudentBot(X) = D and X(PrudentBot) = C)? There may be a constructive proof in PA that (there does not exist a proof in PA of length N or shorter that (PrudentBot(X) = D) and X(PrudentBot) = C). If so, as long as FairBot searches for long-enough proofs in PA of (X(PrudentBot) = C) it can first prove that (there does not exist a proof in PA of length N or shorter that (PrudentBot(X) = D) and X(PrudentBot) = C) and subsequently that (PrudentBot(X) = C) and so decide to cooperate. If N is also large enough that PrudentBot can find a proof in PA that (PrudentBot(CooperateBot) = D and CooperateBot(PrudentBot) = C) then I think it can do everything the original PrudentBot did in PA+Con(PA) in a generic way.
There’s a hierarchy for existence of short proofs similar to the hierarchy for existence of proofs in this tower of formal systems. (If there weren’t, then these agents wouldn’t be much discussing! As it is, though, there are bounded algorithmic analogues of all these modal agents.) However, proving properties of such algorithms gets a lot trickier there, as you need to keep track of how long it takes to make all the trivial deductions in addition to Lobian ones.
Essentially, what you’re suggesting is something like an algorithmic analogue of the modal agent you considered before: searching for short proofs of exploitability, then longer proofs of mutual cooperation, is akin to searching for exploitability in a lower formal system and then mutual cooperation in a higher one. Not a bad idea! But when we transfer it to the easier-to-work-with context, it’s clear that waiting for a proof search to terminate must cost you against anything cooperative but impatient/low-powered. (Explicitly, the algorithm you suggested can never cooperate with an agent that only looks for proofs of cooperation up to length N.)
One last thing: all proofs in PA of the form “there does not exist a proof in PA of X with length less than N” must have length at least N, for analogous reasons to the fact that PA cannot prove its own consistency.
What about optimizing proof search order? An extreme example would just be an agent with a lookup table indexed by the Goedel number of each possible agent up to a maximum value of some N, with either Defect or Cooperate in the lookup table which is the action the agent will take. If impatient agents came first in the lookup table they could quickly prove cooperation. The agent could append its quine to the end of the lookup table before searching in order to cooperate with itself. There should be an optimal lookup table for any length N and set S of games against other agents, defined as the lookup table that generates the highest score when playing all the games in set S.
Instead of including the lookup table the agent could perform the same sort of proof search necessary to generate the lookup table at runtime. If it searched for proofs in roughly the same order as the corresponding entries in the lookup table then impatient opposing agents would conveniently find a cooperation proof early in the simulation of the agent. In this case there would be an optimal list of rules for proof search order (perhaps including direct proofs for the most likely impatient opposing agents) that would approach the optimality of the lookup table, or perhaps exceed it if enough opposing agents give up when they see the size of the lookup-table-agent.
I have no idea if any of this is theoretically interesting or just a hack to potentially play PD slightly better.
And presumably more like O(2^N) in practice? I don’t know what percentage of bit strings are well formed formulas in an average formal language, but I would imagine it’s a significant fraction. The proof searcher would have to check every wff to completion because it doesn’t have Con(PA) to rule out contradictions, and I assumed that most of the proofs would be of the form “First the agent writes a 0 and moves the read-head right and goes to state 5, … , then the agent halts in a Cooperating state”, so N would probably be very large.