The Gödel machine's life consists of discrete cycles or time steps . Its total lifetime may or may not be known in advance. In what follows, the value of any time-varying variable at time will be denoted by ; its initial value by .

During each cycle the Gödel machine hardware (which may be emulated as unchangeable software on a traditional computer) executes an elementary operation which affects its variable state (without loss of generality we assume is encoded as a bitstring) and possibly also the variable environmental state , where the possibly uncountable set may be unknown or only partially known.

Instead of insisting on a linear relationship between cycles and physical time, we use a hardware-oriented, causal model of time embodied by a hardwired state transition function . For , is the state at a point where the hardware operation of cycle is finished, but the one of has not started yet. may depend on and is simultaneously updated or (probabilistically) computed by the possibly reactive environment, whose computational resources may vastly exceed the ones of the Gödel machine.

For example, if the hardware is a
Turing machine^{2}(TM) [50],
then is a bitstring that encodes the current
contents of all tapes of the TM, the positions of its
scanning heads, and the current *internal state*
of the TM's finite state automaton, while specifies
the TM's look-up table which maps any possible combination
of internal state and bits above scanning heads
to a new internal state and an action such as:
replace some head's current bit by 1/0, increment
(right shift) or decrement (left shift) some
scanning head, read and copy next input bit to cell above
input tape's scanning head,
etc. Alternatively, if the hardware is given by the abstract model
of a modern microprocessor with limited storage, will
encode the current storage contents,
register values,
instruction pointers etc.

In order to conveniently talk about programs and data,
we will often attach names to certain string variables encoded
as components or substrings of .
Of particular interest are 7 variables called
*time*,
*x*,
*y*,
*p*,
*proof*,
*switchbit*,
*switchprog*, to be explained below.
All these variables except for the hardware-written
*time* and *x* are in principle writable by programs
stored within , although at least the initial software
or policy will be set up such that initially can
modify only certain limited parts of , as long as it cannot
prove the usefulness of modifying other parts as well.

- At time , variable
holds a unique binary representation of .
We initialize
, the bitstring consisting only of a one.
The hardware increments from one cycle to the next.
This requires at most and on average only
computational steps.
- Variable
*x*holds environmental inputs. For , may differ from only if a program running on the Gödel machine has executed a special input-requesting instruction at time . Generally speaking, the delays between successive inputs should be sufficiently large so that programs can perform certain elementary computations on an input, such as copying it into internal storage (a reserved part of ) before the next input arrives. - is an output bitstring which may subsequently influence the
environment, where
by default.
For example, could be interpreted as a control
signal for an environment-manipulating
robot whose actions may have an effect on
future inputs.
- is the initial software: a program
implementing the original policy
for interacting with the environment and for proof searching.
Certain parts of may be
used by the policy for computing temporary results.
Using some sort of process interleaving technique,
the initial is written such
that it will allocate a fixed fraction of the time to
a subpolicy , which
somehow computes outputs in response to inputs .
We may initialize by any known problem solving algorithm,
to exploit from the start whatever
initial prior knowledge is available.
In the remaining time will execute a proof-searching subroutine that systematically tests proof-generating programs called

*proof techniques*written in a universal programming language implemented as part of the initial software running on the Gödel machine's hardware. A special role is played by three global variables (initially) writable*only*by proof techniques:*switchprog*holds a program whose execution may directly modify any part of the Gödel machine except for variables that can be set directly only by the hardware or by the environment, such as and (or, in case a TM is used as hardware, the representation of the current internal state of the TM's finite state automaton).*switchbit*is a binary variable initialized by `0'. Setting it to `1' starts the unstoppable process of transferring control to the current*switchprog*.*proof*holds a proof incrementally computed by the currently tested proof technique. The proof searcher's goal is to find a proof stating that*switchbit*should be set, which implies that the current*switchprog*will be executed. So the decision of whether the Gödel machine should be changed in a particular way (out of many possible ways) will be reduced to the binary decision of whether*switchbit*should adopt a particular value. The next subsections will describe details; the final Section 4 will summarize everything.

Back to Goedel machine home page