Essential Details of One Representative Gödel Machine

Theorem proving requires an
axiom scheme yielding an
enumerable set of
axioms of a formal logic
system whose formulas and theorems are symbol
strings over some finite alphabet that may include traditional
symbols of logic (such as
,
),
probability theory (such as , the expectation operator),
arithmetics (
),
string manipulation (in particular, symbols for
representing any part of state at any time,
such as
).
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 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.