** Next:** Alternative Relaxed Target Theorem
** Up:** Global Optimality Theorem
** Previous:** Global Optimality Theorem

##

Globally Optimal Self-Changes, Given and Encoded in

**Theorem 4.1**
Given any formalizable utility function

(Item

1f),
and assuming consistency of the underlying formal system

,
any self-change of

obtained through execution of
some program

*switchprog* identified
through the proof of a target theorem (

2)
is globally optimal in the following sense:
the utility of starting the execution of the present

*switchprog* is higher than the utility of
waiting for the proof searcher
to produce an alternative

*switchprog* later.

**Proof.** Target theorem (2)
implicitly 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* (set *switchbit* ), or
(2) keep searching for *proof*s and *switchprog*s (set *switchbit* )
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 .
*Q.E.D.*

The initial proof searcher of Section 5
already generates all possible proofs and *switchprogs* in -optimal fashion.
Nevertheless, since it is part of , its proofs can speak about the
proof searcher itself, possibly triggering proof searcher rewrites
resulting in better than merely -optimal performance.

** Next:** Alternative Relaxed Target Theorem
** Up:** Global Optimality Theorem
** Previous:** Global Optimality Theorem
Juergen Schmidhuber
2005-01-03