** Next:** Bias-Optimal Proof Search (BIOPS)
** Up:** Global Optimality Theorem
** Previous:** Global Optimality and Recursive

##

How Difficult is it to Prove Target Theorems?

This depends on the tasks and the initial axioms , of course.
It is straight-forward to devise simple tasks and
corresponding consistent
such that there are short and trivial proofs of target theorems.
On the other hand, it is possible to construct
set-ups where it is impossible to prove target theorems,
for example, by using results of undecidability theory,
e.g., [32,3,4].
The point is: usually we do not know in advance whether it is
possible or not to change a given initial problem solver
in a provably good way. The traditional approach is to
invest human research effort into finding out. A Gödel machine, however, can
do this by itself, without essential limits
apart from those of computability and provability.

Note that to prove a target theorem,
a proof technique does not necessarily have to compute
the true expected utilities of switching and not
switching--it just needs to determine which is higher.
For example, it may be easy to prove that
speeding up a subroutine of the proof searcher
by a factor of 2 will certainly be worth
the negligible (compared to lifetime ) time needed to
execute the subroutine-changing algorithm, no matter
what is the precise utility of the switch.

** Next:** Bias-Optimal Proof Search (BIOPS)
** Up:** Global Optimality Theorem
** Previous:** Global Optimality and Recursive
Juergen Schmidhuber
2005-01-03