Solovay’s theorem is so significant because it shows that an interesting fragment of an undecidable formal theory like Peano Arithmetic—namely that which arithmetic can express in propositional terms about its own provability predicate—can be studied by means of a decidable modal logic, GL, with a perspicuous possible worlds semantics.
The post I linked is based on GL.
In your scenario with two reasoners, I think they will be unpredictable to each other, and both will fail to find enough counterfactuals to choose an action. Modal UDT is single player only.
More generally I think single player decision theory will never make game theory fall out for free—that dream should be abandoned. But that’s a different conversation.
Consider “B := Have A’ give you a source code X, then execute X.” in modal combat. (Where f may be partial.) Pit B against itself. (D,C) and (C,D) are impossible by symmetry, so assuming our proof system is sound the pointwise maximum of all f will be at most the utility of (C,C). This can be reached by returning “Cooperate”.
Pitting B against FairBot or PrudentBot, they shouldn’t be able to prove B won’t prove he can gain more from defecting, unless they assume B’s consistency, in which case they should cooperate.
I can see B failing to establish corporation with itself when symmetry arguments are barred somehow. Perhaps it could work if B had a probability distribution over what PA+n it expects to be consistent...
Game theory also gives no answer to that problem. That said, I see hope that each could prove something like “We are symmetric enough that if I precommit to take no more than 60% by my measure, he will have precommited to take no more than at most 80% by my measure. Therefore, by precommiting to take no more than 60%, I can know to get at least 20%.”.
Sorry about the late reply, I’m on vacation and not using the internet much. By have heart I meant stay strong. By decidability I meant this:
https://plato.stanford.edu/entries/logic-provability/#AritComp
The post I linked is based on GL.
In your scenario with two reasoners, I think they will be unpredictable to each other, and both will fail to find enough counterfactuals to choose an action. Modal UDT is single player only.
More generally I think single player decision theory will never make game theory fall out for free—that dream should be abandoned. But that’s a different conversation.
https://arxiv.org/abs/1401.5577 makes me think single player decision theory should be enough.
Consider “B := Have A’ give you a source code X, then execute X.” in modal combat. (Where f may be partial.) Pit B against itself. (D,C) and (C,D) are impossible by symmetry, so assuming our proof system is sound the pointwise maximum of all f will be at most the utility of (C,C). This can be reached by returning “Cooperate”.
Pitting B against FairBot or PrudentBot, they shouldn’t be able to prove B won’t prove he can gain more from defecting, unless they assume B’s consistency, in which case they should cooperate.
I can see B failing to establish corporation with itself when symmetry arguments are barred somehow. Perhaps it could work if B had a probability distribution over what PA+n it expects to be consistent...
For the glider vs honeycomb maximizer, I think the problem is agreeing on what division of the universe counts as (C,C).
Game theory also gives no answer to that problem. That said, I see hope that each could prove something like “We are symmetric enough that if I precommit to take no more than 60% by my measure, he will have precommited to take no more than at most 80% by my measure. Therefore, by precommiting to take no more than 60%, I can know to get at least 20%.”.