If there are theorem in PA of the form “If there are theorems of the form A()≠a and of the form A’()≠a’ then the a and the a’ such that the corresponding theorem come first in the appropriate ordering must be identical.” then you should be okay in the prisoner dilemma setting but otherwise there will be a model of PA in which the two players end up playing different actions and we end up in the same situation as in the post.
More generally, no matter how you try to cut it, there will always be a model of PA in which all theorems are provable and your agent behavior will always depend on what happen in that model because PA will never be able to prove anything which is false in that model.
Well, depend how different the order is...
If there are theorem in PA of the form “If there are theorems of the form A()≠a and of the form A’()≠a’ then the a and the a’ such that the corresponding theorem come first in the appropriate ordering must be identical.” then you should be okay in the prisoner dilemma setting but otherwise there will be a model of PA in which the two players end up playing different actions and we end up in the same situation as in the post.
More generally, no matter how you try to cut it, there will always be a model of PA in which all theorems are provable and your agent behavior will always depend on what happen in that model because PA will never be able to prove anything which is false in that model.