A simple approach to 5-and-10

by Gurkenglas 9mo17th Dec 201810 comments

5


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!