In this comment the mistake is thinking that "the best b found in step 1" is indeed the best b for the given problem. For example, in the problem given in the post, B could find a correct proof that B()=1 implies U()=5 and a spurious proof that B()=2 implies U()=0. Then B will go on to return 1, thus making the spurious proof also correct because its premise is false.

Ah, I think I get it. By returning 1, B makes B()=2 false, and therefore it can no longer proof anything about the cases where it would have returned 2. In essence, counter-factual reasoning becomes impossible.

However, these problems only happen if B does not find a proof of "B()=2 implies U()=10". If it does find such a proof then it would correctly return 2. This reminds me of bounded rationality. If B searches for all proofs up to some length L, then for large enough L it will also find the non-spurious ones.

Counter-factuals were my reason for writing U=U'(A). By allowing the argument to U' to be different from A you can examine counter-factual cases. But perhaps then you end up with just CDT.