The nature of the six proof-modifying instructions below (there are no others) makes it impossible to insert an incorrect theorem into proof, thus trivializing proof verification. Let us first provide a brief overview of the most important instructions: get-axiom(n) appends the -th possible axiom to the current proof, apply-rule(k, m, n) applies the -th inference rule to the -th and -th theorem in the current proof (appending the result), set-switchprog(m,n) sets , and check() tests whether the last theorem in proof is a target theorem showing that a self-rewrite through switchprog would be useful. The details are as follows.
For example, if the hardware is a Turing machine2(TM) [56], 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.
For instance, the following axiom could
describe how some 64-bit hardware's instruction pointer
stored in is continually incremented as long as
there is no overflow and the value
of does not indicate that a jump to some other address
should take place:
Given a particular formalizable hardware (Item 1a) and formalizable assumptions about the possibly probabilistic environment (Item 1c), obviously one can fully axiomatize everything that is needed for proof-based reasoning about past and future machine states.
Note that it is no fundamental problem to fully encode both the hardware description and the initial hardware-describing within itself. To see this, observe that some software may include a program that can print the software.
The purpose of introducing is to deal with hardware-specific temporal delays that may be involved in checking and switching--it may take a significant amount of time to match abstract symbol strings found during proof search to the Gödel machine's real current state. If a target theorem has been found, check() uses a simple prewired subroutine (also encoded in , of course) to check whether there is enough time left to set variable switchbit (originally 0) to 1 before the continually increasing will equal . If this subroutine returns a negative result, check() exits. Otherwise it sets switchbit (there is no other way of changing switchbit). Then it repeatedly tests until , to make sure the condition of formula (2) was fulfilled at . Then it transfers control to switchprog (there is no other way of calling switchprog). The switchprog may subsequently rewrite all parts of , excluding hardware-reserved parts such as and , but including .
This non-traditional online interface between syntax and semantics requires special care though. We must avoid inconsistent results through parts of that change while being read. For example, the present value of a quickly changing instruction pointer IP (continually updated by the hardware) may be essentially unreadable in the sense that the execution of the reading subroutine itself will already modify IP many times. For convenience, the (typically limited) hardware could be set up such that it stores the contents of fast hardware variables every cycles in a reserved part of , such that an appropriate variant of state2theorem() could at least translate certain recent values of fast variables into theorems. This, however, will not abolish all problems associated with self-observations. For example, the to be read might also contain the reading procedure's own, temporary, constantly changing string pointer variables, etc.3To address such problems on computers with limited memory, state2theorem first uses some fixed protocol (encoded in , of course) to check whether the current is readable at all or whether it might change if it were read by the remaining code of state2theorem. If so, or if are not in the proper range, then the instruction has no further effect. Otherwise it appends an observed theorem of the form to proof. For example, if the current time is 7770000, then the invocation of state2theorem(6,9) might return the theorem , where reflects the time needed by state2theorem to perform the initial check and to read leading bits off the continually increasing (reading also costs time) such that it can be sure that is a recent proper time label following the start of state2theorem.
The axiomatic system is a defining parameter of a given Gödel machine. Clearly, must be strong enough to permit proofs of target theorems. In particular, the theory of uncertainty axioms (Item 1d) must be sufficiently rich. This is no fundamental problem: we simply insert all traditional axioms of probability theory [21].