In my formulation of ASP, the predictor has a stronger formal system than the agent, so some statements can have short proofs in the predictor’s formal system but only long proofs in the agent’s formal system. An extreme example is consistency of the agent’s formal system, which is unprovable by the agent but an axiom for the predictor.
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?
In my formulation of ASP, the predictor has a stronger formal system than the agent, so some statements can have short proofs in the predictor’s formal system but only long proofs in the agent’s formal system. An extreme example is consistency of the agent’s formal system, which is unprovable by the agent but an axiom for the predictor.
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?