gRR comments on A model of UDT with a halting oracle - Less Wrong Discussion
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 (100)
I visualized the process like this: S would start proving things. It will notice that "if S does not prove A()!=a AND S does not prove A()!=b AND AgentStep2Proves("A()=a => U()=u") AND AgentStep2Proves("A()=b => U()=w") AND u>w THEN A()!=b", so it would prove A()!=b. Etc.
Which is wrong since it makes S look on itself, which would make it inconsistent. Except it is inconsistent anyway...
On the other hand, this method still does not let the agent prove its decision, since it would make the step 2 explode. Damn, I'm stupid :(
But this should work. It's just TDT, I think. Does it have serious drawbacks that make UDT/ADT desirable?