Vladimir_Nesov comments on Controlling Constant Programs - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (33)
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?
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.