Hm. So what would you still need to win. You’d still need to prove that A()==1 implies U()==10^6. But if that’s true, the only way the agent doesn’t prove that A()==2 implies U()==10^6+10^3 is if the predictor is really always right. But that’s not provable to the agent, because I’m pretty sure that relies on the consistency of the agent’s formal system.
The ASP post already has a rigorous proof that this implementation of A will fail. But maybe we can find a different algorithm for A that would search for proofs of some other form, and succeed?
Hm. So what would you still need to win. You’d still need to prove that A()==1 implies U()==10^6. But if that’s true, the only way the agent doesn’t prove that A()==2 implies U()==10^6+10^3 is if the predictor is really always right. But that’s not provable to the agent, because I’m pretty sure that relies on the consistency of the agent’s formal system.
The ASP post already has a rigorous proof that this implementation of A will fail. But maybe we can find a different algorithm for A that would search for proofs of some other form, and succeed?