... machine1
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.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
... machine3
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 $s$ 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 $s$ in phase $i$: 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