To recap, A is trying to deduce enough about U to maximize it:
A := Find some f with a proof of “U = f(A)”, then return argmax f.
If U is A, A can fail by proving f = {(5,5),(10,0)}: If it could prove this, it would be true, for only 5 is checked. Then by Löb’s theorem, it can prove this.
I’ve thrown this problem at some people in my university and a fellow student’s idea led to:
A’ := Find all f with a proof of “U = f(A’)”, then return argmax (their pointwise maximum).
The true f is among the found f. Fooling ourselves into a suboptimal action would require us to believe it at least as good as the true maximum, which the single check refutes.
Note that A’ can’t prove that some f is not found, due to Gödel. Therefore, it can never prove what it is going to do!
A simple approach to 5-and-10
To recap, A is trying to deduce enough about U to maximize it:
A := Find some f with a proof of “U = f(A)”, then return argmax f.
If U is A, A can fail by proving f = {(5,5),(10,0)}: If it could prove this, it would be true, for only 5 is checked. Then by Löb’s theorem, it can prove this.
I’ve thrown this problem at some people in my university and a fellow student’s idea led to:
A’ := Find all f with a proof of “U = f(A’)”, then return argmax (their pointwise maximum).
The true f is among the found f. Fooling ourselves into a suboptimal action would require us to believe it at least as good as the true maximum, which the single check refutes.
Note that A’ can’t prove that some f is not found, due to Gödel. Therefore, it can never prove what it is going to do!