- ... machine
^{1} - Or
*`Goedel machine'*, to avoid the*Umlaut*. But*`Godel machine'*would not be quite correct. Not to be confused with what Penrose calls, in a different context,*`Gödel's putative theorem-proving machine'*[27]!. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...
state.
^{2} - The concept of online
proof techniques raises several unconventional
issues concerning the connection between syntax and semantics.
Proofs are just symbol strings produced from other symbol strings
according to certain syntactic rules. Such a symbol string, however, may
be interpreted in online fashion as a statement about the computational
costs of the program that computes it (a semantic issue), and may suggest
a Gödel machine-modifying algorithm whose execution would be semantically useful
*right now*as the proof is being created. BIOPS must deal with the fact that the utility of certain self-modifications may depend on the remaining lifetime, and with the problem of producing the right proof at the right time.. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ... machine
^{3} -
Turing reformulated Gödel's unprovability results in terms
of Turing machines (TMs) [52] which
subsequently became the most widely used abstract model of
computation. It is well-known that there are
*universal*TMs that in a certain sense can emulate any other TM or any other known computer. Gödel's integer-based formal language can be used to describe any universal TM, and vice versa.. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...
etc.
^{4} - We see that certain parts of the
current may not be directly observable without changing
the observable itself.
Sometimes, however, axioms and previous observations will allow
the Gödel machine to
*deduce time-dependent storage contents that are not directly observable. For instance, by analyzing the code being executed through instruction pointer**IP in the example above, the value of**IP at certain times may be predictable (or postdictable, after the fact). The values of other variables at given times, however, may not be deducable at all. Such limits of self-observability are reminiscent of Heisenberg's celebrated uncertainty principle [11], which states that certain physical measurements are necessarily imprecise, since the measuring process affects the measured quantity.*. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

*....*^{5}*Even faster search is possible for proof techniques that do not read changing parts of in phase : we do not have to recompute results of their own, shorter, previously executed prefixes. The precise, recursive, backtracking-based procedure for this case is more complex than Method 2.1 and has been described elsewhere [38,40].*. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Back to Goedel machine home page