Essential Details of One Representative Gödel Machine

Notation. Unless stated otherwise or obvious, throughout the paper newly introduced variables and functions are assumed to cover the range implicit in the context. $l(q)$ denotes the number of bits in a bitstring $q$; $q_n$ the $n$-th bit of $q$; $\lambda$ the empty string (where $l(\lambda)=0$); $q_{m:n}= \lambda$ if $m>n$ and $q_m q_{m+1} \ldots q_n$ otherwise (where $q_0 := q_{0:0} := \lambda$).

Theorem proving requires an axiom scheme yielding an enumerable set of axioms of a formal logic system $\cal A$ whose formulas and theorems are symbol strings over some finite alphabet that may include traditional symbols of logic (such as $\rightarrow,\wedge,=,(,), \forall, \exists, \ldots$, $c_1, c_2, \ldots,$ $f_1, f_2, \ldots$), probability theory (such as $E(\cdot)$, the expectation operator), arithmetics ( $+, -, /, = , \sum, <, \ldots$), string manipulation (in particular, symbols for representing any part of state $s$ at any time, such as $s_{7:88}(5555)$). A proof is a sequence of theorems, each either an axiom or inferred from previous theorems by applying one of the inference rules such as modus ponens combined with unification, e.g., [10].

The remainder of this paper will omit standard knowledge to be found in any proof theory textbook. Instead of listing all axioms of a particular $\cal A$ in a tedious fashion, we will focus on the novel and critical details: how to overcome potential problems with self-reference and how to deal with the potentially delicate online generation of proofs that talk about and affect the currently running proof generator itself.