Towards Concise, Machine-discovered Proofs of Gödel’s Two Incompleteness Theorems

MATR’s basic organizational unit is called the box. A box may contain a set of formula nodes, inference nodes, other boxes, and connections between nodes or boxes. If a box $\mathcal{B}$ contains a node or box $o$, then we say that $o$ has $\mathcal{B}$ as a parent box. All elements in MATR have exactly one parent box, with one exception: the top-level box. It is also referred to as the proof space or root box and is the starting point of all MATR proofs.

Formula nodes contain formula objects, which are typically S-expression strings. Inference nodes are used to link a set of formula nodes $\mathbf{F}$ (the premise node) to another formula node $\phi$ (the conclusion node), where $\phi\notin\mathbf{F}$. Inference nodes contain information about the nature of the inference from $\mathbf{F}$ to $\phi$, typically a string corresponding to the name of the inference rule, metadata about which codelet suggested the inference, and other information of use to codelets. Thus, directed edges connect formula nodes to inference nodes, and inference nodes to formula nodes, but never directly connect two nodes of the same type.

Formula nodes can also be axioms or goals of their parent box. If $\alpha$ is an axiom of box $\mathcal{B}$, then it is an axiom of any box which has $\mathcal{B}$ as a parent box. Formula nodes may also contain metadata such as the binary checked flag, which denotes whether a formula node follows from the axioms of its parent box. Formula nodes which are axioms of their parent boxes automatically have checked flags, and a special codelet propagates checked flags by looking at inference nodes: if, for inference node $i$, (1) all of $i$’s premise nodes have checked flags, and (2) $i$ is marked as a deductive¹¹1Although not used in this paper, inference nodes can correspond to non-deductive inferences, in order to open the door to proof-solving heuristics and proof tactics. inference, then $i$’s conclusion node is given a checked flag.

The most important component of MATR’s design is the codelet, an individual piece of specialized code whose job is to analyze the current proof space, and make recommendations about how to modify the proof space (typically the addition of inference and formula nodes). In keeping with the design principles listed earlier, codelets can be written in virtually any programming language, are easily interchangeable, and are principally responsible for both defining and behaving in accordance with the intended semantics of the proof state. The term ‘codelet’ is borrowed from the Copycat model of analogical reasoning (?; ?; ?), and like Copycat codelets, our codelets should be thought of as independently operating “worker ants” which each specialize in searching for a unique set of features in the proof space (or in a local subset of the proof space), and making recommendations based on their findings.

Most codelets directly correspond to inference rules; e.g., the Modus Ponens codelet simply looks for formulae pairs of the form $\phi$, $\phi\rightarrow\psi$ and recommends adding a “Modus Ponens” inference node and a $\psi$ formula node. Other codelets are responsible for background or support tasks, such as propagating checked flags, or ensuring that every formula node contains syntactically valid formulae. If the application calls for it, codelets may even contain entire external programs or automated theorem provers; e.g., we make use of a full first-order resolution codelet later in this paper.

MATR’s codelets typically operate either in a forward or backward mode. Forward-operating codelets look for sets of formulae that jointly satisfy some inference schema’s premises, and suggest the addition of a conclusion, as in the Modus Ponens example earlier. It is beneficial for such codelets to restrict its search to formulae that have checked flags, so that any new formula nodes added will also have checked flags propagated to them. Backwards operating codelets work in the other direction, adding formulae that lead to nodes which have yet to be checked. Allowing some codelets to operate unconstrained could result in a potentially infinite number of recommendations per iteration, such as a forward operating Disjunction Introduction codelet. This explosion is managed by heuristics in the codelet chooser and recommendation resolver.

The MATR core (sometimes referred to as the back-end) is the fixed central unit that coordinates all of MATR’s interchangeable parts. In its simplest form, it merely serves as the conduit through which the components of MATR communicate and maintains the repository of shared proof state. Currently, core presents a REST API which wraps a datascript graph database that holds all of the proof state. Core also provides provides a minimal Codelet Chooser and Recommendation Resolver. The former can be configured to trigger codelets based on the result of queries against the core database, while the latter is mostly focused on sanity checking (e.g. preventing the addition of duplicate nodes and boxes).

The front-end is the primary way to interact with MATR as a whole. It wraps some of core’s API into a graphical user interface that allows the user to upload a configuration to core, set up the axioms and goals of the proof space, trigger the execution of codelets, and view the resulting proof.

Codelet Servers act as hosts for the codelets provided by core. They present REST endpoints for the codelet chooser to send messages to trigger the execution of particular codelets. The codelets can then make additional queries against core, perform logical inferences, and the codelet server responds to the request with actions for the recommendation resolver.

As a demonstration and test of MATR’s proof-finding capabilities, we set out to generate a proof of Gödel’s First and Second Incompleteness Theorems, given a proof sketch. Verifying proofs of these theorems are often used as a sort of stress test for an automated reasoner’s formalism, and the the ability to automatically discover these proofs has been claimed by many with various degrees of success (?; ?; ?; ?; ?). All existing machine-discovered proofs of the incompleteness theorems rely on carefully selected symbols and inference rules. An ongoing goal of such work is to discover proofs of the incompleteness theorems with increasingly minimal assumptions and custom tailoring of the prover’s starting conditions. Here, our contribution does so with a formalism and automated reasoner robust enough to not only find concise proofs of both incompleteness theorems, but of similar theorems in the metalogical space as well.

Our formalizations of the incompleteness proofs are loosely based on the versions and terminology described by (?). Let us assume a Gödelian numbering scheme that assigns a unique integer to all formulae in first-order Peano Arithmetic (PA), using the normal conventions. Then for any well-formed-formula (wff) $\phi$ in PA, $\ulcorner\phi\urcorner$ denotes its corresponding Gödel number. Slightly abusing notation for convenience, if $\Phi$ is a proof in PA, $\ulcorner\Phi\urcorner$ denotes its corresponding encoding (called a Super Gödel number). Given an integer in $n\in\mathds{N}$, determining whether $n$ encodes a PA wff, a well-formed proof in PA, or neither, is decidable and captured in PA itself (?).

$\mathit{Prv_{PA}}(n)$ is shorthand for the wff formula in PA which expresses (but does not capture) the numerical property “$n$ corresponds to the Gödel number of a formula that is a theorem of PA.” This predicate also satisfies the Hilbert-Bernays provability conditions (Equations 2 - 4 below). $\mathit{Opposite}(m,n)$ is shorthand for the PA wff which is provable if and only if $n$ encodes a PA wff which is the negated form of the PA wff that $m$ encodes. Because this formula trivially captures a primitive recursive property, it is captured in PA (?) and thus it is an axiom that for all PA wffs $\phi$, PA $\vdash\mathit{Opposite}(\ulcorner\phi\urcorner,\ulcorner\neg\phi\urcorner)$. Consistency in PA is expressed by the formula $\mathit{Con_{PA}}$:

$$\forall_{m,n}(\mathit{Opposite}(m,n)\wedge\mathit{Prv_{PA}}(m))\rightarrow\neg\mathit{Prv_{PA}}(n)$$

(1)

More precisely, a metalogic wff is either: (1) a single formula symbol, (2) a PA wff, or (3) if $\phi$ and $\psi$ are metalogic wffs, then metalogic wffs include: $\neg\phi$, $\phi\vee\psi$, and so on using the normal rules of logical operators. All operators in first-order PA have analogs in the metalogic. Only one additional operator is added: The provability operator $\vdash$ is written $\square(p,f)$, where $p$ is a proof theory, and $f$ is a metalogic wff. It should be read, “the proof theory $p$ has the formula corresponding to $f$ as one of its theorems.” Unlike $\mathit{Prv_{PA}}(\ulcorner\psi\urcorner)$, which is a PA wff, $\square(PA,\psi)$ is a metalogic wff. Furthermore, $\forall_{\phi}\square(PA,\phi)\rightarrow\mathit{Prv_{PA}}(\ulcorner\phi\urcorner)$ and $\forall_{\phi}\square(PA,\mathit{Prv_{PA}}(\ulcorner\phi\urcorner))\rightarrow\mathit{Prv_{PA}}(\ulcorner\phi\urcorner)$ are provided as axioms, but the converse are not.

Given this notation, we can introduce the three Hilbert-Bernays provability conditions as axioms as well:

$$\forall_{\phi}\square(PA,\phi)\rightarrow\square(PA,\mathit{Prv_{PA}}(\ulcorner\phi\urcorner))$$

(2)

	$\displaystyle\forall_{\phi,\psi}$	$\displaystyle\square(PA,\mathit{\mathit{Prv_{PA}}(\ulcorner\phi\rightarrow\psi\urcorner)}$		(3)
		$\displaystyle\mathit{\rightarrow(\mathit{Prv_{PA}}(\ulcorner\phi\urcorner)\rightarrow\mathit{Prv_{PA}}(\ulcorner\psi\urcorner))})$

$$\forall_{\phi}\square(PA,\mathit{Prv_{PA}}(\ulcorner\phi\urcorner)\rightarrow\mathit{Prv_{PA}}(\ulcorner\mathit{Prv_{PA}}(\ulcorner\phi\urcorner)\urcorner))$$

(4)

$$\neg\exists_{\phi}\square(PA,\phi)\wedge\square(PA,\neg\phi)$$

(5)

To establish a basis for the proof, two initial setup codelets populate the proof space with several intermediate nodes and boxes to act as the foundation for later codelets. By statically introducing these intermediate nodes and boxes we guide the proof search process in a way which avoids combinatorial explosion. While the front end could be used to introduce each of these boxes and nodes by hand, using setup codelets simplified the process of re-running the entire proof while testing. In the future we hope to use heuristics to completely automate this as well. In our proof sketch we used three subproofs, which are created in this step. They are handled in setup due to the need for intermediate nodes to be placed in those subproofs as well. Additionally, the existential elimination acting on one of the axioms occurs in the setup so that the symbol chosen to take place of the quantifier is fixed to be the same as those used in the intermediate nodes.

In order to simplify the proof space, we employ four types of resolution codelets; two for the metalogic, and two for first-order logic. The two “$\mathit{PA\vdash}$” codelets simply search for formulae nodes $\square(PA,\phi_{1}),...,\square(PA,\phi_{n})$ with checked flags, and either a formula $\square(PA,\psi)$ without a checked flag or a $\square(PA,\bot)$ formula. It then attempts to show that, subject to timeout and memory limitations, $\psi$ follows from $\{\phi_{1},...,\phi_{n}\}$ using first-order resolution without equality. Likewise, the “$\mathit{ML\vdash}$” codelets search for formula nodes $\gamma_{1},...,\gamma_{m}$ with checked flags and uses resolution to prove whether a formula $\psi$ or $\bot$ without a checked flag follows. Although these codelets are quite powerful (and potentially combinatorially explosive), they do not operate in a purely forward mode, which severely limits what can be practically derived. But neither can either of these codelets complete the entire proof on their own. Consider the three Hilbert-Bernays Provability Conditions: After $\forall$-Elimination, Equations 3 and 4 produce subformulae that can be reasoned over by $\mathit{PA\vdash}$, but Equation 2 does not—it requires inferences at the metalogical level. Conceivably, one might simply strengthen $\mathit{ML\vdash}$ to subsume what $\mathit{PA\vdash}$ does, but this explodes its average run time, removes MATR’s ability to introduce smarter heuristics, and would prevent us from using a general purpose first order resolution implementation.

In order to ensure proper connection between the nodes introduced by the resolution codelet and the nodes that already exist outside of the subproof, a reiteration codelet connects the node outside of the subproof to the corresponding node inside the subproof. This allows for propagation of checks into the subproof, so that resolution can truly demonstrate that it has proven a particular formula with accordance to information both inside and outside of the subproof.

We also implemented a dedicated codelet for Hilbert-Bernays 1 (2) instead of providing it as an axiom of the root box. In testing, we discovered that providing HB1 as an axiom lead to an explosion of the number of necessary clauses to process in the resolution procedure. More specifically, the proof of Con(PA) with resolution explodes from 97 clauses to not resolving with an upper bound of 2000 clauses. The HB1 codelet works purely in a backwards mode, adding inferences for nodes of the form $\mathit{\square(PA,\mathit{Prv_{PA}}(\ulcorner\phi\urcorner))}$ and connecting to (or creating) a corresponding node of the form $\mathit{\square(PA,\phi)}$.

Once the proof is completed, a pruning process identifies (and displays) the shortest proofs of each goal node in the root box. Figure 2 shows this pruned proof. Pruning is accomplished in two steps. The first propagates forward from the axioms of every box to count the number of justifications in the shortest proof of any reachable and checked node. Given these proof size counts, a backwards traversal is performed from each goal of the root box to extract the nodes and boxes used in the shortest proof of that goal.

With the provided intermediate nodes, the proof takes four iterations to complete. Interestingly, the proof found by MATR is actually shorter than the proof sketch we used to select our intermediate nodes and high level proof structure. Most surprising to us was MATR using part of the proof of the first incompleteness theorem in its proof of the second, short circuiting three intermediate nodes.

MATR owes its existence to work started at the Rensselaer AI and Reasoning (RAIR) Lab and contributed to by many students and collaborators since then—too many to reasonably name here. We are extremely grateful to the support and contributions of them all.

This material is based upon work supported by the Air Force Office of Scientific Research under award numbers FA9550-17-1-0191 and FA9550-18-1-0052. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the United States Air Force.