How Online Proof Techniques Connect Syntax and Semantics

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 $rightarrow,wedge,=,(,), forall, exists, ldots$, $c_1, c_2, ldots,$ $f_1, f_2, ldots$.

A proof is a sequence of theorems. Each theorem is either an axiom or inferred from previous theorems by applying one of several given inference rules such as modus ponens combined with unification [9]. It is obvious and well-known that theorems can be uniquely encoded as bitstrings, and that one can write a program that systematically enumerates all possible proofs--compare Gödel's original paper [10] and any textbook on logic or proof theory, e.g., [9]. In what follows, we do not have to specify all details of a particular axiomatic encoding--it suffices to recall that concepts such as elementary hardware operations, computational costs, utility functions, probability, provability, etc. can be formalized.

First consider a brute force proof searcher systematically generating all proofs in order of their sizes. To produce a certain proof, this approach takes time exponential in proof size.

Instead our $p(1)$ will produce many proofs with low algorithmic complexity [48,20,25] much more quickly. It runs and evaluates proof techniques composed from instructions of the $p(1)$-encoded language $cal L$. For example, $cal L$ may be a variant of PROLOG [7] or the universal FORTH[26]-inspired programming language used in recent experiments with OOPS [38,40]. $cal L$ includes instructions that allow any part of $s$ to be read, such as inputs $x$, or the code of $p(1)$. Other instructions in $cal L$ may write on $s^p$, a part of $s$ reserved for temporary results of proof techniques. The output of any tested proof technique written in $cal L$ is an incrementally growing proof placed in the string variable proof stored somewhere in $s$ (proof and $s^p$ are reset to the empty string at the beginning of each new proof technique test). Certain long proofs can be produced by short proof techniques.

What is the best way of systematically testing proof techniques? Section 2.3 will later present a general, bias-optimal [38,40] proof searcher initialization $p(1)$ of $p$. This initialization, however, is not essential for understanding the basic principles of the Gödel machine, as there are many alternative initializations.

For now it is more important to specify the precise goals of the proof search, details of the proofs that can be derived by proof techniques, and ways of verifying proofs and translating their results into online changes of the Gödel machine software. This is most conveniently done by describing the essential instructions for generating/checking axioms/theorems and for transferring control to provably good Gödel machine-changing programs.

Back to Goedel machine home page