Suppose there’s a short proof that agent1()==”C” iff agent2()==”cooperate”. [...] Therefore, under the supposition, agent1 will choose “C”; similarly, agent2 will choose “cooperate”.
Sounds right (but it’s a rather strong supposition).
Sorry, I wasn’t being as clear as I should have been:
The above is true as a metatheorem, but uninteresting, because as you say, the supposition is rather strong.
What I was trying to argue is that in the agent’s proof system (for concreteness, say PA), when assuming the supposition, the conclusion follows, so by the deduction theorem, PA proves “the supposition implies the conclusion”. I wanted to use this for a proof-size-bounded Löbian argument à la cousin_it.
But this does not work because in PA, the conclusion does not follow when assuming the supposition, as pointed out by cousin_it.
Sounds right (but it’s a rather strong supposition).
Sorry, I wasn’t being as clear as I should have been:
The above is true as a metatheorem, but uninteresting, because as you say, the supposition is rather strong.
What I was trying to argue is that in the agent’s proof system (for concreteness, say PA), when assuming the supposition, the conclusion follows, so by the deduction theorem, PA proves “the supposition implies the conclusion”. I wanted to use this for a proof-size-bounded Löbian argument à la cousin_it.
But this does not work because in PA, the conclusion does not follow when assuming the supposition, as pointed out by cousin_it.