Important Instructions Used by Proof Techniques

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 $n$-th possible axiom to the current proof, apply-rule(k, m, n) applies the $k$-th inference rule to the $m$-th and $n$-th theorem in the current proof (appending the result), set-switchprog(m,n) sets $switchprog:= s^p_{m:n}$, 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.

1. get-axiom(n) takes as argument an integer $n$ computed by a prefix of the currently tested proof technique with the help of arithmetic instructions such as those used in previous work [47]. Then it appends the $n$-th axiom (if it exists, according to the axiom scheme below) as a theorem to the current theorem sequence in proof. The initial axiom scheme encodes:
   1. Hardware axioms describing the hardware, formally specifying how certain components of $s$ (other than environmental inputs $x$) may change from one cycle to the next.

      For example, if the hardware is a Turing machine²(TM) [56], then $s(t)$ 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 $F$ 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, $s(t)$ 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 $s_{1:64}$ is continually incremented as long as there is no overflow and the value of $s_{65}$ does not indicate that a jump to some other address should take place:
      

      $$(\forall t \forall n : [(n < 2^{64}-1) \wedge (n > 0) \wedge (t > 1) \wedge (t < T)$$
      
      
      
      
      $$\wedge (string2num(s_{1:64}(t))=n) \wedge (s_{65}(t)=\lq 0\textrm{'}) ]$$
      
      
      
      
      $$\rightarrow (string2num(s_{1:64}(t+1))=n+1))$$
      
      
      Here the semantics of used symbols such as `(' and `$>$' and `$\rightarrow$' (implies) are the traditional ones, while `$string2num$' symbolizes a function translating bitstrings into numbers. It is clear that any abstract hardware model can be fully axiomatized in a similar way.

   2. Reward axioms defining the computational costs of any hardware instruction, and physical costs of output actions, such as control signals $y(t)$ encoded in $s(t)$. Related axioms assign values to certain input events (encoded in variable $x$, a substring of $s$) representing reward or punishment (e.g., when a Gödel machine-controlled robot bumps into an obstacle). Additional axioms define the total value of the Gödel machine's life as a scalar-valued function of all rewards (e.g., their sum) and costs experienced between cycles $1$ and $T$, etc. For example, assume that $s_{17:18}$ can be changed only through external inputs; the following example axiom says that the total reward increases by 3 whenever such an input equals `11' (unexplained symbols carry the obvious meaning):
      
      $$(\forall t_1 \forall t_2: [(t_1 < t_2) \wedge (t_1 \geq 1) \wedge (t_2 \leq T) \wedge (s_{17:18}(t_2)=\lq 11\textrm{'}) ]$$
      
      
      
      
      $$\rightarrow [R(t_1,t_2)= R(t_1,t_2-1)+3]),$$
      
      
      where $R(t_1,t_2)$ is interpreted as the cumulative reward between times $t_1$ and $t_2$. It is clear that any formal scheme for producing rewards can be fully axiomatized in a similar way.

   3. Environment axioms restricting the way the environment will produce new inputs (encoded within certain substrings of $s$) in reaction to sequences of outputs $y$ encoded in $s$. For example, it may be known in advance that the environment is sampled from an unknown probability distribution $\mu$ contained in a given set $M$ of possible distributions (compare equation 1). E.g., $M$ may contain all distributions that are computable, given the previous history [52,53,16], or at least limit-computable [41,42]. Or, more restrictively, the environment may be some unknown but deterministic computer program [58,39] sampled from the Speed Prior [43] which assigns low probability to environments that are hard to compute by any method. Or the interface to the environment is Markovian [35], that is, the current input always uniquely identifies the environmental state--a lot of work has already been done on this special case [33,2,55]. Even more restrictively, the environment may evolve in completely predictable fashion known in advance. All such prior assumptions are perfectly formalizable in an appropriate $\cal A$ (otherwise we could not write scientific papers about them).

   4. Uncertainty axioms; string manipulation axioms: Standard axioms for arithmetics and calculus and probability theory [21] and statistics and string manipulation that (in conjunction with the hardware axioms and environment axioms) allow for constructing proofs concerning (possibly uncertain) properties of future values of $s(t)$ as well as bounds on expected remaining lifetime / costs / rewards, given some time $\tau$ and certain hypothetical values for components of $s(\tau)$ etc. An example theorem saying something about expected properties of future inputs $x$ might look like this:
      
      $$(\forall t_1 \forall \mu \in M: [(1 \leq t_1) \wedge (t_1 + 15597 < T) \wedge (s_{5:9}(t_1) = \lq 01011\textrm{'})$$
      
      
      
      
      $$\wedge (x_{40:44}(t_1)=\lq 00000\textrm{'}) ] \rightarrow (\exists t: [(t_1 < t < t_1 + 15597)$$
      
      
      
      
      $$\wedge (P_{\mu}(x_{17:22}(t) = \lq 011011\textrm{'}\mid s(t_1)) > \frac{998}{1000} )])),$$
      
      
      where $P_{\mu}(. \mid . )$ represents a conditional probability with respect to an axiomatized prior distribution $\mu$ from a set of distributions $M$ described by the environment axioms (Item 1c).

      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.

   5. Initial state axioms: Information about how to reconstruct the initial state $s(1)$ or parts thereof, such that the proof searcher can build proofs including axioms of the type
      
      $$(s_{{\bf m}:{\bf n}}(1)={\bf z}), ~e.g.:~ (s_{7:9}(1)=\lq 010\textrm{'}).$$
      
      
      Here and in the remainder of the paper we use bold font in formulas to indicate syntactic place holders (such as m,n,z) for symbol strings representing variables (such as m,n,z) whose semantics are explained in the text--in the present context $z$ is the bitstring $s_{m:n}(1)$.

      Note that it is no fundamental problem to fully encode both the hardware description and the initial hardware-describing $p$ within $p$ itself. To see this, observe that some software may include a program that can print the software.

   6. Utility axioms describing the overall goal in the form of utility function $u$; e.g., equation (1) in Section 2.1.

2. apply-rule(k, m, n) takes as arguments the index $k$ (if it exists) of an inference rule such as modus ponens (stored in a list of possible inference rules encoded within $p(1)$) and the indices $m, n$ of two previously proven theorems (numbered in order of their creation) in the current proof. If applicable, the corresponding inference rule is applied to the addressed theorems and the resulting theorem appended to proof. Otherwise the currently tested proof technique is interrupted. This ensures that proof is never fed with invalid proofs.

3. delete-theorem(m) deletes the $m$-th theorem in the currently stored proof, thus freeing storage such that proof-storing parts of $s$ can be reused and the maximal proof size is not necessarily limited by storage constraints. Theorems deleted from proof, however, cannot be addressed any more by apply-rule to produce further prolongations of proof.

4. set-switchprog(m,n) replaces $switchprog$ by $s^p_{m:n}$, provided that $s^p_{m:n}$ is indeed a non-empty substring of $s^p$, the storage writable by proof techniques.

5. check() verifies whether the goal of the proof search has been reached. First it tests whether the last theorem (if any) in proof has the form of a target theorem. A target theorem states that given the current axiomatized utility function $u$ (Item 1f), the utility of a switch from $p$ to the current switchprog would be higher than the utility of continuing the execution of $p$ (which would keep searching for alternative switchprogs). Target theorems are symbol strings (encoded in $s$) of the (decoded) form
   

   $$(u[s({\bf t_1}) \oplus (switchbit({\bf t_1})=\lq 1\textrm{'}), ... ... \oplus (switchbit({\bf t_1})=\lq 0\textrm{'}), Env({\bf t_1})] )$$ (2)

   
   
   where the variable $t_1$ (represented by syntactic place holder ${\bf t_1}$) stands for a time step, while all other symbols belong to the alphabet of the theorem-proving calculus, that is, the set of possible target theorems is parameterized only by $t_1$. Here the calculus should permit the notation $s({\bf t_1}) \oplus (switchbit({\bf t_1})=\lq b\textrm{'})$ as a shortcut for the state obtained when we replace switchbit($t_1$), the true value of the variable bit $switchbit$ (encoded in $s$) at time $t_1$, by $b \in \{0, 1\}$. This will facilitate the formulation of theorems that compare values conditioned on various alternative hypothetical properties of $s(t_1)$. (Note that $s(t_1)$ may be only partially known by the current proof technique even in environments where $s(t_1)$ and switchbit($t_1$) are fully predetermined for all valid $t_1$.)

   The purpose of introducing $t_1$ 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 $p(1)$, of course) to check whether there is enough time left to set variable switchbit (originally 0) to 1 before the continually increasing $time$ will equal $t_1$. If this subroutine returns a negative result, check() exits. Otherwise it sets switchbit $:=1$ (there is no other way of changing switchbit). Then it repeatedly tests $time$ until $time > t_1$, to make sure the condition of formula (2) was fulfilled at $t_1$. Then it transfers control to switchprog (there is no other way of calling switchprog). The switchprog may subsequently rewrite all parts of $s$, excluding hardware-reserved parts such as $time$ and $x$, but including $p$.

6. state2theorem(m, n) takes two integer arguments $m, n$ and tries to transform the current contents of $s_{m:n}$ into a theorem of the form
   
   $$(s_{{\bf m}:{\bf n}}({\bf t_1})={\bf z}), ~e.g.:~ (s_{6:9}(7775555)=\lq 1001\textrm{'}),$$
   
   
   where $t_1$ represents a time measured (by checking time) shortly after state2theorem was invoked, and $z$ the bistring $s_{m:n}(t_1)$ (recall the special case $t_1=1$ of Item 1e). So we accept the time-labeled current observable contents of any part of $s$ as a theorem that does not have to be proven in an alternative way from, say, the initial state $s(1)$, because the computation so far has already demonstrated that the theorem is true. Thus we may exploit information conveyed by environmental inputs, and the fact that sometimes (but not always) the fastest way to determine the output of a program is to run it.

   This non-traditional online interface between syntax and semantics requires special care though. We must avoid inconsistent results through parts of $s$ 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 $c$ cycles in a reserved part of $s$, 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 $s_{m:n}$ to be read might also contain the reading procedure's own, temporary, constantly changing string pointer variables, etc.³To address such problems on computers with limited memory, state2theorem first uses some fixed protocol (encoded in $p(1)$, of course) to check whether the current $s_{m:n}$ is readable at all or whether it might change if it were read by the remaining code of state2theorem. If so, or if $m,n,$ are not in the proper range, then the instruction has no further effect. Otherwise it appends an observed theorem of the form $(s_{{\bf m}:{\bf n}}({\bf t_1})={\bf z})$ to proof. For example, if the current time is 7770000, then the invocation of state2theorem(6,9) might return the theorem $(s_{6:9}(7775555)=\lq 1001\textrm{'})$, where $7775555-7770000=5555$ reflects the time needed by state2theorem to perform the initial check and to read leading bits off the continually increasing $time$ (reading $time$ also costs time) such that it can be sure that $7775555$ is a recent proper time label following the start of state2theorem.

The axiomatic system $\cal A$ is a defining parameter of a given Gödel machine. Clearly, $\cal A$ 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].