Introduction

In 1931 Kurt Gödel used
elementary arithmetics to build a universal programming language
for encoding arbitrary proofs, given an arbitrary enumerable set of
axioms. He went on to construct *self-referential* formal statements that claim their own unprovability,
using Cantor's diagonalization trick [5]
to demonstrate that formal systems such as
traditional mathematics are either flawed in a certain
sense or contain unprovable but true statements [10].

Since Gödel's exhibition of the fundamental limits of proof and computation, and Konrad Zuse's subsequent construction of the first working programmable computer (1935-1941), there has been a lot of work on specialized algorithms solving problems taken from more or less general problem classes. Apparently, however, one remarkable fact has so far escaped the attention of computer scientists: it is possible to use self-referential proof systems to build optimally efficient yet conceptually very simple universal problem solvers.

Many traditional problems of computer science require just
one problem-defining input at the beginning of the problem solving
process. For example, the initial input may be a large integer,
and the goal may be to factorize it.
In what follows, however, we will
also consider the *more general case*
where the problem solution requires interaction with a dynamic,
initially unknown environment that produces a continual stream of
inputs and feedback
signals, such as in autonomous robot control tasks,
where the goal may be to maximize expected cumulative
future reward [18]
(examples in Section 3.2).
This may require the solution of essentially arbitrary problems.

Back to Goedel Machine Home Page