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 machine2(TM) , 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.
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: