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?
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?