Intuitively, at any given time the Gödel machine should execute some self-modification algorithm only if it is the `best' of all possible self-modifications, given the optimality criterion, which typically depends on available resources, such as storage size and remaining lifetime. At first glance, however, target theorem (2) seems to implicitly talk about just one single modification algorithm, namely, switchprog as set by the systematic proof searcher at time . Isn't this type of local search greedy? Couldn't it lead to a local optimum instead of a global one? No, it cannot, according to the global optimality theorem:
Proof. The target theorem (2) implicitly talks about all the other switchprogs that the proof searcher could produce in the future. To see this, consider the two alternatives of the binary decision: (1) either execute the current switchprog, or (2) keep searching for proofs and switchprogs until the systematic searcher comes up with an even better switchprog. Obviously the second alternative concerns all (possibly infinitely many) potential switchprogs to be considered later. That is, if the current switchprog were not the `best', then the proof searcher would not be able to prove that setting switchbit and executing switchprog will cause higher expected reward than discarding switchprog, assuming axiomatic consistency.
That is, only if it is provable that the current proof searcher cannot be expected to find sufficiently quickly an even better switchprog, will it also be provable that the current switchprog should be executed. So the trick is to let the formalized improvement criterion take into account the (expected) performance of the original search method, which automatically enforces globally optimal self-changes, relative to the provability restrictions.
Will the Gödel machine ever prove a target theorem? This obviously depends on the nature of environment and utility function. See Section 3.1 for intuitive examples of very simple, limited self-rewrites (affecting only near-future rewards) whose benefits should be easily provable, given appropriate axioms, and compare Section 3.4 on fundamental limitations of the Gödel machine.