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 [46,20,25] much more quickly. It runs and evaluates proof techniques written in language $\cal L$ implemented within $p(1)$. 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]. Certain long proofs can be produced by short programs.

Section 2.3 will present a general, bias-optimal [38,40] way of systematically testing proof techniques through a convenient initialization $p(1)$ of $p$. First, however, we need 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