Vladimir_Nesov comments on What a reduction of "could" could look like - Less Wrong

53 Post author: cousin_it 12 August 2010 05:41PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Comments (103)

Comments (103)

You are viewing a single comment's thread. Show more comments above.

Comment author: Vladimir_Nesov 14 August 2010 05:05:37PM 0 points [-]

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).

Comment author: Benja 14 August 2010 05:52:22PM 0 points [-]

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.

Powered by Reddit Powered by Reddit