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, since the target theorem
implicitly also talks about all the other
*switchprog*s 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 *proof*s and *switchprog*s
until the systematic
searcher comes up with an even better *switchprog*.
Obviously the second alternative concerns all (possibly infinitely
many) potential *switchprog*s 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 consistency of the
underlying formal system. 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.

Back to Goedel machine home page