gRR comments on Controlling Constant Programs - Less Wrong

25 Post author: Vladimir_Nesov 05 September 2010 01:45PM

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

Comments (33)

You are viewing a single comment's thread.

Comment author: gRR 18 February 2012 07:14:59PM 0 points [-]

Let's say the agent proves two statements implying different consequences of the same action, such as [agent()==2 => world2()==1000] and
[agent()==2 => world2()==2000].
Then, it can also prove that (agent()==2) implies a contradiction, which normally can't happen

Why not? (X implies a contradiction) implies (NOT X), it's a standard reductio-ad-absurdum proof technique (= derived rule of propositional calculus). Or do I miss something here?

Comment author: Vladimir_Nesov 18 February 2012 07:31:23PM *  0 points [-]

It does mean that [agent()==2] is false, but that allows proving statements like [agent()==2 => world2()==U] for any value of U, which breaks our algorithm. If we use Goedel diagonal (chicken) rule of performing an action whenever it's proven that this action won't be performed, that guarantees that an action can never be proven to be impossible, unless the reasoning system is compromised.