The next question I have is whether this non-optimality result holds if the universes are using PA+100 rather than PA. The proof in that post no longer goes through (the expression □¬□⊥ becomes □100¬□⊥, which is of course a tautology). So is there a modal agent which wins at both of those universes?
Never mind, that’s trivial, you can win at that decision problem via the agent that does one thing if its proof search succeeds and another if its proof search fails.
To generalize, though, if there are N different actions, and for each action there’s a decision problem which rewards you iff PA+M proves you take that action, then I think that there exists a decision theory which wins at all of them iff M≥N−1. (I think you can inductively prove that the number of possible actions a decision theory can take if PA+m is inconsistent is ≤m+1.)
The next question I have is whether this non-optimality result holds if the universes are using PA+100 rather than PA. The proof in that post no longer goes through (the expression □¬□⊥ becomes □100¬□⊥, which is of course a tautology). So is there a modal agent which wins at both of those universes?
Never mind, that’s trivial, you can win at that decision problem via the agent that does one thing if its proof search succeeds and another if its proof search fails.
To generalize, though, if there are N different actions, and for each action there’s a decision problem which rewards you iff PA+M proves you take that action, then I think that there exists a decision theory which wins at all of them iff M≥N−1. (I think you can inductively prove that the number of possible actions a decision theory can take if PA+m is inconsistent is ≤m+1.)